2.8.2 A Context with Colours

Start by creating a context called ctx1, as described in Section 2.6. We model the colours of the traffic light as a so-called “enumerated set” (3.3.4): We explicitly specify all elements (the three colours) of a new user-defined data type. We define the constants:

CONSTANTS

We introduce the new data type as a set:

SETS

And last, we need to provide typing of the constants. We do this by creating a partition (3.3.4.7):

AXIOMS

Please note the curly braces {} around the colours. It’s very easy to forget these, but if they are missing, typing errors will be displayed that are very hard for a novice to interpret.

This completes the context.