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 can only behave in a way that corresponds to the behavior of A. We will now look into more detail of what “corresponds” here means. In such a setting, we call A the abstract and B the concrete machine.

This is just overview over the concept of refinement. Later in Section 2.8 we will 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.

An event of the abstract machine may be refined by one or several events of the concrete machine. To ensure that the concrete machine does only what is allowed to do by the abstract one, we must prove two things:

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

• 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 hypotheses 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 occurrence of a modified variable is replaced by its new value. The hypotheses we use are:

• We assume that the invariant of both the concrete and abstract machines were valid 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 any invariants.

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

These two conditions are the central issues that we need to deal with to prove the correctness of a refinement. We now just explain a few common special cases.

2.7.4.1 Variable re-use

Most of the time, we do not want to replace all variables with 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 this 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 true and doesn’t need to be proven. We still have to prove 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 we are dealing with a refined 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 in which 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 a witness construct. 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 , where represents an expression that maps to . How this works in practice is shown in Section 2.8.5.