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();
previous
|
start
|
next
.... [Slide 50] ....