Postconditions

• Conditions that the service provider guarantees
• Every method promises description, @return
• Sometimes, can assert additional useful condition
• Example: add method
  

  @postcondition size() > 0
  

• Postcondition of one call can imply precondition of another:
  

  q.add(m1);
  m2 = q.remove();