Rodin User’s Handbook v.2.8: A Context with Colours

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:

$\includegraphics[width=7mm]{img/pencil_64.png}$

CONSTANTS

$\tt red$

$\tt yellow$

$\tt green$

We introduce the new data type as a set:

$\includegraphics[width=7mm]{img/pencil_64.png}$

SETS

$\tt COLOURS$

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

$\includegraphics[width=7mm]{img/pencil_64.png}$

AXIOMS

$\tt type :$

$\it partition(COLOURS, \{ red\} , \{ yellow\} , \{ green\} )$

$\includegraphics[width=7mm]{img/warning_64.png}$
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.