'forall' Postconditions

Sometimes it's useful to apply a postcondition to all elements of a collection. Let's suppose that you want to add 1 to all elements of a sequence of integers called array. You can do this using a forall postcondition:

forall i::0..<#array :- array[i]! + 1

This is very much like a forall expression, except that the ":-" symbol is followed by a postcondition instead of being followed by an expression. The meaning is that the bound variables (the single variable i in this case) take all values in the bound (all the indices of array in this case) and that the postcondition following ":-" is satisfied for all those values.

So, the above is equivalent to combining the postconditions:

array[0]! + 1, array[1]! + 1, array[2]! + 1, ... , array[<#array]! + 1

Notionally, all the "branches" are satisfied in parallel.

It is required that the postcondition following ":-" has a distinct frame for each value of the bound variable (or each combination of the values of the bound variables, if there is more than one). This means that you can't use a postcondition such as:

forall i::0..<#array :- total! + array[i]

because total is part of the frame irrespective of the value of i. In practice, forall postconditions are almost always used to update sequences.

Next: Combining postconditions