Software Engineering With B (International Computer Science Series) - Softcover

Wordsworth, J. B.

Softcover

ISBN 10: 0201403560 ISBN 13: 9780201403565

Publisher: Addison-Wesley, 1996

Synopsis

This is the definitive guide to software engineering with B - the generic name for the software development method invented by Jean-Raymond Abrial, and for the language and CASE tool developed by B-Core (UK) Ltd. The B-method is almost unique among formal software development methods in that it uses a single notation for specification, design and programming. Using tutorial examples, this practical guide can be applied to the whole software engineering life cycle. An accompanying disk allows the reader to experiment with program examples.

About this title

From the Inside Flap:

Software engineering with B has three aspects, and in this book I hope to show that the interaction of these can be used in two ways: first as an aid to practical software development in a competitive environment, and second as a subject of study for potential software engineers. The dual nature of the book means that it caters for two distinct audiences. For the industrial user it is a complete account of the B-Method, with examples and exercises, for many of which solutions are provided. For the academic user it is a source book of applications of a simple but far-reaching mathematical theory, and can serve as a text for an undergraduate or post-graduate software engineering course.

The first aspect of B is the B-Method, a method for the systematic development of large software systems from reusable fragments, which is an essential part of software engineering. It is important that the approach should be systematic, and not piecemeal, or software development could hardly qualify as an engineering discipline. It is also important that we should be able to develop large software systems, since today's software purchasers demand a lot of function. Lastly it is important to have a way of reusing software components, or software development projects will inevitably have low productivity and take a long time to market.

The second aspect of B is the abstract machine notation (AMN), a well-tried body of mathematics to support the systematic method just mentioned. The abstraction and precision that come from using set theory and predicate calculus in software development give the software developer a power that is not available to those using informal methods. This power is required by some software procurers, especially for defence and safety-critical systems, but its use to gain commercial advantage in industrial software development, particularly in high-integrity, high-availability systems, is becoming more common.

The third aspect of B is the B-Toolkit, a collection of computer-based tools to automate many of the procedures of a mathematically based software development method. The toolkit supports most of the activities of software engineering: specification, animation, consistency proofs, design, proof obligation generation, correctness verification, code generation from designs, test application generation, and the production of well-indexed documentation to record the development.

The subject of this book is the ideal combination of these three. The systematic method makes the software engineer's efforts profitable, the mathematics makes them dependable, and the toolkit makes them possible. The contents of the book are as follows: Chapter 1 introduces the ideas of software engineering supported by the B-Method, particularly the notion of a layered structure for software.

Chapter 2 introduces the idea of a machine as a specification for software, discusses the nature of the proof obligations for consistency of a machine, and describes ways of using machines in various layers of a software structure.

Chapter 3 shows how a component-layer machine is built, and introduces more substitutions for machines.

Chapter 4 introduces the ideas of deferred sets, and introduces some substitutions for specifying non-determinism in operations.

Chapter 5 shows how large machines can be constructed from smaller machines.

Chapter 6 completes the repertoire of substitutions that can be used in machines.

Chapter 7 introduces the idea of software design as the process of producing a software object from a specification expressed as a machine. It explores the idea of correctness of designs.

Chapter 8 introduces the idea of an implementation as the software developer's view of a software system, and describes ways of reusing machines from lower layers of the software structure.

Chapter 9 concentrates on machines for the application programming interface (API) layer, and on their implementations. This chapter also shows how data types more complex than numbers can be introduced into a development.

Chapter 10 introduces the idea of a refinement as an intermediary between a machine and its implementation.

Appendices review the relevant discrete mathematics, and summarize the notation used in the book. There are definitions of the B-Toolkit library machines used in the book, sample solutions to many of the exercises, a bibliography, a glossary of technical terms and a comprehensive index. SUPPLEMENTARY MATERIAL ON THE WORLD WIDE WEB

Readers of the book who do not have a copy of the B-Toolkit are invited to access the following FTP site: ftp://ftp.aw/cseng/authors/wordsworth/softeng-b/
where they will find a demonstration copy of the B-Toolkit. The README.softeng-b file gives instructions for down-loading the toolkit and for operating it using some of the material from this book.

Readers of the book who have access to a full-function copy of the B-Toolkit can use the diskette provided with the book for working through the demonstrations and exercises. Full operating instructions for using the diskette with the B-Toolkit are available on the World Wide Web. Use your web browser to find
aw/cseng/authors/wordsworth/softeng-b/
and follow the link to the book supplements page.

If you have questions or comments about this book, please send e-mail to aw.cse@awl.

ACKNOWLEDGEMENTS

The B-Method and the abstract machine notation were invented by Jean-Raymond Abrial, and developed by him and others over several years at BP Research, Sunbury on Thames. As Abrial is also the inventor of Z, everyone interested in formal methods of software development owes him a considerable intellectual debt.

An early draft of this book was reviewed by several people who made useful comments, and I list them here: Juan Bicarregui, Rutherford-Appleton Laboratory; Jeremy Jacob, University of York; Michel Lemoine, CERT-ONERA; Ken Robinson, University of New South Wales; Arthur Ryman, IBM Canada; Shin'ichi Sano, Fujitsu Co.; Bill Stoddart, University of Teesside; Takeji Tanaka, International Christian University, Tokyo; Eoin Woods, LBMS. Several anonymous reviewers made comments on behalf of publishers, but they must remain anonymous.

IBM has always encouraged its employees to publish books that might enhance the corporation's technical reputation in the industrial and academic worlds. I am pleased to say that they have supported the preparation of this book by allowing me to use a B-Toolkit system at the Hursley Park laboratory, by giving me facilities for text preparation and storage, and by allowing me to print drafts, of which the last is the one now published. The figures and some of the text relating to the Resource Manager example have appeared before in tutorial material prepared for IBM, and this material is reproduced here with IBM's permission.

During most of the fourteen years that I have been studying and using formal methods, I have been fortunate to know Ib Sorensen, first at the University of Oxford, where he worked on the IBM CICS project, then at BP Research, and finally at B-Core (UK) Ltd. His help with this book has been invaluable, and he has acted as teacher, critic, and as an inexhaustible source of information.

Finally I should like to thank my wife and family for putting up yet again with the disruption to family life caused by the writing process.

John Wordsworth
June 1996 0201403560P04062001

About the Author:

John Wordsworth is a technical writer at IBM United Kingdom Laboratories at Hursley Park.

About this edition

• Publisher: Addison-Wesley
• Publication date: 1996
• ISBN 10: 0201403560
• ISBN 13: 9780201403565
• Binding: Paperback
• Number of pages: 331