Expressing Behaviours as Properties

Where an expected behaviour is intimately concerned with more than one method call, then instead of expressing it as a post-assertion attached to one of the methods, it is better to express it in a property declaration.

Let's look at another expected behaviour of operators in the Money class. We declared operators for adding another Money object and for multiplying and dividing by integers. As a check on the correctness of our specifications, let's declare our expectation that adding a Money object to itself is equivalent to multiplying it by two. We could declare this as a post-assertion on the declaration of "+" like this:

Or, we could instead attach a post-assertion to the declaration of "*" like this:

However, this behavior involves both operators to a similar degree, so rather than use a post-assertion, it is more appropriate to declare a property within the interface section of class Money like this:

Not only is this more symmetrical in its treatment of the "+" and "*" operators, it is also simpler to express.

Let's take another example. If we multiply a Money object by an integer, then divide the result by the same integer, we expect to get back to our original value. We can express this as follows:

By declaring a parameter n of type nat, we are stating that the behavior should be true for all values of n (as well as for all legal values of self). However, we must exclude zero, since the precondition of our "/" operator requires that its second operand is nonzero; hence we give the property a precondition.

Properties don't have to be declared within classes - you can declare global properties too (of course, in a global property there is no self object to refer to). Here is a global property that states that our two different "*" operators behave like each other with the operands reversed:

This could equally well be stated as a class member property thus:

End of Tutorials!!!!!!!!!