Anatomy of a Context (Rodin User Manual)

From Event-B

1 Carrier Sets
- 1.1 Carrier Sets Creation Wizard.
- 1.2 Direct Editing of Carrier Sets.
2 Enumerated Sets
3 Constants
- 3.1 Constants Creation Wizard.
- 3.2 Direct Editing of Constants.
4 Axioms
- 4.1 Axioms Creation Wizard.
- 4.2 Direct Editing of Axioms.
5 Adding Comments
6 Dependencies
7 Pretty Print
8 Synthesis

Once a context is created, a window such as the following appears in the editing area (usually next to the center of the screen):

You are in the "Edit" area allowing you to edit pieces of the context, namely dependencies (keyword "EXTENDS"), carrier sets (keyword "SETS"), constants (keyword "CONSTANTS"), or axioms (keyword "AXIOMS"). By pressing the triangle next to each keyword, you can add, remove, or move corresponding modelling elements. As an example, here is what you obtain after pressing the triangle next to the keyword "AXIOMS":

By pressing the

button, you obtain the following:

You can now enter a new axiom and a comment in the corresponding boxes as indicated below:

You can add another axiom in a similar fashion:

For removing an axiom, press the

button. You can also move an axiom up or down by selecting it (press mouse left key when situated on the axiom logo) and then pressing one of the two arrows:

. Other modelling elements are created in a similar fashion.

It is also possible to do so in a different way as explained in sections 2.1 to 2.7. The creation of these elements, except dependencies (studied in section 2.7), can be made by two distinct methods, either by using wizards or by editing them directly. In each section, we shall review both methods. NOTE: The hurried reader can skip these sections and go directly to section 2.8

Carrier Sets

Carrier Sets Creation Wizard.

In order to activate the carrier set creation wizard, you have to press the

button in the toolbar as indicated below:

After pressing that button, the following wizard pops up:

You can enter as many carrier sets as you want by pressing More. When you’re finished, press the OK.

Direct Editing of Carrier Sets.

It is also possible to create (Add) or remove (Delete) carrier sets by using the central editing window (see window below). For this, you have first to select the "Carrier Sets" tab of the editor. Notice that you can change the order of carrier sets: first select the carrier set and then press button Up or Down.

As can be seen, we have created three carrier sets $C$ , $E$ , and $D$ .

Enumerated Sets

In order to activate the enumerated set creation wizard, you have to press the

button in the toolbar as indicated below:

After pressing that button, the following wizard pops up:

You can enter the name of the new enumerated set as well as the name of its elements. By pressing More Elements, you can enter additional elements. When you’re finished, press the OK. The effect of using this wizard as indicated is to add the new carrier set $C O L O R$ (section 2.1) and the three constants (section 2.3) $r e d$ , $g r e e n$ , and $o r a n g e$ . Finally, it adds the following axiom (section 2.4):

$\operatorname{partition}(COLOR , \{red\}, \{green\}, \{orange\})$

If you enter several time the same enumerated set element, you get an error message.

Constants

Constants Creation Wizard.

In order to activate the constants creation wizard, you have to press the

button in the toolbar as indicated below:

After pressing that button, the following wizard pops up:

You can then enter the names of the constants, and an axiom which can be used to define its type. Here is an example:

By pressing {{button|More Axm.} button you can enter additional axioms. For adding more constants, press Add. When you’re finished, press OK.

Direct Editing of Constants.

It is also possible to create (Add) or remove (Delete) constants by using the central editing window. For this, you have first to select the "Constants" tab of the editor. You can also change the relative place of a constant: first select it and then press Up or Down.

As can be seen, two more constants, $b i t 1$ and $b i t 2$ have been added. Note that this time the axioms concerning these constants have to be added directly (see next section 2.4).

Axioms

Axioms Creation Wizard.

In order to activate the axioms creation wizard, you have to press the

button in the toolbar as indicated below:

After pressing that button, the following wizard appears:

You can then enter the axioms you want. If more axioms are needed then press More. When you are finished, press OK.

The "Theorem" checkbox indicates whether the corresponding axiom is a theorem. If checked, a Proof Obligation will be generated for this predicate. This mechanism replaces the older one (before Rodin 1.0), in which there used to be separate entries for axioms on one hand (w/o PO) and theorems on the other hand (with PO). So now, there remains only axioms, which may or may not be theorems.

Direct Editing of Axioms.

It is also possible to create (Add) or remove (Delete) axioms by using the central editing window. For this, you have first to select the "Axioms" tab of the editor. You can also change the relative place of an axiom: first select it and then press Up or Down.

Note that the Up and Down buttons for changing the order of axioms are important for well-definedness. For example the following axioms in that order

$\begin{array}{l} \hbox{axm1}: y/x=3 \\ \hbox{axm2}: x \neq 0 \end{array}$

does not allow to prove the well-definedness of $y / x = 3$ . The order must be changed to the following:

$\begin{array}{l} \hbox{axm2}: x \neq 0 \\ \hbox{axm1}: y/x=3 \end{array}$

The same remark applies to invariants (section 3.3) and event guards (section 3.3.2)

Adding Comments

It is possible to add comments to carrier sets, constants, axioms and theorems. For doing so, select the corresponding modeling element and enter the "Properties" window as indicated below where it is shown how to add comments on a certain axiom:

Multiline comments can be added in the editing area labeled "Comments".

Dependencies

By selecting the "Dependencies" tab of the editor, you obtain the following window:

This allows you to express that the current context is extending other contexts of the current project. In order to add the name of the context you want to extend, use the combobox which appears at the bottom of the window and then select the corresponding context name.

There exists another way to directly create a new context extending an existing context $C$ . Select the context $C$ in the project window, then press the right mouse key, you’ll get the following menu:

After pressing Extend, the following wizard pops up:

You can then enter the name of the new context which will be made automatically an extension of $C$ .

Pretty Print

By selecting the "Pretty Print" tab, you may have a global view of your context as if it would have been entered through an input text file.

Synthesis

By selecting the "Synthesis" tab, you may have a global view of your context's elements (carrier set/constant/axiom/extended context).

After pressing set (respectively cst or axm), you can filter carrier sets of your context (respectively constants or axioms).

If you select for example an axiom, you can change its priority order by pressing or . You can do the same for carrier sets, constants or extended contexts.