More Postconditions

To recap, we've just covered three sorts of postconditions:

• change frame satisfy condition
• var! = expr
• var! op expr

Now to look at two more sorts of postcondition:

• schema calls
• pass

The call:

means the following:
satisfy the postcondition of the schema outOfPrint, substituting myBook for self, hardback@PublishedVersion for the parameter v, and left for the parameter versionsLeft.

For purists: the frame of a schema call postcondition is, basically, the variables that are followed by exclamation marks (including the implicit self if self!s is abbreviated to !s), but may be narrowed to just parts of those variables (since the frame of the schema postcondition may be confined to just some parts of the variables that the schema is allowed to modify). The condition of a schema call postcondition comprises the condition of the postcondition of the schema (with appropriate parameter substitutions).
As an example, the above schema call is equivalent to

(except that the expanded version would be illegal unless the versions attribute of class Book were declared publicly writable). If the above sounds a little complicated, don't worry - expanding schema calls into frames and conditions is a job for Perfect Developer : you needn't do it!

The other simple form of postcondition pass has an empty frame and satisfies the condition true. In other words, pass represents "no change".

We've now covered five types of simple postcondition, namely:

• change frame satisfy condition
• var! = expr
• var! op expr
• schema call
• pass

Next:  Applying a postcondition to all elements of a collection