precondition
   Condition                      Comment

   Condition  error OutArgument   Comment

   Condition  fault OutArgument   Comment

   Condition  catch Name          Comment
.

A precondition consists of a set of assertions that are run first in a procedure. They are coded after any other declarations in the preamble and before any executable commands in the procedure body. The conditions they assert can only reference parameters and use constants and intrinsic functions.

Preconditions are part of a procedure's signature. They provide useful documentation when writing a call to a procedure. Compilers can potentially use them for optimization and static analysis.

An initial value declared on an Exit parameter is set before the Precondition is checked. Any variable length arrays are allocated only after the precondition has passed.