Constraints
(assert | pre | post | inv) condition
- An assert condition is checked whenever the instruction is reached.
- A pre condition is checked just before the first instruction of the procedure or function, in which the constraint appears, is followed.
- A post condition just before the instruction following the call to the procedure or
function, in which the constraint appears, is followed.
- An invariant condition must be defined globally and is implicitly added to
every pre and post condition in the same module.
If a constraint condition is False when checked, a debugging environment
should report the violation and stop the program. In a program that may not stop,
nothing happens.
Compilers used to compile programs which may not stop on errors are
expected to produce warnings for every constraint condition which might not always
result in True when checked.
Implementation note.
Herman Venter
This is Slim documentation as snarfed on 27 May 1999 by dB.