Procedure Calls

  A valid procedure call is processed as follows:

1. If the call has in- or inout-arguments then (a copy of) the block which is the procedure body is prefixed by initialized local declarations parameter specification := argument.
2. If the call has out-parameters then the body is further prefixed by local declarations parameter specification.
3. If the procedure specifies a result type then the body of the procedure is prefixed with a local declaration res: result type declaring res as a local variable of the result type given in the declaration of the procedure.

   The order in which these local declarations are added to the procedure body is undefined although the arguments and the parameters correspond in the order in which they are written.

   Hint: The fact that the order of evaluating the arguments is not specified is especially important for inlining code.

4. The local declarations specified in steps 1 to 3 are processed.
5. The body of the procedure is processed. If the procedure specifies a result type the processing of the body must contain at least one assignment to the variable res.
6. The processing of the body ends when the end of the body or the statement return is reached. Then the current value of res is the result of the procedure call. If the procedure contained out- or inout-parameters then the entities designated by the out-arguments are determined and the current values of the corresponding local variables created in step 2 are assigned to these entities.
7. If the class in which the procedure is declared contains a feature named invariant then this must be a parameterless procedure yielding a result of type BOOL. This procedure is called. The original procedure call is undefined if the result is false.
8. The local entities of the procedure are discarded and the result is returned to the caller.

If a procedure call occurs as a statement then its result, if any, is discarded. The semantics of a program must not depend on the evaluation of invariants.