On B, Jean-Raymond Abrial

 Cet article date du temps où Jean-Raymond Abrial habitait rue des plantes à Paris. Digilog était deveni Steria, mais pas encore Clearsy. Donc d'avant 2001.

On B

Jean-Raymond Abrial

Consultant,

26, rue des Plantes, 75014, Paris.

abrial@steria.fr

In the B-Book [Abr96], an introduction entitled “What is B ?” presents it in a few pages. There is no point in reproducing this introduction here. There is, however, clearly a need to have in this book a sort of informal presentation of B complementing that of the B-Book for those readers who are not familiar with this approach. This is the purpose of this short text, where the emphasis will be put on the question of the development process with B. At the end of the text, I will also cover some more general problems concerning B (tool, education, research, future).

B is o “Debugger”.

The aim of B is very practical. Its ambition is to provide to industrial prac- titioners a series of techniques for helping them in the construction of software systems. As everyone knows, the complexity of such systems, as well as the con- text within which they are developed makes them very prone to errors. Within this framework, the goal of B is to accompany the system development process in such a way that the inevitable errors, produced either during the technical specification phase, or the design phase, or, of course, during the coding phase, that all these errors are trapped as soon os they are produced. In a sense, from that point of view, B is nothing else but a generalized debugging technology.

Classical Debupginp Techniques or Based on Execution.

In classical software developments, errors are usually (but partially) discov- ered, and hopefully corrected, after the coding phase: this is done by checking the final product (or better, some parts of it) against a variety of tests supposed to cover the widest range of behaviors. Another technique, which becomes very popular these days, is that of modef checking by which it is shown that the final system satisfies certain properties: this is done by an exhaustive search under all possible executions of the program.

As can be seen, both techniques, testing and model checking, work on the final product and are based on some “laboratory” ececution of it. Since we be- lieve in the great importance of trapping errors as soon as they are produced, it is clear that such techniques cannot be used during the technical specification and the design phases, where no execution can take place.

The B Debugging Technique is Based on Proofs. Conceptuol Difficulties.

The debugging technology, which is proposed by B, is thus not based on execution, it is rather based on mothematical proofs. This apparently simple ap- proach, which is widely used in other engineering disciplines, poses a number of specific problems.

When execution is the criterion, the developer obviously tends to write his formal text (his program) with execution in mind. He reasons in terms of data that are modified by some actions (assignments), and he constructs his program by means of a number of operations on such actions: conditionals, sequencing, loop, procedure calls, etc.

With B, the developer (at least, in the early phases) is not supposed to rea- son in terms of execution. Since the basic paradigm is that of proof, he has to think directly in terms of properties that have to be satisfied by the future system. This shift from execution to properties and proofs constitutes, in fact, a great step, which could sometimes represent an insurmountable difficulty to some persons. In our experience, it is not so much the manipulation of well de- fined mathematical concepts (sets, relations, functions, numbers, sequences, etc) that poses a serious problem to certain B practitioners, it is rather the neces- sary change of habit consisting in abandoning (for a while) the idea of execution.

Necessity of Re-writing the Requirement Documents.

As a matter of fact, some B novices use it as if it were a programming language with the classical concepts of discrete mathematics directly at their disposal. From our point of view, it is a mistake. We must say, however, that people are inclined to do so, since the informal requirements of the system they realize are often also written with execution in mind. Very often indeed, such requirements are already written in the form of a pseudo-implementation de- scribing the future system in terms of data and algorithms acting on them.

This is the reason why, in our opinion, it is almost always indispensable, before engaging in any development with B, to spend a significant time (that is, for a large system, several months) to just rewrite these requirements in english, say, so as to re-orient them towards the precise statements of the properties of the future system. The natural language statements, the diagrams, or the tables describing these properties in one form or another must be identified, isolated and labeled in order to clearly separate them from the rest of the text (hyper- text technology and “literate programming” helps here).

Such properties may concern either the static aspect of the system (that is, the permanent properties of its data), or its dynamic aspect (that is, the prop- erties expressing how the data are allowed to evolve).

Obviously, such a rewriting should be performed hand in hand with the “client” , who has to give his final agreement so that this second text becomes the new contractual basis of the future development.

Extracting Some Properties from the Requirement Documents.

Once this is done, the work of the B practitioner is to transcribe such infor- mally stated properties into mathematical models. This has to be done gradually. It is out of the question to do this in a flat manner. One has first to extract from the informal text a few very fundamental properties that are the expression of the essence of the system.

The corresponding model takes the form of a, so-called, abstract machine, which encapsulates some variables whose types and static properties are formal- ized within a, so-called, invariant clause. These variables often denote some very abstract concepts related to the problem at hand. This is the reason why they are quite naturally “encoded” by equally abstract mathematical objects such as those mentioned above (sets, and the like).

