Refinement calculus
Subtitle: a systematic introduction
By: Ralph-Johan Back, Joakim von Wright.
Contributors: Wright, J. von 1955-
Series: Graduate texts in computer science; Graduate texts in computer science (Springer-Verlag New York Inc.)
Publisher: Springer
Published: 1998
Place of publication: New York
Language: eng
Number of pages: 519
Subjects: Computer programming; Calculus; Computer logic
Description: The authors begin with a presentation of a new foundation for the refinement calculus based on lattice theory and higher order logic, together with a simple theory of program variables. The second part of the book describes the predicate transformer approach to programming logic and program semantics as well as the refinement calculus. The authors examine contracts, games, and program statements and show how their operational semantics is related to their predicate transformer interpretation.

The third part of the book shows how to handle recursion and iteration in the refinement calculus and also describes how to use the calculus to reason about two-person games. Also presented are case studies of program refinement. In the final part, the book addresses specific issues related to program refinement, such as implementing specification statements, making refinements in context, and transforming iterative structures in a correctness preserving way.

The book is intended for graduate and advanced undergraduate students interested in the mathematics and logic of systematic program construction as well as for programmers and researchers interested in a deeper understanding of these issues.
Notes: Includes bibliographical references (p. [501]-508) and index.