zbMATH — the first resource for mathematics

Programming from specifications. 2nd ed. (English) Zbl 0829.68083
Prentice Hall International Series in Computer Science. London: Prentice Hall. xv, 332 p. (1994).
This is a substantially enhanced version of the well known book printed in 1990 ( Zbl 0697.68018), whose main idea is that specifications and code are all programs and there is a refinement order between programs, induced by the ‘client’ point of view in describing the negotiation: the program \(P\) refines \(Q\) if \(Q\) is ‘better’ then \(P\) for the client. The refinement process is governed by a rich set of laws of refinement, collected in a useful appendix, for a direct access. In this new edition there is a rearrangement of the material so that the programming language feature are introduced consecutively, without the intervention of chapters on more technical matters. The chapter ‘Procedure and parameters’ has been also modified, receiving a more conventional treatment. The new included material is considerable. Thus, the chapter ‘Constructed types’ contains two new sections ‘9.5 Functions’ and ‘9.6 Relations’ in the ‘Z style’ presentation. There is a new added chapter ‘15 Recursive types’; the chapter ‘17 State transformation and data refinement’ contains a new section on ‘Abstract functions’. There are two new large case studies: ‘the largest rectangle under a histogram’ and a ‘mail system’. The new form of the book preserves the accessibility, the self understanding feature and the conciseness of the first edition. Research workers will find much stimulating material here. The book may be also successfully used as a support for both undergraduate and graduate courses.
Reviewer: T.Balanescu

68Q60 Specification and verification (program logics, model checking, etc.)
68-02 Research exposition (monographs, survey articles) pertaining to computer science