• Handbook Home
• Feedback
• Email Feedback
• Handbook as PDF
• Rodin Wiki
• Rodin Download
• Contact

Refinement

User Manual for Rodin v.2.3

Feedback

2.7.4 Refinement

Refinement is a central concept in Event-B. Refinements are used to gradually introduce the details and complexity into a model. If a machine B refines a machine A, B is only allowed to behave in a way that corresponds to the behavior of A. We now look into more detail of what “corresponds” here means. In such a setting, we call A the abstract and B the concrete machine.

Here we give just a brief overview over the concept of refinement. Later in Section 2.8 we use refinement in an example.

The concrete machine has its own set of variables. Its invariants can refer to the variables of the concrete and the abstract machine. If a invariant refers to both, we call it a “gluing invariant”. The gluing invariants are used to relate the states between the concrete and abstract machines.

The events of a concrete machine can now refine an abstract event. To ensure that the concrete machine does only what is allowed by the abstract one, we must show two things:

• The concrete events can only occur when the abstract one can occur.

• If a concrete event occurs, the abstract event can occur in such a way that the resulting states correspond again, i.e. the gluing invariant remains true.

The first condition is called “guard strengthening”. The resulting proof obligation has the label concrete_event/abstract_guard/GRD. We have to prove that under the assumption that the concrete event is enabled (i.e. its guard are true) and the invariants (both the abstract and the concrete) hold, the abstract guards holds as well. Thus the goal is to prove that the abstract guard, the invariants and the concrete guards can be used as hypothesis in the proof.

The second condition, that the gluing invariant remains true, is just a more general case of the proof obligation which ensures that an event does not violate the invariant. So the proof obligation’s label is again concrete_event/concrete_invariant/INV. The goal is to prove that the invariant of the concrete machine is valid when each occurence of a modified variable is replaced by its new value. The hypotheses we can use are:

• We assume that the invariant of both the concrete and abstract machines hold before the event occurred.

• The abstract invariants where the modified variables are replaced by their new values are valid because we know that the abstract event does not violate the invariants.

• The event occurs only when the guards of both the concrete and abstract machines are true.

These two conditions are the central piece to prove the correctness of a refinement. We now just explain a few common special cases.

2.7.4.1 Variable re-use

Most often, we do not want replace all variables by new ones. It is sometimes useful to keep all of the variables. We can do this just by repeating the names of the abstract variables in the variable section of the concrete machine. In that case, we must prove for each concrete event that changes such a variable that the corresponding abstract event updates the variable in the same way. The proof obligation has the name concrete_event/abstract_action/SIM.

2.7.4.2 Introducing new events

An event in the concrete machine might not refine any event in the abstract machine. In that case it is assumed to refine skip, which is the event that does nothing and can occur any time. The guard strengthening is then trivially true and doesn’t need to be proven. It still must be proven that the gluing invariant holds but this time under the assumption that the abstract machine’s variables have not changed. Therefore, the new state of our newly introduced event corresponds to the same state of our abstract machine from before the event happened.

2.7.4.3 Witnesses

Let’s consider a situation where we have an abstract event with a parameter and in a refining event that no longer needs that parameter. We saw above that we have to prove that for each concrete event the abstract event may act accordingly. With the parameter, however, we now have the situation that we must prove the existence of a value for such that an abstract event exists. Proofs with existential quantification are often hard to do, so Event-b uses the construct of a witness. A witness is just a predicate of the abstract parameter with the name of the variable as label. Often a witness has just the simple form .