The dynamics of the model is defined by a number of, so-called, operations, formalized as predicate transformers, called in B generalized substitution. Usu- ally, at the top level, such operations are very straightforward: they take the form of a pre-condition followed by a simple, often highly non-deterministic, ac- tion defined on all (or part of) the variables at once (no sequencing, no loop). At this point, a first series of proofs must be performed in order to show that the static properties of the variables are indeed preserved by the operations. It constitutes a first form of debugging of the original informal text. Note that the requirement properties that have been chosen must be referenced. In this way, an easy navigation from the informal statements of these properties to their first formal setting counterparts is indeed possible.

Refinement as a Technique Jor Extracting more Details oJ the Problem.

Our first mathematical model is then refined, but still with properties and proofs in mind, not yet execution. It is done by extracting more properties from the informal specification in order to incorporate them in the model (without forgetting to reference them as above). Another set of proofs has then to be per- formed in order to certify that the extended model is itself coherent and, above all, that it is not contradictory with its abstraction (debugging continues). This extended model itself is then refined (that is, more properties are extracted) and more proofs are done, etc.

The Technique of Model Decomposition.

The process of refinement mentioned above can be complemented by that of decomposition. By this, we mean the splitting of a (possibly refined) model into several sub-models, which are then themselves refined and possibly decomposed independently, and so on. Such sub-models are said to be imported in their par- ent model.

Architecture Construction.

Note that in doing so (refinement and decomposition), the orchitecture of our future system is gradually emerging. It is interesting to note that it is realized solely in terms of the successive extractions of the properties of the system from within the informal requirements.

Refinement as a Technique for Transforming Models into Modules.

When all the original properties have been extracted in this way, we may claim that we have a complete mathematical model of our system. As we have seen above, such a model is already made of a number of abstract machines, together with their refinements and decompositions. This may already form a significantly large structure. At this point, the informal requirement document is of no use anymore. It is then time to start thinking in terms of execution. For this, we continue the refinement and decomposition processes as above, but, this time, we are not driven anymore by the incorporation of new properties, we are rather driven by the idea of gradually transforming our motheinnticof models into software rrioduies.

Now refinement mainly acts on the variable spaces. It changes these spaces into others with components closer to programming variables (still represented, however, by well defined mathematical objects). Refinement also acts on the statements of the actions: pre-conditions are weakened (in fact, very shortly they disappear completely), non-determinacy is gradually reduced (in other words, postponed decisions are taken), conditionals, sequencing and loops gradually appear (the program takes shape). Proofs continue also to be performed, hence debugging is still active. At this point, we clearly think less as professionals of our system, more as pure informaticians concerned by efficiency.

Final Implementation on nn Extraneous Enuironment.

It is now time to envisage the end of our B development process. We may have two opposite attitudes here, or a mixture of both.

Either, we continue down refining until each of our variables has a direct counterpart in a classical programming language (scalar of a limited size, arrays

with well defined bounds, files, etc); in this case, the final formal text is indeed a program, which can be translated automatically into a classical programming language, or even directly into assembly code.

Or, we decide to stop earlier. In this case, we may use another collection of abstract machines, whose operations represent our “repertoire of instructions” . These machines are used to implement the last refinements we have obtained; of course, such machines are never refined (at least by us), they only represent the formal B interface to the environment, on which we decide to implement our final refinements. This environment can be very low level (for instance: a simple library), or, on the contrary, a vast piece of data and code (for instance: an entire data base). This technique allows us to use B on the most vital parts of a system only. Notice that it can also be the beginning of yet another B development that has been made beforehand (bottom up construction and reusability) .

The Proofs Accompany the Development Process.

As can be seen, the proof process has indeed accompanied the development process along each of its phases, namely the property extraction phases, the architecture building phases, and the implementation phases. Experience shows that the complexity of the proofs is a faithful indication of that of our devel- opment. If proofs are too complicated, a certain re-organization of the way the design is done might have, quite often, some spectacular effects. In fact, thinking in terms of proof constitutes, as experience shows, an extremely efficient heuris- tic for constructing large and complex software systems. Incorporating in one's mind the permanent idea of proving is, we think, a sign of maturity.

Why use B ?

As the text above has shown, doing a development with B is not a small enterprise. One might then wonder whether it is worth at all engaging in this direction. Sometimes people say that B should only be used for the development of safety critical systems, in other words that the decision to use B is dictated by the nature of the problem at hand. This view, in our opinion, is erroneous.

People, we think, should engage in a B development only if they are ready to do so. A measure of this readiness is indicated by their degree of disappointment with respect to their present development process. Should this process be well integrated in their organization and should it give entire satisfaction, then no B development is necessary, even worse it could be dangerous to destroy some- thing that works well. On the other hand, when people have some doubts about the adequacy of their development process, then the utilization of B could be envisaged.

