Systematic software development using VDM. 2nd ed.

*(English)*Zbl 0743.68048
Prentice Hall International Series in Computer Science. New York etc.: Prentice Hall. XIV, 333 p. (1990).

This is a necessary text book: it introduces to the systematic development of software and uses the VDM notation for it (which is also introduced). The book’s point is that software needs to be developed in a mathematically oriented fashion, and it exercises a particular approach. Its main theme is “to show how mathematical notation can be used to increase the precision of a specification”, as the author writes in Chapter 13, a postscript to the main text. It achieves well what it wants to do: the reader is introduced in a leisurely fashion into basic notions from mathematics (sets, maps, propositional and predicate logic). From the beginning proof rules and proof obligations are introduced, so that the necessity of proving specifications correct comes rather naturally a little later on. The reader who has had no previous exposure to discrete mathematics should expect from this book a careful introduction into this field, as far as capturing the essence of proving specifications correct are concerned. This is not to say that the text is overly theoretical in approach or reasoning: it holds about the right balance between introducing and exercising theoretical concepts, and applying them to problems that have the smell of real world problems (cp. for example the discussion of biased models in Ch. 9.3).

The first four chapters introduce and develop the basic mathematics. This is applied in chapters 5-7 to composite objects (maps and sequences among them), emphasizing structural induction. Data transformations (called data reification here) are discussed in Chapter 8, and Chapter 9 introduces modules as data types. Operational decomposition is discussed in Chapter 10 (giving some nice demonstrations of the semantic compositionality of constructs and the associated proof rules as well as some equally nice loop holes), and two small case studies in Chapter 11 conclude the main part of the book. Some fourty pages are devoted to appendices.

In summary, this book is to be recommended to everybody who wants to have a practically oriented introduction to verifying formal specifications which is theoretically sound. It is well written. I am glad it’s there.

The first four chapters introduce and develop the basic mathematics. This is applied in chapters 5-7 to composite objects (maps and sequences among them), emphasizing structural induction. Data transformations (called data reification here) are discussed in Chapter 8, and Chapter 9 introduces modules as data types. Operational decomposition is discussed in Chapter 10 (giving some nice demonstrations of the semantic compositionality of constructs and the associated proof rules as well as some equally nice loop holes), and two small case studies in Chapter 11 conclude the main part of the book. Some fourty pages are devoted to appendices.

In summary, this book is to be recommended to everybody who wants to have a practically oriented introduction to verifying formal specifications which is theoretically sound. It is well written. I am glad it’s there.

Reviewer: E.E.Doberkat (Essen)