Precondition and Postcondition

Precondition

---

The constraints on the method's input and the states of all related objects that must hold before the method is called.

The precondition involves:

• explicit parameters
• implicit parameters (e.g. instance variables in the same class)
• global variables

Postcondition

---

The constraints on the method's output and the states of all related objects that the method guarantees when it returns.

The postcondition may involve both

• what is changed
• what remains unchanged

The precondition \(P\) and the postcondition \(Q\) of a method \(M\) can be represented by the correctness formula \(\{ P \}M\{ Q \}\), also known as Hoare Triples.

\(\{ P \}M\{ Q \}\) can be read as "any execution of \(M\), starting in a program state where \(P\) holds, will terminate in a program state where \(Q\) holds."

Program state is not just limited to the method itself, but all relevant objects in the program.

The correctness formula captures semantic properties of the method, meaning it may be independent of the method's implementation details.

• Consider a Stack object: its pop and peek methods require that the Stack is not empty. That the stack is implemented with a Vector doesn't matter, nor does the actual implementation of pop or peek.
• In other words, the precondition and postcondition of a method describe what to do rather than how to do it.

Preconditions and postconditions may be specified as:

• comments in source code
• part of the API documentation
• executable assertions in source code
  • goal: terminate the program on unexpected failure conditions
  • NOTE:
    • assertions should be used to check for conditions that should never occur to identify bugs.
    • assert is not a control structure
    • assert is not an input-checking mechanism
  • as opposed to exceptions, which handle expected failure conditions

Assumed Precondition vs. Validated Precondition

• Assumed Precondition (demanding)
  • method assumes that the precondition is always satisfied by all clients
  • clients check for precondition before calling method
  • adopted in design by contract, must follow those rules
    • only applies in trustworthy environment
• Validated Precondition (tolerant)
  • the precondition is validated in the method body by some control structure
    • if/then, etc.
  • often adopted by defensive design to deal with untrusted clients/external environments
  • very important for safety- and security-critical software

Validating a precondition either

• turns the original precondition into a tautology
• converts a partial function¹ into a total function²

Validation turns the original precondition into a part of the actual postcondition with a conditional effect. An assumed precondition/corresponding postcondition of

Precondition:  0 <= row < TOTAL_ROWS and 0 <= column < TOTAL_COLUMNS

Postcondition: return value is either Cell.EMPTY, Cell.CROSS, or Cell.NOUGHT

when validated becomes

Precondition:  none (tautology, always applicable)

Postcondition: return value is either Cell.EMPTY, Cell.CROSS, or Cell.NOUGHT
               if 0 <= row < TOTAL_ROWS and 0 <= column < TOTAL_COLUMNS
               otherwise null

When a method declares a precondition, it usually assumes that the client is responsible for validating the precondition.

In Test-Driven Development, the precondition and postcondition change over time as the development process evolves. The pre/postconditions at a specific time only reflect the assumptions behind that current iteration of code.

Pre/Postcondition Specifications

Pre/postconditions need to be specified rigorously and precisely. This allows us to use the specification to reason about the correctness of an implementation.

Obtaining a precise, rigorous specification isn't a trivial task. Consider the following correct specification for a sorting algorithm (p. 101 contains incorrect examples as well).

Note: count(x, list) returns the number of occurrences of element x in list

Postcondition:
  - p.length = q.length
  - q[i] <= q[i + 1] for any i
  - 0 <= i < q.length - 1 and count(p[j], p) = count(p[j], q), 0 <= j < p.length

Postcondition specifications need to consider both what should change after a method call and what should remain unchanged.

As a general rule, don't over-specify what should remain unchanged. Avoiding all-knowing oracles is an important TDD practice! Checking every detail every time can decrease test efficiency, slowing the iteration speed of TDD (tests should be efficient to be run so frequently).

Practice Exercises

Write accurate and meaningful specifications for the following:

• int[] reverse(int[] list) returns the reversed order of all elements in list.
• int linearSearch(int[] list, int key) returns the index of the first occurrence of key in list or -1 if it is not found.
• bool isVowel(char letter) returns true if letter is a vowel.
• bool isLeapYear(int year) returns true if it is a leap year.
• TriangleType reportTriangleType(int a, int b, int c) returns the triangle type for the given sides a, b, and c.
  • TriangleType is an enumeration type {SCALENE, ISOSCELES, EQUILATERAL}.

Footnotes