In other words, it is not so much the nature of the problem that counts for taking such a decision (of using B), than the understanding that something has gone wrong in the way systems are developed. And one of the first question to be solved is then, of course, that of the integration of B within the old development process. In particular, as we pointed out above, the question of the re-writing of the requirement documents (to be integrated at the beginning of the develop- ment process), and the question of the proofs (to be integrated as a permanent concern in each phase the development process) are of utmost importance.

How to Use B., Questioning the Provers.

It is clear that B cannot be used without some tools. On view of what has been said above, it is also clear that, among thèse tools, the provers (automatic and interactive) play a prominent rôle. On projects of a significant size and “av- erage” difficulty, a classical figure is that the automatic prover should succeed in discharging 80% of the proofs. The remaining proofs have to be handled with the interactive prover. One should also remember the following rule of thumb: roughly speaking, a B development resulting in n lines of final code demands the proof of n/2 little lemmas, and an “average” trained person is able to conduct 15 interactive proofs per day. For instance, on a project whose part developed with B amounts to 50,000 lines, we have thus 25,000 proofs, among which 5,000 (that is 20%) are not discharged automatically. The manual (interactive) treatment of such proofs will then represent a work load that amounts to 5, 000/ 15 = 333 man-days, that is roughly 15 man-months '. This has to be compared with the testing effort (as well as with the “price” of the late discovery of bugs) that must be paid in the classical development of large software systems.

The inside of such provers must be visible and trustable. It is not conceivable that people take the “success/failure” answers of such programs for granted. In particular, all the inference rules of such provers should, not only be visible (this is obvious), but they should themselves be proved, with full visibility given on such second order proofs and on the corresponding second order prover. In fact, experience shows that, on the average, between 2 to 5% of such inference rules are wrong, if no care is taken. Moreover, for the purpose of extending the capa- bilities of the prover, people can add their own rules of inferences. Such added rules must also be proved “on line” .

More generally, the industrial usage of such tools and the importance of the projects in which they are engaged, require that they obtain an industrial “recog- nition” of some sort on the part of an independent “body”. Such an effort is very costly, but is, we think, an indispensable prerequisite for the industrial credibility of the B approach. To the best of our knowledge, Atelier B fulfills, to a large extent, these requirements: it has been formally approved by a consortium led by RATP, the Parisian Metro Authority

' This figure can be lowered provided the interactive prover hae the capability to

largely re-use tactics and sub-proofs

People and Education

Technology is nothing without people. And people are able to develop and use a certain technology provided they hone received the odequate education. In the case of B, what can be seen in some parts of the world is very encouraging. There is, however, an area where this education is, we think, too weak. This is precisely that part that is centered around the question of /ormof proo/s. In our opinion, this subject is still taught in a way that is either too formal and theoretical, or, at the other end of the spectrum, entirely devoted to the study of some tools.

It seems to us that a new subject entitled “Proof and Prover Technology” has to be introduced in Computer Science curricula in the coming years. This has to be done in an independent fashion, in very much the same way as the “Lan- guage and Compiler Technology” subject has been introduced many decades ago independently of any particular language and compiler. By the way, a number of techniques of compiler technology could certainly be fruitfully incorporated in the prover technology (the static part of a compiler is, after all, a low level prover) .

Formal methods in general, and B in particular, are still sometimes taught in an old-fashioned way, by concentrating the presentations around the linguistic aspects. Students then get the impression that these formalisms are just very high level programming languages. This is reinforced by the practical exercises they are asked to do, namely to put their knowledge into practice by just writing some formal specifications and designs. It is very important that they should also be asked to prove them, so as to figure out that it is not easy (in particular the first time), and that the idea of the proof must permanently influence the way they have to structure their formal texts.

Research and the Future of B

Research on B must continue, it is vital. The proceedings of this conference show, if at all necessary, that it is indeed very active and rich. People have al- ready proposed a number of extensions to B, and they will do so in the future. This is normal and certainly shows the interest and the creativity of our com- munity. It must therefore be warmly encouraged. There is a risk, hoWever, that everyone knows: the proliferation of various incompatible dialects, all pretending to represent the “genuine” B. We have seen quite often this terrible tendency at work in other formalisms. It is dangerous. We have, however, the chance to still form a very small community.

In order to limit such risks, I thus propose that a (very small) committee be organized to think and propose some solutions to this problem. We have to remember that, on one hand, democracy is certainly indispensable, but that, on the other hand, no language or formalism project has ever been successfully achieved by a committee. Efficiency and reason should dictate our action here.

References

[Abr96] J.-R. Abrial, The B-Book: A 4signing proqrntns to tnenninps, Cambridge University Press, 1996.