Refinement Calculus

by Back, Ralph-Johan; Wright, J. Von

• ISBN13: 9780387984179
• ISBN10: 0387984178
• Format: Paperback
• Copyright: 1998-04-01
• Publisher: Springer Verlag

Summary

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.

Table of Contents

Preface	v
1 Introduction	1	(26)
1.1 Contracts	1	(5)
1.2 Using Contracts	6	(3)
1.3 Computers as Agents	9	(1)
1.4 Algebra of Contracts	10	(2)
1.5 Programming Constructs	12	(3)
1.6 Specification Constructs	15	(3)
1.7 Correctness	18	(2)
1.8 Refinement of Programs	20	(1)
1.9 Background	21	(3)
1.10 Overview of the Book	24	(3)
I Foundations	27	(158)
2 Posets, Lattices, and Categories	29	(28)
2.1 Partially Ordered Sets	29	(7)
2.2 Lattices	36	(4)
2.3 Product and Function Spaces	40	(3)
2.4 Lattice Homomorphisms	43	(6)
2.5 Categories	49	(5)
2.6 Summary and Discussion	54	(1)
2.7 Exercises	54	(3)
3 Higher-Order Logic	57	(12)
3.1 Types and Terms	57	(5)
3.2 Semantics	62	(1)
3.3 Deductive Systems	63	(2)
3.4 Theories	65	(1)
3.5 Summary and Discussion	66	(1)
3.6 Exercises	67	(2)
4 Functions	69	(16)
4.1 Properties of Functions	69	(4)
4.2 Derivations	73	(4)
4.3 Definitions	77	(3)
4.4 Product Type	80	(2)
4.5 Summary and Discussion	82	(1)
4.6 Exercises	83	(2)
5 States and State Transformers	85	(24)
5.1 State Transformers	85	(1)
5.2 State Attributes and Program Variables	86	(5)
5.3 Reasoning with Program Variables	91	(6)
5.4 Straight-Line Programs	97	(1)
5.5 Procedures	98	(3)
5.6 Blocks and Value Parameters	101	(6)
5.7 Summary and Discussion	107	(1)
5.8 Exercises	108	(1)
6 Truth Values	109	(18)
6.1 Inference Rules for Boolean Lattices	109	(2)
6.2 Truth Values	111	(1)
6.3 Derivations with Logical Connectives	112	(3)
6.4 Quantification	115	(3)
6.5 Assumptions	118	(2)
6.6 Derivations with Local Assumptions	120	(3)
6.7 Summary and Discussion	123	(1)
6.8 Exercises	124	(3)
7 Predicates and Sets	127	(12)
7.1 Predicates and Sets	127	(3)
7.2 Images and Indexed Sets	130	(1)
7.3 Inference Rules for Complete Lattices	131	(2)
7.4 Bounded Quantification	133	(2)
7.5 Selection and Individuals	135	(1)
7.6 Summary and Discussion	136	(1)
7.7 Exercises	137	(2)
8 Boolean Expressions and Conditionals	139	(12)
8.1 Boolean Expressions	139	(2)
8.2 Reasoning About Boolean Expressions	141	(2)
8.3 Conditional Expressions	143	(3)
8.4 Proving Properties About Conditional State Transformers	146	(2)
8.5 Summary and Discussion	148	(1)
8.6 Exercises	149	(2)
9 Relations	151	(16)
9.1 Relation Spaces	151	(2)
9.2 State Relation Category	153	(1)
9.3 Coercion Operators	154	(1)
9.4 Relational Assignment	155	(4)
9.5 Relations as Programs	159	(2)
9.6 Correctness and Refinement	161	(3)
9.7 Summary	164	(1)
9.8 Exercises	164	(3)
10 Types and Data Structures	167	(18)
10.1 Postulating a New Type	167	(3)
10.2 Constructing a New Type	170	(2)
10.3 Record Types	172	(3)
10.4 Array Types	175	(4)
10.5 Dynamic Data Structures	179	(2)
10.6 Summary and Discussion	181	(1)
10.7 Exercises	181	(4)
II Statements	185	(114)
11 Predicate Transformers	187	(16)
11.1 Satisfying Contracts	187	(2)
11.2 Predicate Transformers	189	(3)
11.3 Basic Predicate Transformers	192	(3)
11.4 Relational Updates	195	(3)
11.5 Duality	198	(1)
11.6 Preconditions and Guards	199	(1)
11.7 Summary and Discussion	200	(2)
11.8 Exercises	202	(1)
12 The Refinement Calculus Hierarchy	203	(10)
12.1 State Categories	203	(3)
12.2 Homomorphisms	206	(5)
12.3 Summary and Discussion	211	(1)
12.4 Exercises	212	(1)
13 Statements	213	(20)
13.1 Subtyping, Sublattices and Subcategories	213	(4)
13.2 Monotonic Predicate Transformers	217	(2)
13.3 Statements and Monotonic Predicate Transformers	219	(4)
13.4 Derived Statements	223	(4)
13.5 Procedures	227	(1)
13.6 Summary and Discussion	228	(2)
13.7 Exercises	230	(3)
14 Statements as Games	233	(16)
14.1 Game Interpretation	233	(6)
14.2 Winning Strategies	239	(5)
14.3 Correctness and Refinement	244	(2)
14.4 Summary and Discussion	246	(1)
14.5 Exercises	246	(3)
15 Choice Semantics	249	(10)
15.1 Forward and Backward Semantics	249	(3)
15.2 Comparing Semantics for Contract Statements	252	(2)
15.3 Refinement in the Choice Semantics	254	(1)
15.4 Summary and Discussion	255	(1)
15.5 Exercises	256	(3)
16 Subclasses of Statements	259	(10)
16.1 Homomorphic Predicate Transformers	259	(5)
16.2 Subcategories of Statements	264	(2)
16.3 Summary and Discussion	266	(1)
16.4 Exercises	267	(2)
17 Correctness and Refinement of Statements	269	(30)
17.1 Correctness	269	(4)
17.2 Stepwise Refinement	273	(7)
17.3 Refinement Laws	280	(7)
17.4 Refinement in Context	287	(4)
17.5 Refinement with Procedures	291	(1)
17.6 Example: Data Refinement	292	(3)
17.7 Summary and Conclusions	295	(2)
17.8 Exercises	297	(2)
III Recursion and Iteration	299	(126)
18 Well-founded Sets and Ordinals	301	(16)
18.1 Well-Founded Sets and Well-Orders	301	(2)
18.2 Constructing the Natural Numbers	303	(2)
18.3 Primitive Recursion	305	(2)
18.4 Ordinals	307	(3)
18.5 Ordinal Recursion	310	(2)
18.6 How Far Can We Go?	312	(2)
18.7 Summary and Discussion	314	(1)
18.8 Exercises	314	(3)
19 Fixed Points	317	(12)
19.1 Fixed Points	317	(3)
19.2 Fixed points as Limits	320	(2)
19.3 Properties of Fixed Points	322	(4)
19.4 Summary and Discussion	326	(1)
19.5 Exercises	327	(2)
20 Recursion	329	(18)
20.1 Fixed Points and Predicate Transformers	329	(5)
20.2 Recursion Introduction and Elimination	334	(2)
20.3 Recursive Procedures	336	(6)
20.4 Example: Computing the Square Root	342	(1)
20.5 Summary and Discussion	343	(1)
20.6 Exercises	344	(3)
21 Iteration and Loops	347	(18)
21.1 Iteration	347	(3)
21.2 Properties of Iterations	350	(2)
21.3 Correctness of Iterations	352	(1)
21.4 Loops	353	(1)
21.5 Loop Correctness	356	(3)
21.6 Loop Introduction and Elimination	359	(2)
21.7 Summary and Discussion	361	(1)
21.8 Exercises	362	(3)
22 Continuity and Executable Statements	365	(18)
22.1 Limits and Continuity	365	(2)
22.2 Continuity of Statements	367	(4)
22.3 Continuity of Derived Statements	371	(2)
22.4 Executable Statements	373	(4)
22.5 Interactive Guarded Commands	377	(3)
22.6 Summary and Discussion	380	(1)
22.7 Exercises	381	(2)
23 Working with Arrays	383	(20)
23.1 Resetting an Array	383	(3)
23.2 Linear Search	386	(2)
23.3 Selection Sort	388	(2)
23.4 Counting Sort	390	(12)
23.5 Summary and Discussion	402	(1)
23.6 Exercises	402	(1)
24 The N-Queens Problem	403	(10)
24.1 Analyzing the Problem	403	(3)
24.2 First Step: The Terminating Case	406	(1)
24.3 Second Step: Extending a Partial Solution	407	(2)
24.4 Third Step: Completing for Recursion Introduction	409	(2)
24.5 Final Result	411	(1)
24.6 Summary and Discussion	411	(1)
24.7 Exercises	412	(1)
25 Loops and Two-Person Games	413	(12)
25.1 Modeling Two-Person Games	413	(2)
25.2 Winning Strategies	415	(2)
25.3 Extracting Winning Strategies	417	(4)
25.4 Strategy Improvement	421	(1)
25.5 Summary and Discussion	422	(1)
25.6 Exercises	422	(3)
IV Statement Subclasses	425	(72)
26 Statement Classes and Normal Forms	427	(20)
26.1 Universally Conjunctive Predicate Transformers	427	(2)
26.2 Conjunctive Predicate Transformers	429	(2)
26.3 Disjunctive Predicate Transformers	431	(1)
26.4 Functional Predicate Transformers	432	(3)
26.5 Continuous Predicate Transformers	435	(2)
26.6 Homomorphic Choice Semantics	437	(6)
26.7 Summary and Discussion	443	(1)
26.8 Exercises	444	(3)
27 Specification Statements	447	(16)
27.1 Specifications	448	(1)
27.2 Refining Specifications by Specifications	449	(4)
27.3 Combining Specifications	453	(4)
27.4 Refining Conjunctive Specifications	457	(1)
27.5 General Refinement of Specifications	458	(2)
27.6 Summary and Discussion	460	(1)
27.7 Exercises	461	(2)
28 Refinement in Context	463	(16)
28.1 Taking the Context into Account	463	(4)
28.2 Rules for Propagating Context Assertions	467	(4)
28.3 Propagation in Derived Statements	471	(4)
28.4 Context Assumptions	475	(2)
28.5 Summary and Discussion	477	(1)
28.6 Exercises	478	(1)
29 Iteration of Conjunctive Statements	479	(18)
29.1 Properties of Fixed Points	479	(3)
29.2 Relating the Iteration Statements	482	(2)
29.3 Iteration of Meets	484	(2)
29.4 Loop Decomposition	486	(1)
29.5 Other Loop Transformations	487	(2)
29.6 Example: Finding the Period	489	(5)
29.7 Summary and Discussion	494	(1)
29.8 Exercises	494	(3)
Appendix	497	(4)
References	501	(8)
Index	509