Part 9
Parameter Mode "updates x "

The outgoing value of x will be an update of the input value as specified in the ensures clause.

Operation Increment (updates I: Integer);
      requires: I < Max_Int;
      ensures: I = #I + 1;

In the main program we have:
     Var Num: Integer;
     Num := 2;
     Increment (Num);

Then after operation Increment executes:
     Num = 3;