Part 3

Equivalent Specifications

There is more than one way to write correct specifications using math notation. Refer to the specification of Stack Template. Let's look at the requires clause of the Stack operation Push:

Operation Push( alters E: Entry; updates S: Stack);
      requires: |S| < Max_Depth;

The specification above says that the length of the Stack should be less than Max_Depth, the max number of elements allowed on the stack. But we can also write it like this:
                requires: |S| <= Max_Depth + 1;

Both the requires clauses have the same meaning, because each statement can be proven using the other one. They are equivalent.