Mappings

The Book example, continued from the basic tutorials, as we left it:

Currently, each Book object holds a set of PublishedVersion indicating what versions are available (paperback, hardback etc.). Our task is to associate a price with each version. Let's assume we will define a class Money to represents monetary amounts.

To relate prices to versions, one possibility is to define a new class VersionAndPrice to hold both a PublishedVersion and a Money object, then our versions attribute can hold a set of values of this class. However, since each version has exactly one price, we would need an invariant or type constraint to restrict versions to contain no more than one VersionAndPrice value for any PublishedVersion, like this:

(where the ver attribute of VersionsAndPrice is assumed to be the PublishedVersion).

If we wished to avoid declaring a new class solely to store a version and a price, we could, at some loss of readability, use the predefined template class pair instead, like this:

(the first component of a pair is called x so in this case it is the PublishedVersion part).

A simpler way of representing this data is to use the "map of (X -> Y)" class. This represents a set of values of type X, with a value of type Y associated with each value in the set. So the following declaration:

captures precisely what we need. Note that each PublishedVersion has exactly one associated Money value (i.e. one price), but there is nothing to stop several versions having the same price.

If we define versions like this, we can use it in the following ways. First, if we want to determine all the available published versions in the mapping, we can do so using the dom method (short for "domain"), like this:

Likewise, we can obtain all the prices using the ran method (short for "range"), e.g.:

To test if a particular PublishedVersion called ver is in the mapping, we could use the expression ver in versions.dom but the expression ver in versions means exactly the same thing, and it is shorter.

To lookup the price of a PublishedVersion called ver that is known to be in the mapping, we can use the expression versions[ver], which is rather like indexing into a sequence. In fact, a sequence can be considered as a particular type of mapping in which the domain comprises the set of integers from zero to one less than the length of the sequence.

We can also use indexing to modify an element of a mapping, as in the postcondition versions[ver]! = newPrice.

Armed with this, we can now complete the specification of the adjustPrice schema:

assuming that class Money provides operators for multiplying and dividing by integers. We'll look at how to do this next.

Next:  Operator declarations