Rodin HandbookThis work is sponsored by the Deploy Project This work is sponsored by the ADVANCE Project This work is licensed under a Creative Commons Attribution 3.0 Unported License 
3.2.4 MachinesA machine describes the dynamic behavior of a model by means of variables whose values are changed by events. There are two basic things that must be proven for a machine:
3.2.4.1 Refinement and Abstract machinesA machine can refine at most one other machine. We refer to the refined machine as the abstract machine and refer to the refinement as the concrete machine. More generally, a machine can be refined by machine , refined by and so on. The most concrete refinement would be . Basically, a refinement consists of two aspects:
The full invariant of the machine consists of both abstract and concrete invariants. The invariants are accumulated during refinements.
3.2.4.2 Seeing a contextIf the machine sees a context, the sets and constants declared in the context can be used in all predicates and expressions. The conjunction of axioms can be used as hypotheses in the proofs. 3.2.4.3 Variables and invariantsVariables can be declared by adding their unique name (an identifier) to the Variables section. The type of the variables must be inferable by the invariants of the machine. We denote the variables of the abstract machines with a and the variables of the concrete machine with a . An invariant is a statement that must be valid at each state of the machine. Each invariant consists of a label and a predicate . An invariant can refer to the constants as well as the variables of the concrete and all abstract machines. We write to denote the conjunction of all invariants of the abstract machines and for the conjunction of the concrete machine’s invariant. Invariants that are marked as theorems derive their correctness from the preservation of other invariants, so their preservation does not need to be proven. The proof obligation can be found in Section 3.2.6.2. If an invariant contains a welldefinedness condition, a corresponding proof obligation is generated (3.2.5.2). 3.2.4.3.1 Common variables between machinesWith some restrictions, the abstract variables and concrete variables can have variables in common. If a variable is declared in a machine , it can be reused in the direct refinement . In that case, it is assumed that the values of the abstract and concrete variable are always equal. To ensure this, special proof obligations are generated (3.2.4.4). Once a variable disappears in a refinement, i.e. it is not declared in machine , it cannot be reintroduced in a later refinement. 3.2.4.4 EventsA possible state change for a machine is defined by an event. The condition under which an event can be executed is given by a guard. The event’s action describes how the new and old state relate to each other. Events occur atomically (i.e. one event happens at a time) and to a new state. Two events never happen at the same time. Time is also not factored into the execution of the event. An event has the following elements:
An event can refine one or more events of an abstract machine. To keep things simple, we will first consider events with only one refined event. If there are several refinement steps, we describe events from the refined machines as abstract events and the event from the concrete machine as the concrete event. For example, if an event is refined by and is refined by , we call and the abstract events and the concrete event. Likewise, if we refer to the parameters of the abstract events, we mean all the parameters of all the abstract events (e.g., the parameters of and ). 3.2.4.4.1 ParametersAn event can have an arbitrary number of parameters. Their names must be unique, i.e. there must be no constant or variable with the same name. The types of the parameters must be declared in the guards of the event. We denote the parameters of all abstract events with and the parameters of the concrete event with . Similarly to variables, an event can have parameters in common with the event it refines. If the refined event has a parameter which is not a parameter of the refinement, a witness for the abstract parameter must be specified (3.2.4.4.4). All free identifiers in must be either constants, concrete or abstract variables, concrete parameters or the abstract parameter . 3.2.4.4.2 GuardsEach guard consist of a label and a predicate . All free identifiers in must be constants, concrete variables or concrete parameters. Variables or parameters of abstract machines are not accessible in a guard. We write for the conjunction of all guards of all abstract events. Like axioms and invariants, guards can also be marked as theorems. The proof obligation can be found in Section 3.2.6.3. If the guard contains WDconditions, a proof obligation is generated. See Section 3.2.5.3 for the proof obligation. 3.2.4.4.3 ActionsAn action is composed of a label and an assignment. Section 3.3.8 gives an overview of how they are assigned. They can be put into two groups: deterministic and nondeterministic assignments. Each assignment affects one or more concrete variables. If an event has more than one action, they are executed in parallel. An error will occur if a new value is assigned to a variable in more than one action. All variables to which no new value is assigned keep the same value in new and old state. We now define the beforeafterpredicate of the actions together. Let be the beforeafterpredicate of the event’s assignments. Let be the variables that are assigned by any action of the event. Let be the variables of the concrete machine that are not modified by any of the event’s actions (i.e. ). Then the beforeafterpredicate of the concrete event is . Please note that Rodin optimizes proof obligations when a beforeafterpredicate is a hypothesis. is replaced directly by when is not changed by the event and replaced by when is assigned to deterministically. 3.2.4.4.4 WitnessesWitnesses are composed of a label and a predicate that establishes a link between the values of the variables and parameters of the concrete and abstract events. Most of the time, this predicate is a simple equality.
If the user does not specify a witness, Rodin uses the default witness . Witnesses are necessary in the following circumstances:
We denote the conjunction of all witnesses of an event with . The feasibility of the witness must be proven, i.e. that there is actually a value for which the predicate holds.
A witness may contain welldefinedness conditions. See 3.2.5.4 for the corresponding proof obligation. 3.2.4.4.5 InitialisationThe initialisation of a machine is given by a special event called INITIALISATION. Unlike other events, the initialisation must not contain guards and parameters. The actions must not make use of variable values before the initialisation event occurs. All variables must have a value assigned to them. If there is no assignment for the variable , Rodin assumes a default assignment of the form . 3.2.4.4.6 Ensuring machine consistencyThe following proof obligations are generated for events: The assignment of each action must be welldefined when the event is enabled. See 3.2.5.5 for the corresponding proof obligation. If the event’s guard is enabled, every action must be feasible. This is trivially true in the case of the deterministic assignments. For a nondeterministic assignment , the feasibility must be proven. The feasibility operator is described in Section 3.3.8.
For each invariant with the label invlabel that contains a variable affected by the assignment, it must be proven that the invariant still is still valid for the new values.
Rodin simplifies this proof obligations by replacing with for variables that are not changed and by for variables that are assigned by a deterministic () assignment. There are special proof obligations generated for the initialisation event:
3.2.4.5 Ensuring a correct refinementAn event can refine one or more events of the abstract machine. We first consider the refinement of only one event. For refining more than one event (i.e. merging events), please refer below to Section 3.2.4.6. If an event does not refine an abstract event, it is implicitly assumed that it refines skip, the event that is always enabled (i.e. its guard is ) and does nothing (i.e. all variables keep their values). 3.2.4.5.1 Guard strengtheningA concrete event must only be enabled if the abstract event is enabled. This condition is called guard strengthening. For each abstract guard with label guardlabel, the following proof obligation is generated:
3.2.4.5.2 Action simulationIf an abstract event’s action (with beforeafter predicate ) assigns a value to a variable that is also declared in the concrete machine, it must be proven that the abstract event’s behaviour corresponds to the concrete behaviour. The behaviour of the concrete event is given by the concrete beforeafterpredicate , and the relevant abstract behaviour is given by the beforeafterpredicate . The relation between abstract and concrete event is specified by witnesses.
When the assignments are deterministic or the witnesses are equations, the proof obligation can usually be simplified by Rodin. 3.2.4.5.3 Preserved variablesIf is a variable of both the abstract and concrete machine and the concrete event assigns a value to but the abstract event does not, it must be proven that the variable’s value does not change. Let be the beforeafterpredicate of the action that changes .
3.2.4.6 Merging eventsRefining more than one abstract event by a single event is called merging of events. To merge events, two conditions must be taken into account.
Instead of the guard strengthening proof obligation, the following proof obligation is created with as the abstract guards of the merged events and as their parameters.
The other proof obligations are the same as for refining a single event. Also, the same rules for defining witnesses apply. 3.2.4.7 Extending eventsInstead of refining another event, an event can extend it. In this case the refined event will implicitly have all the parameters, guards and actions of the refined event. It can have additional parameters, guards and actions. The same effect can be achieved by manually copying the parameters, guards and actions. This is especially useful when additional features are gradually introduced into a model by refinement (also called “superposition refinement”). 3.2.4.8 TerminationEventB makes it possible to prove how an event will terminate. Termination means that a chosen set of events are enabled only a finite number of times before an event that is not marked as terminating occurs. To support proofs for termination, a variant can be specified in a model. All free identifiers in must be constants or concrete variables. A variant is an expression that is either numeric () or a finite set (, where is an arbitrary type). Events can be marked as:
Informally, termination is proven by stating that the convergent events strictly decrease the variant which has a lower bound. If a model contains a convergent event, a variant must be specified. If only anticipated events are declared, it is sufficient to create a default constant variant so that all anticipated events do not increase the variant. When an event is marked as anticipated, one must just prove that the event does not increase the variant. The proof of termination is then delayed to the refinements of the anticipated event. A refinement of an anticipated event must be either anticipated or convergent. If the convergence of an event is proven, the convergence of its refinements is also guaranteed due to guard strengthening. A variant must be welldefined. The corresponding welldefinedness proof obligations can be found in Section 3.2.5.6. The following other proof obligations are generated: 3.2.4.8.1 Numeric variantIf the variant is numeric, an anticipated or convergent event must only be enabled when the variant is nonnegative.
A convergent event must decrease the variant
and an anticipated event must not increase the variant.
3.2.4.8.2 Set variantIf the variant is a set t, it must be proven that the set is always finite:
A convergent event must remove elements from the set
and an anticipated event must not add elements.
