preassertion

Syntax   An preAssertion is:

 pre trueFalseExpn

Description   A pre assertion is a special form of an assert statement that is used at the beginning of a procedure or function. It is used to give requirements that the caller of the procedure or functions is supposed to satisfy. These requirements are given by the trueFalseExpn. The trueFalseExpn is evaluated. If it is true, all is well and execution continues. If it is false, execution is terminated with an appropriate message. See assert statements and procedure and function declarations for more details. See also post and invariant assertions.

Example   This function computes the average of n values. Its pre condition requires that n must be strictly positive, to avoid the possibility of dividing by zero when computing the average.

        function average ( a : array 1 .. * of real, n : int) : real
            pre n > 0
            var sum : real := 0
            for i : 1 .. n
                sum := sum + a ( i )
            end for
            result sum / n
        end average
Details   A pre assertion can also be used in a module, monitor, class or process declaration to make sure that requirements for initialization are met.

See also   module and process.