Methods definitions may include optional pre- and post-conditions. Together with 'assert' and these features allow the earnest programmer to annotate the intention of code. The Sather compiler provides facilities for turning on or off the runtime checking these safety features imply. Classes may also define a routine named 'invariant', which is a post condition that applies to all public methods.
These safety features are associated with the notion of programming contracts. The precondition of a method is the contract that the method requires the caller to fulfill. It is a statement of the condition of the world that the method needs to find, in order to work correctly. The postcondition is a contract that the method guarantees, if its precondition has been met. It is a statement of the state the method will leave the world in, when it is finished executing. These programming contracts are very important in the creation of robust, reusable code.
In addition to providing a level of checking, these safety features are also an invaluable form of documentation. Since preconditions and postconditions must actually execute, they can be trusted to be accurate and up-to-date, unlike method comments which may easily fall out of sync with the code.
A precondition states the assumptions that a method makes. It is the contract that the caller must fullfil in order for the routine to work properly. Preconditions frequently include checks that an argument is non-zero or non-void.
The optional 'pre' construct of method definitions contains a boolean expression which must evaluate to true whenever the method is called; it is a fatal error if it evaluates to false.The expression may refer to self and to the routine's arguments. For iterators, pre and post conditions are checked before and after every invocation of the iterator (not just the first or last time the iterator is called).
class POSITIVE_INTERVAL is
readonly attr start, finish:INT;
create(start, finish:INT)
-- Ensure that the interval is positive on positive numbers
pre start > 0 and finish > 0 and finish-start >= 0
is
res ::= new;
res.start := start;
res.finish := finish;
return res;
end;
end; -- class POSITIVE_INTERVAL |
Note that it is usually not appropriate to place conditions on the internal state in the precondition. This is an inappropriate conduct, since it may be impossible for the caller to determine whether the conduct can be properly fulfilled.
move_by(i:INT) pre start > 0 is ... |
The test on 'start' is actually verifying something about the internal state of the object, and has nothing to do with the caller of the routine. Tests such as the one above are more appropriately placed in assertions.