Combining Postconditions Sequentially

To combine postconditions sequentially, just write the keyword then between them;
for example:

has the same meaning as

In postcondition elements combined with then, a primed value refers to the final value in that particular element, not in the entire postcondition. So, in the following:

the final value of x is equal to e, not to e + 1.

It is good practice to avoid using then if the desired state change can be expressed in another way. A specification should express what a method achieves, not how it achieves it. The main reason for using then is to combine sequentially a schema call postcondition with another postcondition that affects the same variable(s). In this situation, avoiding use of then would involve replacing the schema call with the postcondition of the schema.

Combining postconditions with "&" has higher precedence than combining with then,
so:

means the same as:

When you combine postconditions using then, the resulting postcondition cannot be satisfied in parallel with any other postcondition. This means that you cannot use a then-combined postcondition in a list of more than one postcondition, nor can you use "&" to combine it with any other postcondition.
For example, the following are not permitted:

Next:  Bracketed postconditions