Constructing correct software.
2nd ed.

*(English)*Zbl 1061.68032
London: Springer (ISBN 1-85233-820-2/pbk). xxi, 509 p. (2005).

The book under review is the second edition of a standard text on formally based software construction procedures [Constructing correct software. The basics. Formal Approaches to Computing and Information Technology (FACIT). (Berlin: Springer). (1998; Zbl 0903.68121)], that appeared in 1998. This new edition is a carefully revised, up-dated and fine polished version of the previous one, keeping the content into the already established framework. Several approaches are reconsidered and enriched, as for instance Logical-Functional-Procedural (LFP) scheme of software development, which is mainly based in the first edition on ”checking” operations and forward directed, from the logic specification toward a Program Design Language (PDL) implementation. Accordingly, as compared to the first edition, the LFP scheme becomes bidirectional, allowing to work backwards toward the specification, and consequently, facilitating the human interventions to ”steer” the mechanical process of derivation, using heuristically based steps.

It is worth to point out that in the new version the style is significantly improved; several chapters are restructured and insignificant details are removed, facilitating the reader to focus on a deeper understanding of the main topics. We appreciate the idea of providing an interactive web page (www.springeronline.com/uk/1-85233-820-2) where additional text is available to the readers interested in a more detailed exposure.

The central ideas about the LFP program synthesis strategy come from Chapter 3- Algorithm Extraction, where the construction of recursive designs as solutions to various programming problems is rigorously presented. The design process is fairly mechanical and deals with both (reversible) algebraic transformations and (irreversible) refinements. The author introduces the concept of transfinement standing for the chain of design actions yielding to a rather recursive program scheme instead of an iterative control structure. Therefore, in the LFP strategy, the recursion has a ”bridging” effect between the extreme levels of specification, namely the logical level corresponding to an initial specification, and the procedural one, corresponding to a (possibly) iterative control structure expressed in PDL. The intermediate functional level results directly from the ”transfinement” process and contains (possibly) recursive definitions of different involved functions. Next, by a systematic recursive removal procedure the functional recursive design is turned into a procedural program containing iterative control structures. The main advantage of using recursion as an intermediate stage toward the iterative form, resides from the fact that the task of finding a loop invariant may be avoided. This way is essentially different from the ”standard” way in approaching algorithm synthesis [C. Morgan, Programming from specifications, Prentice Hall International Series in Computer Science. (London: Prentice Hall). (1994; Zbl 0829.68083)] where the loop invariant is the ”core” of the ”derivation process” from a specification to an implementation.

Additional techniques for translating recursive definitions into target languages that do not allow recursion, are considered in Chapter 4- Recursion Removal, where several removal schemes dealing with tail recursion, associative recursion and some ”counting up” recursive definitions are given a detailed presentation.

For the sake of completeness, we briefly recall the content of the book, which basically remained unchanged as compared to the first edition. Part A: Preliminaries contains two chapters: 1. The technical background and 2. On Programming. Part B: Fundamentals contains 4 chapters: 3. Algorithm Extraction; 4. Recursion Removal; 5. Quantifications. 6. Refinement and Re-use. Part C: Developments contains 6 chapters: 7. Sorting; 8. Data Refinement; 9. Sorting Revisited; 10. Failure and Fixes; 11. Further Examples; 12. On Interactive Software. The Appendix ”Transformation Digest” contains the following sections: A.0. Re-write rule Conventions; A.1. Data Manipulation Rules. A.2. Quantifier Properties; A.3. ”Not Occurs in”; A.4. On PDL Structure; A.5. PDL Transformation Rules.

The content of the book is mainly based on the lectures presented by the author at Loughborough University. In our opinion, the book could be of interest for a wider area of readers, graduate students and computer scientists involved in tasks of algorithm formal design.

It is worth to point out that in the new version the style is significantly improved; several chapters are restructured and insignificant details are removed, facilitating the reader to focus on a deeper understanding of the main topics. We appreciate the idea of providing an interactive web page (www.springeronline.com/uk/1-85233-820-2) where additional text is available to the readers interested in a more detailed exposure.

The central ideas about the LFP program synthesis strategy come from Chapter 3- Algorithm Extraction, where the construction of recursive designs as solutions to various programming problems is rigorously presented. The design process is fairly mechanical and deals with both (reversible) algebraic transformations and (irreversible) refinements. The author introduces the concept of transfinement standing for the chain of design actions yielding to a rather recursive program scheme instead of an iterative control structure. Therefore, in the LFP strategy, the recursion has a ”bridging” effect between the extreme levels of specification, namely the logical level corresponding to an initial specification, and the procedural one, corresponding to a (possibly) iterative control structure expressed in PDL. The intermediate functional level results directly from the ”transfinement” process and contains (possibly) recursive definitions of different involved functions. Next, by a systematic recursive removal procedure the functional recursive design is turned into a procedural program containing iterative control structures. The main advantage of using recursion as an intermediate stage toward the iterative form, resides from the fact that the task of finding a loop invariant may be avoided. This way is essentially different from the ”standard” way in approaching algorithm synthesis [C. Morgan, Programming from specifications, Prentice Hall International Series in Computer Science. (London: Prentice Hall). (1994; Zbl 0829.68083)] where the loop invariant is the ”core” of the ”derivation process” from a specification to an implementation.

Additional techniques for translating recursive definitions into target languages that do not allow recursion, are considered in Chapter 4- Recursion Removal, where several removal schemes dealing with tail recursion, associative recursion and some ”counting up” recursive definitions are given a detailed presentation.

For the sake of completeness, we briefly recall the content of the book, which basically remained unchanged as compared to the first edition. Part A: Preliminaries contains two chapters: 1. The technical background and 2. On Programming. Part B: Fundamentals contains 4 chapters: 3. Algorithm Extraction; 4. Recursion Removal; 5. Quantifications. 6. Refinement and Re-use. Part C: Developments contains 6 chapters: 7. Sorting; 8. Data Refinement; 9. Sorting Revisited; 10. Failure and Fixes; 11. Further Examples; 12. On Interactive Software. The Appendix ”Transformation Digest” contains the following sections: A.0. Re-write rule Conventions; A.1. Data Manipulation Rules. A.2. Quantifier Properties; A.3. ”Not Occurs in”; A.4. On PDL Structure; A.5. PDL Transformation Rules.

The content of the book is mainly based on the lectures presented by the author at Loughborough University. In our opinion, the book could be of interest for a wider area of readers, graduate students and computer scientists involved in tasks of algorithm formal design.

Reviewer: Tudor Bălănescu (Pitesti)

##### MSC:

68Q60 | Specification and verification (program logics, model checking, etc.) |

68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |

68N01 | General topics in the theory of software |