Refinement Calculus

Much current research in computer science is concerned with two questions: is a program correct? And how can we improve a correct program preserving correctness? This latter question is known as the refinement of programs and the purpose of this book is to consider these questions in a formal setting. In fact, correctness turns out to be a special case of refinement and so the focus is on refinement. Although a reasonable background knowledge is assumed from mathematics and CS, the book is a self-contained introduction suitable for graduate students and researchers coming to this subject for the first time. There are numerous exercises provided of varying degrees of challenge.

1 Introduction.- 1.1 Contracts.- 1.2 Using Contracts.- 1.3 Computers as Agents.- 1.4 Algebra of Contracts.- 1.5 Programming Constructs.- 1.6 Specification Constructs.- 1.7 Correctness.- 1.8 Refinement of Programs.- 1.9 Background.- 1.10 Overview of the Book.- I Foundations.- 2 Posets, Lattices, and Categories.- 2.1 Partially Ordered Sets.- 2.2 Lattices.- 2.3 Product and Function Spaces.- 2.4 Lattice Homomorphisms.- 2.5 Categories.- 2.6 Summary and Discussion.- 2.7 Exercises.- 3 Higher-Order Logic.- 3.1 Types and Terms.- 3.2 Semantics.- 3.3 Deductive Systems.- 3.4 Theories.- 3.5 Summary and Discussion.- 3.6 Exercises.- 4 Functions.- 4.1 Properties of Functions.- 4.2 Derivations.- 4.3 Definitions.- 4.4 Product Type.- 4.5 Summary and Discussion.- 4.6 Exercises.- 5 States and State Transformers.- 5.1 State Transformers.- 5.2 State Attributes and Program Variables.- 5.3 Reasoning with Program Variables.- 5.4 Straight-Line Programs.- 5.5 Procedures.- 5.6 Blocks and Value Parameters.- 5.7 Summary and Discussion.- 5.8 Exercises.- 6 Truth Values.- 6.1 Inference Rules for Boolean Lattices.- 6.2 Truth Values.- 6.3 Derivations with Logical Connectives.- 6.4 Quantification.- 6.5 Assumptions.- 6.6 Derivations with Local Assumptions.- 6.7 Summary and Discussion.- 6.8 Exercises.- 7 Predicates and Sets.- 7.1 Predicates and Sets.- 7.2 Images and Indexed Sets.- 7.3 Inference Rules for Complete Lattices.- 7.4 Bounded Quantification.- 7.5 Selection and Individuals.- 7.6 Summary and Discussion.- 7.7 Exercises.- 8 Boolean Expressions and Conditionals.- 8.1 Boolean Expressions.- 8.2 Reasoning About Boolean Expressions.- 8.3 Conditional Expressions.- 8.4 Proving Properties About Conditional State Transformers.- 8.5 Summary and Discussion.- 8.6 Exercises.- 9 Relations.- 9.1 Relation Spaces.- 9.2 State Relation Category.- 9.3 Coercion Operators.- 9.4 Relational Assignment.- 9.5 Relations as Programs.- 9.6 Correctness and Refinement.- 9.7 Summary.- 9.8 Exercises.- 10 Types and Data Structures.- 10.1 Postulating a New Type.- 10.2 Constructing a New Type.- 10.3 Record Types.- 10.4 Array Types.- 10.5 Dynamic Data Structures.- 10.6 Summary and Discussion.- 10.7 Exercises.- II Statements.- 11 Predicate Transformers.- 11.1 Satisfying Contracts.- 11.2 Predicate Transformers.- 11.3 Basic Predicate Transformers.- 11.4 Relational Updates.- 11.5 Duality.- 11.6 Preconditions and Guards.- 11.7 Summary and Discussion.- 11.8 Exercises.- 12 The Refinement Calculus Hierarchy.- 12.1 State Categories.- 12.2 Homomorphisms.- 12.3 Summary and Discussion.- 12.4 Exercises.- 13 Statements.- 13.1 Subtyping, Sublattices and Subcategories.- 13.2 Monotonic Predicate Transformers.- 13.3 Statements and Monotonic Predicate Transformers.- 13.4 Derived Statements.- 13.5 Procedures.- 13.6 Summary and Discussion.- 13.7 Exercises.- 14 Statements as Games.- 14.1 Game Interpretation.- 14.2 Winning Strategies.- 14.3 Correctness and Refinement.- 14.4 Summary and Discussion.- 14.5 Exercises.- 15 Choice Semantics.- 15.1 Forward and Backward Semantics.- 15.2 Comparing Semantics for Contract Statements.- 15.3 Refinement in the Choice Semantics.- 15.4 Summary and Discussion.- 15.5 Exercises.- 16 Subclasses of Statements.- 16.1 Homomorphic Predicate Transformers.- 16.2 Subcategories of Statements.- 16.3 Summary and Discussion.- 16.4 Exercises.- 17 Correctness and Refinement of Statements.- 17.1 Correctness.- 17.2 Stepwise Refinement.- 17.3 Refinement Laws.- 17.4 Refinement in Context.- 17.5 Refinement with Procedures.- 17.6 Example: Data Refinement.- 17.7 Summary and Conclusions.- 17.8 Exercises.- III Recursion and Iteration.- 18 Well-founded Sets and Ordinals.- 18.1 Well-Founded Sets and Well-Orders.- 18.2 Constructing the Natural Numbers.- 18.3 Primitive Recursion.- 18.4 Ordinals.- 18.5 Ordinal Recursion.- 18.6 How Far Can We Go?.- 18.7 Summary and Discussion.- 18.8 Exercises.- 19 Fixed Points.- 19.1 Fixed Points.- 19.2 Fixed points as Limits.- 19.3 Properties of Fixed Points.- 19.4 Summary and Discussion.- 19.5 Exercises.- 20 Recursion.- 20.1 Fixed Points and Predicate Transformers.- 20.2 Recursion Introduction and Elimination.- 20.3 Recursive Procedures.- 20.4 Example: Computing the Square Root.- 20.5 Summary and Discussion.- 20.6 Exercises.- 21 Iteration and Loops.- 21.1 Iteration.- 21.2 Properties of Iterations.- 21.3 Correctness of Iterations.- 21.4 Loops.- 21.5 Loop Correctness.- 21.6 Loop Introduction and Elimination.- 21.7 Summary and Discussion.- 21.8 Exercises.- 22 Continuity and Executable Statements.- 22.1 Limits and Continuity.- 22.2 Continuity of Statements.- 22.3 Continuity of Derived Statements.- 22.4 Executable Statements.- 22.5 Interactive Guarded Commands.- 22.6 Summary and Discussion.- 22.7 Exercises.- 23 Working with Arrays.- 23.1 Resetting an Array.- 23.2 Linear Search.- 23.3 Selection Sort.- 23.4 Counting Sort.- 23.5 Summary and Discussion.- 23.6 Exercises.- 24 The N-Queens Problem.- 24.1 Analyzing the Problem.- 24.2 First Step: The Terminating Case.- 24.3 Second Step: Extending a Partial Solution.- 24.4 Third Step: Completing for Recursion Introduction.- 24.5 Final Result.- 24.6 Summary and Discussion.- 24.7 Exercises.- 25 Loops and Two-Person Games.- 25.1 Modeling Two-Person Games.- 25.2 Winning Strategies.- 25.3 Extracting Winning Strategies.- 25.4 Strategy Improvement.- 25.5 Summary and Discussion.- 25.6 Exercises.- IV Statement Subclasses.- 26 Statement Classes and Normal Forms.- 26.1 Universally Conjunctive Predicate Transformers.- 26.2 Conjunctive Predicate Transformers.- 26.3 Disjunctive Predicate Transformers.- 26.4 Functional Predicate Transformers.- 26.5 Continuous Predicate Transformers.- 26.6 Homomorphic Choice Semantics.- 26.7 Summary and Discussion.- 26.8 Exercises.- 27 Specification Statements.- 27.1 Specifications.- 27.2 Refining Specifications by Specifications.- 27.3 Combining Specifications.- 27.4 Refining Conjunctive Specifications.- 27.5 General Refinement of Specifications.- 27.6 Summary and Discussion.- 27.7 Exercises.- 28 Refinement in Context.- 28.1 Taking the Context into Account.- 28.2 Rules for Propagating Context Assertions.- 28.3 Propagation in Derived Statements.- 28.4 Context Assumptions.- 28.5 Summary and Discussion.- 28.6 Exercises.- 29 Iteration of Conjunctive Statements.- 29.1 Properties of Fixed Points.- 29.2 Relating the Iteration Statements.- 29.3 Iteration of Meets.- 29.4 Loop Decomposition.- 29.5 Other Loop Transformations.- 29.6 Example: Finding the Period.- 29.7 Summary and Discussion.- 29.8 Exercises.- References.