Combining Postconditions

There are four ways of combining postconditions:

• Combining with "&"
• Combining with then
• Bracketing without guards
• Bracketing with guards

To combine postconditions with "&", first put brackets around any change...satisfy or forall postconditions that you wish to combine; then write "&" between the postconditions.
For example, the following swaps the values of variables x and y:

Postconditions combined with "&" are satisfied in parallel, but where you prime a variable this refers to the final value of a variable in the entire combined postcondition, so you can make one of the component postconditions depend on a final value that is defined by another.
So, the postcondition:

sets both y and z to the value e, as does the postcondition:

since the order of postconditions combined using "&" is immaterial to the meaning.

The frames of postconditions combined with "&" must be disjoint, so:

is illegal, and:

is valid subject to i ~= j.

Next:  Combining postconditions sequentially