Part 4

Redundant Specifications

Specifications can also be redundant. Let's examine the ensures clause of the Stack operation Push.

Operation Push( alters E: Entry; updates S: Stack);
       requires: |S| <= Max_Depth;
       ensures: S = <#E> o #S and |S| = |#S| + 1;

The new stack is now the new element concatenated with the contents of the initial stack, which implies that the length of the new Stack will now one longer. The conjunct "|S| = |#S| + 1" is redundant.