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.