The incoming value of x (#x) will be used by the operation as specified in the ensures clause, and the outgoing value x will be reset to the initial value as defined in the template of that type.

In a Stack modeled by a mathematical string the initial value is empty string. An Integer will be reset to zero.

Operation Mystery (clears Num: Integer);

Main program:
     Var Num: Integer;
     Num := 5;
     Mystery (Num);

After Mystery executes:
      Num = 0;