Conditional Postconditions

Conditional postconditions are constructed in an analogous way to conditional expressions; that is, a conditional postcondition is constructed by enclosing two or more guarded postconditions in brackets.

To illustrate this, let's return to our Book example. Suppose we wish to associate a list price with each version in which a book is published. Leaving aside for the moment how we store this data, let's assume we want a schema to adjust the price of a particular published version by a given percentage. We could make it a precondition of the schema that the specified version is included in the published versions; but instead, let's define the schema to ignore the call if the specified version is not available. This is what such a schema might look like:

As in a conditional expression, the empty guard "[]:" means "else". In fact, the combination "[]: pass" is required so often that Perfect has a special shorthand for it which is to omit the colon and pass keyword, like this:

The first guard may be preceded by let-declarations, assertions and variable declarations in the usual way, e.g.:

We've now covered all the important forms of postcondition supported in Perfect.

Well done: you have reached the end of the tutorials on the basics of Perfect Developer

Next:  Intermediate tutorial