Refinement calculus. A systematic introduction (Q4396958)

This book is the first systematic introduction to the mathematical and logical basis of refinement calculus, a framework for reasoning about correctness and refinement of programs. Invented by the first author, this method extends Dijkstra's use of weakest precondition for correctness of programs, where program statements are modeled as predicate transformers. The second author gave it a lattice-theoretic basis, which is used in this book in conjunction with higher-order logic to give a new foundation to refinement calculus. The book is divided in four parts. The first one introduces the foundations of refinement calculus, together with basic notions of lattice-theory and higher-order logic. In the second part the authors describe predicate transformers, then characterize a family of program statements which can be interpreted as predicate transformers having a monotonicity property with respect to the lattice-theoretic interpretation. This part is also the place for describing two other semantics, game semantics and choice semantics: the latter is equivalent to predicate transformers semantics and both are abstractions of the game semantics. The third part deals with recursion and iteration. The classical fixed point theorems of Tarski and Scott are taken advantage of to recursive procedures, loops, and various examples of the use of refinement calculus for sorting algorithms, for solving the N-Queen problem, or two-person games are studied in great detail. Finally, some subclasses of predicate transformers and of statements are studied, especially the important class of conjunctive statements. The authors study the application of refinement calculus to specification statements, the way to do refinement taking the context into account, and the correctness-preserving transformation of iterative structures. The book is thoroughly detailed and illustrated with a lot of examples. Each chapter ends with a historical notice and a series of exercises.