On B and Event-B: Principles, Success and Challenges, J.-R. Abrial
Abrial, JR. (2018). On B and Event-B: Principles, Success and Challenges. In: Butler, M., Raschke, A., Hoang, T., Reichl, K. (eds) Abstract State Machines, Alloy, B, TLA, VDM, and Z. ABZ 2018. Lecture Notes in Computer Science(), vol 10817. Springer, Cham. https://doi.org/10.1007/978-3-319-91271-4_3
" 2.1 Differences
One of the main differences between B and Event-B concerns operations (in B)
and events (in Event-B). Each operation in B is usually defined together with a
pre-condition containing a predicate that must be true for the operation to be
able to be called. On the other hand, each event in Event-B is usually defined
together with a guard containing a predicate that must be true for the event to
be able to occur.
2
This results in having both pre-conditions or guards being assumptions when
doing a proof on an operation or on an event (e.g. invariant preservation proofs).
So far thus, there are no differences between the two. However, both differs
strongly when dealing with refinement: pre-conditions can be weakened only,
whereas guards can be strengthened only. This possibility of guard strengthen-
ing is particularly important as it allows users to build models starting from
very abstract cases down to more realistic ones.
In fact, proof obligations are far simpler for events than for operations. In
the case of operations one has always two rules: one for pre-conditions and one
for post-conditions. In the case of event, one has always a single rule.
Another important distinction between the two concerns parameters. In the
case of an operation, such parameters cannot be refined, whereas event param-
eters can be freely refined (removed, added or modified).
Basic sets, constants and their properties are handled differently in B and
Event B. In B, basic sets, constants and their properties are defined in the ab-
stract machine where operations are defined. In Event-B, sets, constants and
their properties are defined in separate structures called contexts. This gives
users more flexibilities in Event-B than in B.
Event-B does not contain any programming constructs such as conditionals,
choices, sequencings or loops as B does. This greatly simplifies proof obligations
generated for Event-B with comparison to those generated for B. This simpli-
fication is particularly important in the case of sequencing. In fact, all such
constructs can be handled in Event-B by using events only. Of course, code gen-
eration is simpler in B because of the presence of such constructs. To do the
same in Event-B one has to apply some specific rules.
2.2 Similarities
Both B and Event-B use the mathematical notation of predicate calculus and
typed set theory. This means that proof obligations stated for both approaches
can be handled by similar provers. In fact, the prover of Atelier B (called PP) is
used successfully in the Rodin toolset. Other external provers (e.g. SMT provers)
are used in both Atelier B and Rodin.
In both cases, there is a notion of machine acting as an encapsulation for
operations (in B) or events (in Event-B). However there is an importante dis-
tinction between the two. The list of input-output definitions of the operations
of a B machine (its signature) is fixed once and for all, although it is not the
case for the events of an Event-B machine. Notice that events have no output
parameters. But there are more: such a list of events can be further extended
with new events in a refinement. This very important feature has been borrowed
from Action Systems [6]. It allows users to be very flexible in the gradual con-
struction (with refinement) of an event system.
In fact such similarities allows one to use Event-B within the Atelier B tool
which is used for B. Some proof obligations which are specific to Event-B have
been developed for that purpose in B. "
Comments
Post a Comment