5.3. Old🔗

In a postcondition you often want to relate the state when the procedure returns to the state when it was entered. Wrapping an expression in old(...) evaluates that expression in the pre-state — the heap as it was on entry. This is the standard way to specify a procedure that mutates its arguments.

composite Cell {
  var value: int
}

procedure bumpCell(c: Cell)
  opaque
  ensures c#value == old(c#value) + 1
  modifies c
{
  c#value := c#value + 1
};

Here c#value denotes the value on return and old(c#value) the value on entry, so the postcondition says the field grew by exactly one. Without old, the clause would read c#value == c#value + 1, which no implementation can satisfy.

old distributes through the structure of an expression, so you can wrap a whole sub-expression: old(2 * c#value + 3) means the same as 2 * old(c#value) + 3. It may also appear inside quantifiers and conditionals in a postcondition:

composite Cell { var value: int }

procedure strictBump(c: Cell)
  opaque
  ensures forall(other: Cell) => other == c ==> other#value > old(other#value)
  modifies c
{
  c#value := c#value + 1
};

A caller can reproduce the two-state reasoning by snapshotting the pre-state into a local variable before the call and asserting against it afterwards:

composite Cell { var value: int }

procedure bumpCell(c: Cell)
  opaque
  ensures c#value == old(c#value) + 1
  modifies c
{
  c#value := c#value + 1
};

procedure bumpCellCaller()
  opaque
{
  var c: Cell := new Cell;
  var pre: int := c#value;
  bumpCell(c);
  assert c#value == pre + 1
};

An old(...) that mentions nothing from the heap has no effect and Laurel warns about it, since it cannot relate two states. The same warning is issued for a redundant old(old(...)), whose inner old is dropped.