previous
|
start
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