Specification Structure
- A precondition, indicated by the keyword requires
- A postcondition, indicated by the keyword effects
- A frame condition, indicated by the keyword
modifies
- The precondition is an obligation of the client.
- The postcondition is an obligation of the implementor of
the method.
- The frame condition identifies which objects may be modified.
José M. Vidal
.
4 of 16