Refinement, decomposition, and instantiation of discrete models: Application to Event-B (Jean-Raymond Abrial)
Refinement, Decomposition and Instantiation of Discrete Models
Jean-Raymond Abrial
ETHZ Zurich, Switzerland
jabrial@inf.ethz.ch
It is my belief that the people in charge of the development of large and complex computer systems must
adopt a point of view shared by all mature engineering disciplines, namely that of using an artifact to
reason about their future system during its construction. In these disciplines, people use blue-prints (in
the wider sense of the term) which allows them to reason formally during the very construction process.
Most of the time, in our discipline, we do not use such artifacts. This results in a very heavy testing
phase on the final product, which is well known to happen quite often too late. The blue-print drawing of
our discipline consists of building models of our future systems. But in no way is the model of a program
the program itself. For the simple reason that the model, like the blue-print, must not be executable:
you cannot drive the blue-print of a car. But the model of a program (and more generally of a complex
computer system), although not executable, allows you to clearly identify the properties of the future
system and to prove that they will be present in it.
Building models of large systems however is not an easy task. First of all because we lack experience
in this activity. Such a discipline does not exist per se in Academia, where quite often model building
is confused with using a very high level programming language where execution is thus still present.
Moreover, reasoning means ensuring that the properties which define the future system can be proved to
be consistent. As a matter of fact, doing a proof on a model replaces an impossible execution. But again,
the mastering of formal proving techniques has not entered yet the standard curriculum of our discipline.
As a consequence, people are quite reluctant to adopt such an approach, simply because they do not know
how to do it.
Another difficulty in model building, which is the one tackled in this paper, is due to the fact that
modeling a large and complex computer system results in a not surprisingly large and complex model. As
proofs will be our standard way to reason about our models, it is thus clear that such proofs will be more
and more difficult to perform as our model becomes inevitably larger and larger.
The aim of this paper
1
is to propose and study three techniques which might be useful to solve this
difficulty while building large models. As we shall see, these techniques are not new in that they are
already used in one way or another in certain programming methodologies, which is not very surprising.
The first one, refinement, is already well known for many years in program design although it is, in my
opinion, not used as it would deserve to be. The second one, decomposition, is also well known and quite
natural in the programming activity: when a computer program becomes too big, then cut it into smaller
pieces, which hopefully will be more tractable. The third one, generic instantiation, is also used in a
limited way in certain programming languages.
But, more interestingly, such techniques, although already present in various programming method-
ologies, are also heavily used in mathematics for mastering the complexity of large theories. Refinement
means that a proof in a certain domain is better first studied in a more abstract one where it will be easier to
perform. The proof will then later be refined to the more concrete case. Decomposition means that a large
proof is better decomposed in a series of little lemmas, which are eventually used in the main proof in a
structured manner (lemmas, needless to say, can also be reused in other different large proofs). Finally,
generic instantiation, is the usual way mathematics “works”: a general theory parameterized by carrier
sets and constants together with corresponding axioms, say group theory, is later used in another context
where the sets and constants are instantiated provided the instantiated axioms are themselves proved to [...]
1
This work has been partly supported by IST FP6 Rigorous Open Development Environment for Comple
Comments
Post a Comment