| 3. Specification Structure | ||
|---|---|---|
 | Chapter 17. Specification |  |
| 3. Specification Structure | ||
|---|---|---|
| | Chapter 17. Specification | |
A specification of a method consists of several clauses:
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 on the client (i.e., the caller of the method). It’s a condition over the state in which the method is invoked.
If the precondition does not hold, the implementation of the method is free to do anything.
The postcondition is an obligation on the implementor of the method. If the precondition holds for the invoking state, the method is obliged to obey the postcondition by returning appropriate values, throwing specified exceptions, etc.
The frame condition identifies which objects may be modified. If we say modifies x, this means that the object x, which is presumed to be mutable, may be modified, but no other object may be.
Omitted clauses:
precondition: That means that every invoking state satisfies it, so there is no obligation on the caller. In this case, the method is said to be total
postcondition: It is never omitted.
frame: The default is modifies nothing. In other words, the method makes no changes to any object.
Copyright © 1998-2009 Dilvan Moreira
| |  | |
| 2. Behavioral Equivalence |  | 4. Declarative Specification |