Book Review: Specification in B: an introduction using the B toolkit. Kevin Lano and Howard Haughton. Published by Imperial College Press and distributed by World Scientific Publishing, London, U.K., 1996. ISBN: 1-86094-018-8, 242 pages. Price: U.K. £17.00, soft cover.
✍ Scribed by Hélène Waeselynck
- Publisher
- John Wiley and Sons
- Year
- 1997
- Tongue
- English
- Weight
- 27 KB
- Volume
- 7
- Category
- Article
- ISSN
- 0960-0833
No coin nor oath required. For personal study only.
✦ Synopsis
Book Reviews
Specification in B: An Introduction described with first-order logic and a set-theoretic model, while the dynamics (operations) are Using the B Toolkit. Kevin Lano and Howard Haughton. Published by Imperial Col-expressed by means of generalized substitutions having the semantics of predicate transformers. lege Press and distributed by World Scientific Publishing, London, U.K., 1996. ISBN: 1-The authors provide a general presentation of the corresponding notation through examples of 86094-018-8, 242 pages. Price: U.K. £17.00, Soft Cover.
simple machines, a more complete summary of notation being given in Appendix C. Of course, such general information would be quite insuf-The B method due to Jean-Raymond Abrial is a ficient in order to answer precise questions of formal approach covering all the software develsyntax that may arise during B development, but opment process, through a series of proved I found the level appropriate for an introductory refinement steps. It is a model-based approach course. However, important notions recently similar to Z and VDM. B has already been introduced by Abrial are missing: the abstract used for several industrial projects; in France, constants and concrete variables. Nonetheless, the especially, it is used for the development of use of both mathematical (LaTeX) and ASCII safety-critical software for railway systems. Two versions of the machines throughout the recent commercial toolsets supporting the method examples-as is done throughout the whole are available, the B Toolkit, from B-Core (UK) book-is appropriate, since tool users need to Limited, and the Atelier-B, from Digilog-Steria. learn their correspondence. I do have some reser-This book is intended to give a practical introducvations concerning the presentation of the semantion to the B method, emphasis being put on tics and consistency proof obligations: it really techniques that arise from the use of the B is too succinct. Also, one might be surprised Toolkit at the various phases of the development to see existence proof obligations that are not process. It is oriented towards educational use:
prescribed by The B-Book. Actually, the B philothe material is based on an M.Sc. course given sophy is to replace them by constructive proofs by the first author, and on various tutorials; some when needed. exercises, and their solutions, are given at the Chapter 2 shows how to compose machines in end of each chapter. Although based on the order to obtain larger pieces of specification. The example of the B Toolkit, the book is also composition mechanisms are illustrated by two intended to be relevant to users of alternative case studies: a drink dispenser and an air traffic toolsets. However, I found that some of the control system (ATC). These case studies possess examples and case studies given were rejected the right level of complexity to support the explaby the Atelier-B: they were not in full conformity nations, and are sufficiently small to remain with 'standard' B as defined by the reference understandable without being trivial. Chapter 3 work: The B-Book (Abrial, 1996). This is due to focuses on design and refinement. It introduces historical reasons, leading to the existence of two nicely the layered architecture paradigm that is toolsets and to delays in the publication of the central to the B development process, and reference book. Having been prepared on the sketches out general approaches to structuring basis of earlier documents, this book by Lano the design. The refinement process down to an and Haughton does not take into account the implementation is exemplified by the case of the most recent work of Abrial.
drink dispenser. The refinement of the ATC sys-This book contains six chapters and a collectem is delayed until Chapter 5 (devoted to tion of appendices. A basic knowledge of firstimplementation), where it serves as an illustration order logic and set-theory is a prerequisite for of how to implement abstract data structures. reading it. Chapter 1 introduces the concept of Together, Chapters 2, 3 and 5 introduce all essenan abstract machine (the basic component of a tial aspects of software construction. Practical B development) and the associated notation and examples of the facilities offered by the B Toolkit semantics. An abstract machine encapsulates state at the various development stages accompany data obeying static laws, called the invariant, and the discourse (specification animation, prototype offers some operations that are guaranteed to preserve the invariant. The statics (data) are generation, base generation, translation of B