Bracketed Postconditions

Just as in expressions, brackets can be used with postconditions to override the usual precedence rules.
For example, in:

(forall i::1..<#s :- s[i]! + 1) & s[0]! = 0

brackets are used around the 'forall' postcondition in order to allow it to be combined with another postcondition using "&".

However, brackets can do far more than that. First, a list of postconditions may be used in place of a single postcondition by bracketing.
For example, the postcondition:

(forall i::1..<#s :- s[i]! + 1, s[0]! = 0)

is equivalent to the one given earlier on this page. This is because postconditions in a list are satisfied in parallel, just as if they were combined using "&".

Second, between the opening bracket and the start of the postcondition list, it is permitted to place let-declarations and assertions (just as in bracketed expressions). It is also possible to declare variables here. This is especially useful when calling a schema with a out parameter, since a local variable declaration can be used to capture the returned value.
For example:

(var temp: int; !doSomething(temp!) then x! = f(temp))

where schema doSomething modifies the current object and also returns a value in its out parameter.

Lastly, brackets are used to build conditional postconditions in much the same way as conditional expressions are constructed, as you can see next.

Next: Conditional postconditions