Part 2

Writing Operation Specifications in RESOLVE

 
The operation below increments an integer.

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

In the ensures clause the "#" notation is used to indicate an incoming value.

Parameter modes specify the effect of the operation on the incoming value of the parameter.

The requires clause is the responsibility of the caller, that is, before you call the operation Increment, you must make sure that the incoming parameter Num is within the specified range.

The ensures clause is the responsibility of the operation implementer. The example above guarantees that the new outgoing value of Num is the old incoming value (#Num) incremented by one.