Rodin Handbook





 

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.