When writing specifications, it is helpful to have access to the values of the variables in the precondition state (i.e., when the function body has not run). In some specification languages, the precondition state is also referred to as the old state. Extend Speclang to add the ability to access precondition states by adding an old expression. An old expression must be used only within postconditions in a specification. An example appears here:

In this example, the postcondition states that the new value of the variable x is 1 greater than the old value of the variable x.