Constructing correct software. The basics
This volume presents a method allowing the construction of correct algorithms from specification using algebraic transformations and refinement techniques. In Chapter 1 are introduced different ways of presenting the specifications. Different components necessary to specify functions are presented. Various data types associated with the inputs and outputs of these functions are introduced. In Chapter 2 are defined some concepts related to term rewriting system based on sets of equations. An example showing how transformations can be used to manipulate programs is introduced. In Chapter 3 the problem of transforming a specification into a scheme for its implementation is investigated. A discussion of how certain recursive forms can be replaced by iteration components is also presented. In Chapter 4 are introduced some more ways of defining composite values -- by means of functions and algebraic operations -- as well as their application to program development. Some rules for the manipulation of quantifiers are also presented. Different problems related to refinement are presented in Chapter 5. First the operational refinement, referring to a finite sequence of consistent relations each of which being more deterministic than its predecessor is introduced. A short discussion on the reuse of existing specification/implementation pairs and a brief digression on data refinement are also presented. Some failures related to the structural splitting strategy are pointed out. In Chapter 6 are presented various ways of selecting different algorithms derived from a single specification for a sorting problem. Three main design levels and the generation of the specifications of sub-problems are first introduced. Finally it is shown how the induced operations can quickly yield a design for a sorting problem. In Chapter 7 are presented two examples in order to describe the problem of manipulation (refinement) prior to software development. First, it is considered the (2-dimensional) convex hull problem for which the complex data involved presents an additional complication in formulating an adequate specification. The second example involving a topological sorting problem, is important for pointing out that a simplistic initial specification leads to the possibility of failure. Some specifications involving change are presented in the first part of the Chapter 8. Lastly are briefly discussed some factors involved in the process of software system design. This book is a useful reading for all those intersted in Computer Science and in Software Engineering to whom correctness and software is of prime importance.
- From informal requirements to a running program: A case study in algebraic specification and transformational programming
- Constructing specification morphisms
- A refinement-based approach to deriving train controllers
- scientific article; zbMATH DE number 2130217 (Why is no real title available?)
- scientific article; zbMATH DE number 46424 (Why is no real title available?)
- scientific article; zbMATH DE number 2080000 (Why is no real title available?)
- scientific article; zbMATH DE number 5199012 (Why is no real title available?)
- The correctness-by-construction approach to programming
This page was built for publication: Constructing correct software. The basics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4390387)
