Schemas that modify their parameters

Schemas may be designed to modify their parameters instead of (or as well as) the current object.

For example, suppose we wish to change the outOfPrint schema so that as well as updating the set of available versions, it also returns the updated set to the caller. Here is a suitable schema declaration:

schema !outOfPrint(v: PublishedVersion, versionsLeft!: out set of PublishedVersion)
pre v in versions
post versions! = versions.remove(v), versionsLeft! = versions';

The new parameter versionsLeft is declared with an exclamation mark after its name to indicate that the schema can modify it. Furthermore, in this example the keyword out indicates that it is only used for passing a value out of the schema, so its initial value is unimportant. Indeed, the caller does not need to initialize it.

We have followed the post keyword by two postconditions separated by a comma. The meaning is that both postconditions are to be satisfied, but in no particular order. However, the prime after versions in the second postcondition means we want the final value of versions at that point; but the final value of versions is defined by the first postcondition, so in this case they will be satisfied in order.

When calling a schema that modifies its parameters, the corresponding actual parameters must be followed by an exclamation mark (thereby indicating at the point of call that the parameter is changed). For example:

... myBook!outOfPrint(hardback@PublishedVersion, left!) ...

where myFavoriteBook is a variable (or modifiable parameter) of type Book and left is a variable (or modifiable parameter) of type set of PublishedVersion.

Usually, it is unnecessary to use a schema that changes more than one object in an after expression, but it can be done. Since the postcondition that follows after is only allowed to change it, the expression you use in front of after needs to be a class with multiple modifiable components. If the schema modifies two objects, the library class pair of (X, Y) is convenient for this purpose:

... ( let temp ^= pair of (Book, set of PublishedVersion)
                     {myFavoriteBook, set of PublishedVersion{}};
      temp after it.x!publish(hardback@PublishedVersion, it.y!)
    )
...

or, more succinct (but possibly less readable):

... pair of (Book, set of PublishedVersion)
{myFavoriteBook, set of PublishedVersion{}}
after it.x!publish(hardback@PublishedVersion, it.y!)
...

Either way, the construct is an expression of type pair of (Book, set of PublishedVersion) whose x component represents the updated Book object and whose y component is the set of remaining versions.

Next: Postconditions