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.