Chapter 11. Safety Features

Table of Contents
11.1. Pre- and post-conditions
11.2. assert statements
11.3. initial expressions
11.4. result expressions

Methods definitions may include optional pre- and post-conditions (See Routine definitions). Together with 'assert' and 'invariant' (See invariant), these features allow the earnest programmer to annotate the intention of code. Implementations of Sather must provide facilities for turning on and off the runtime checking that these features require. The behavior of code that fails to meet the stated safety assertions is undefined. This allows an optimizing compiler to exploit the stated assertions even if they are not checked.

11.1. Pre- and post-conditions

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, not just once per loop.

The optional 'post' construct of method definitions contains a boolean expression which must evaluate to true whenever the method returns; it is a fatal error if it evaluates to false. The expression may refer to self and to the routine's arguments. It may use 'result' expressions (See result expressions) to refer to the value returned by the routine and 'initial' expressions (See initial expressions) to refer to values which are computed before the routine executes.

Classes may also define 'invariant', which is a post condition that applies to all public methods (See invariant).