4.5. Postconditions🔗

A postcondition for a procedure is a condition that is guaranteed to hold after the procedure executes. Sometimes, we can capture the entire desired behavior of a procedure with a postcondition that is simpler than the procedure's implementation. A typical example of sorting a list of numbers: the end result, that the list is sorted, is simpler to describe than the algorithm to do the sorting.

When a postcondition can capture the entire desired behavior of a procedure, and is simpler than the body, then adding it allows improving the correctness guarantee of your program, since only the simpler postcondition needs to be reviewed for correctness. Also, when postconditions are added to a procedure, callers will only be able to use the postconditions to reason about the call, and not the body. This simplifies reasoning at the call-site, improving verification results.

In Laurel, to be explicit, a procedure with postconditions must be marked as opaque, indicating that its body is not visible to callers. A procedure without postconditions can also be marked opaque, although then callers will know nothing about the result of the call. By default Laurel procedures have a transparent body, meaning that callers can use the callee's body for reasoning about the call's result.

procedure max(x: int, y: int) returns (r: int)
  opaque
  ensures r >= x
  ensures r >= y
  ensures r == x || r == y
{
  if x > y then { r := x }
  else { r := y }
};

At a call site, the postcondition is all the caller knows about the result:

procedure useMax()
  opaque
{
  var m: int := max(3, 7);
  assert m >= 3;
  assert m >= 7
  // we cannot assert m == 7 here: the contract only promises r >= x, r >= y,
  // and r == x || r == y, which does not pin m to 7.
};

Postconditions and preconditions work together. It is common to need a precondition in order to be able to prove a postcondition, and adding that precondition simultaneously rules out the calls for which the procedure would not behave as specified.