Postconditions

You've seen how we use postconditions to define the objects created by constructors, to define the changes made by a schema, and in after expressions to express the value that some expression would have if we made some changes to it. It's now time to cover postconditions in detail.

In Perfect, every postcondition precisely defines two things:

• A frame, which is a set of variables (or parts of variables) that may be changed; and
• A condition to be satisfied.

The most basic form of postcondition allows you to specify these two elements separately, like this:

for example:

expresses that the values x and array[i] are swapped and nothing else changes. In the condition, we use a prime to denote the final value of a variable (unprimed variables refer to the initial value). For each variable in the change list, that variable (or some variable containing it) must occur primed at least once in the satisfy expression.

Incidentally, array[i]' means exactly the same as array'[i] and so does self '.array[i] if array is an attribute of the current class.

It's very common to want to change a single variable by making its value equal to some expression; so we have a shorthand for this form. Specifically, any postcondition of the form:

can be abbreviated:

which is the sort of postcondition we've mainly used so far. Note that if you would need to bracket expr in the expression var' = (expr) - such as when expr is a forall, exists, for...yield or after expression, or expr contains a Boolean operator - then you also need to bracket expr in the postcondition var! = (expr).

A variation of the above is the postcondition

where operator is any binary operator. This may be abbreviated to:

So the postcondition

may be abbreviated to either

or to

Next:  More postconditions