## 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 |
## 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 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-useMost 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 ## 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 |