Software Engineering with B

Software Engineering with B was published by Addison Wesley Longman in July 1996, ISBN 0-201-40356-0.

The summary of contents is 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. It shows how a program can be regarded as a generalized substitution.

• 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 show how large machines can be constructed from smaller machines.

• Chapter 6 completes the repertoire of substitutions that can be used in machines, and illustrates the idea of a full-function machine.

• 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. Code generation is discussed in this chapter.

• Chapter 9 introduces machines for the application programming interface (API) layer, and their implementations. It 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.

• Appendixes summarize the discrete mathematics, and the notation used in the book. There are sample solutions to many of the exercises, a bibliography, a glossary of technical terms, and a comprehensive index.

• A diskette containing the source material for the examples and exercises is provided with the book.

Back to my list of publications.

Back to my home page.