Change of Contract

Impact of Contract Change

Updating a method during development is common for any variety of reasons.

When a method's signature is changed, all clients (including unit tests) must be updated as well. This sort of change will likely result in compiler errors, which are easy (if tedious) to find and fix.

Updates become especially risky when a method's original contract is modified without changing the method's signature. This is an implicit interface change that may or may not break existing client code.

Rule of Contract Change

There are some circumstances where pre/postcondition change may not break client code (including test code).

Rule of Contract Change

A safe change to a method may replace:

  • the existing precondition with an equal or weaker one
  • the existing postcondition with an equal or stronger one

Given two unequal conditions \(P_1\) and \(P_2\):

  • \(P_1\) is stronger than \(P_2\) if \(P_1 \implies P_2\).

For example:

  • \(x > 10\) is stronger than \(x > 5\).
  • \(y > 0\) is stronger than \(y \geq 0\).

Some conditions that seem different at first glance may be equivalent.

  • \(x > 0 \iff 2x > 0\), so the conditions are equivalent.
  • even(x) \(\equiv\) !odd(x)

Two unequal conditions may also not be comparable. This circumstance may break client code.

  • \(x = 1\) is not stronger or weaker than \(x = 2\).
  • list.length=count is not stronger or weaker than list.length=count-1.

Unit tests, if they exist, can be very convenient for verifying the impacts of contract change.

Contract Change is Incremental

A special case of contract change is adding new code to a method while preserving existing functionality for incremental development (such as in TDD). We have to ensure that whenever the new version is correct, the old version is also correct. If it is not, we have to modify existing code.

The opposite is not necessarily true! A correct original version doesn't guarantee that new code is correct.

Formalizing this idea: \[ (P_2 \implies Q_2) \implies (P_1 \implies Q_1) \] where \(P_1, Q_1\) are the original pre/postconditions and \(P_2, Q_2\) are the new pre/postconditions.

The above rules of equal or weaker new precondition and equal or stronger new postcondition are sufficient (but not necessary) for the above correctness argument.

Theorem: Let \(P_1 \implies P_2\) and \(Q_2 \implies Q_1\).

  • Then \((P_2 \implies Q_2) \implies (P_1 \implies Q_1)\).

Proof: omitted, available on p. 111

Consider precondition validation1 from Section 4.2. Converting a precondition \(P\) into a tautology necessarily weakens it.2 However, it's not clear that the postcondition is necessarily strengthened. When reasoning about the weaker or stronger relation of postconditions, we may need to consider their corresponding preconditions.

To do so, we need to prove that \(Q_2\) is stronger than \(Q_1\). In other words, show that \(Q_2 \implies Q_1\).3

Page 111 contains more formulations of this idea.

Takeaway

Code updated with a weaker precondition and a stronger postcondition

  • accepts more inputs
  • produces correct results.

Footnotes

1

Specifically the sense of turning the original precondition into a tautology and moving it into the postcondition.

2

Let \(P\) be an arbitrary expression, then \(P \implies \text{true}\). Thus, \(\text{true}\) is weaker than any expression \(P\).

3

We're trying to prove that whenever the new postcondition (\(Q_2\)) is true, the old postcondition (\(Q_1\)) must also be true. It's a verification that a contract change (new functionality) will never break the original contract expected by a caller.