Constructing correct software.

Publication date 19 January 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 \textit{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 \textit{loop invariant} may be avoided. This way is essentially different from the standard way in approaching algorithm synthesis [\textit{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.

Recommendations

Cited in

(3)

This page was built for publication: Constructing correct software.

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3157875)