Part 7
Parameter Mode "alters x "  

The incoming value of x (#x) will be used by the operation as specified in the ensures clause, and the outgoing value of x is an unspecified value of the same type.

Operation Guess (alters Num: Integer);

Main program:
     Var Num: Integer;
     Num := 11;
     Guess (Num);

After Guess executes:
     Num can be any Integer value: 7, 11, 35, etc.