دانلود کتاب Data Refinement: Model-Oriented Proof Methods and their Comparison

فهرست مطالب :

Cover......Page 1
Frontmatter......Page 2
Contents......Page 6
Preface......Page 9
Part I - Theory......Page 14
1.1 Goal and Motivation......Page 15
1.2 Introduction to Data Refinement......Page 17
1.3 Historical Background......Page 30
2.1 Introducing Simulation......Page 32
2.2 Soundness and (In)completeness of Simulation......Page 35
2.3 Data Invariants, Abstraction Relations, and Normal Variables......Page 38
2.4 Towards a Syntactic Characterization of Simulation......Page 47
2.5 Historical Background......Page 59
3.1 Partial Orders and Monotonicity......Page 62
3.2 Binary Relations......Page 63
3.3 Recursion and Termination --- the [GREEK SMALL LETTER MU]-Calculus......Page 68
3.4 Relational Semantics of Recursion --- the Continuous [GREEK SMALL LETTER MU]-Calculus......Page 69
3.5 Reasoning about Termination --- the Monotone [GREEK SMALL LETTER MU]-Calculus......Page 75
3.6 Historical Background......Page 84
4 - Properties of Simulation......Page 86
4.1 Composing Simulation Diagrams......Page 87
4.2 Implications between Simulations......Page 90
4.3 Data Invariants and Totality of Abstraction Relations......Page 93
4.4 Soundness of Simulation......Page 94
4.5 Maximal Data Types......Page 95
4.6 Completeness......Page 96
4.7 Historical Background......Page 100
5 - Notation and Semantics......Page 103
5.1 Introduction......Page 104
5.2 Predicates......Page 106
5.3 Programs......Page 121
5.4 Relational Terms......Page 125
5.5 Correctness Formulae......Page 128
5.6 Historical Background......Page 132
6 - A Hoare Logic......Page 134
6.1 Proof System......Page 135
6.2 Soundness and (Relative) Completeness......Page 141
6.3 Historical Background......Page 143
7 - Simulation and Hoare Logic......Page 145
7.2 L-simulation in Hoare Logic......Page 146
7.3 L[MINUS SIGN]1 -simulation in Hoare Logic......Page 156
7.5 Historical Background......Page 157
8 - An Extension to Total Correctness......Page 159
8.1 Semantic Model and Basic Fixed Point Theory......Page 161
8.2 Interpretation Functions for Total Correctness......Page 173
8.3 Historical Background......Page 191
9.1 Simulation......Page 194
9.2 An L-Simulation Theorem for Total Correctness......Page 202
9.3 Historical Background......Page 206
10 - Refinement Calculus......Page 207
10.1 Lattice-theoretical Framework......Page 209
10.2 Predicate Transformer Semantics......Page 219
10.3 Predicate Transformers and Data Refinement......Page 228
10.4 Predicate Transformers and Partial Correctness......Page 236
10.5 Historical Background......Page 247
Picture Gallery......Page 249
Part II - Applications......Page 268
11.1 Introduction......Page 270
Running Examnle: Finding Paths in Directed Graohs......Page 271
Analysis of Data Refinement à la Reynolds......Page 285
Historical Background......Page 300
12.1 Introduction......Page 302
12.2 Example: Dictionary......Page 304
12.3 Analysis of Data Refinement in VDM......Page 314
12.4 Historical Background......Page 328
13 - Z, Hehner's Method, and Back's Refinement Calculus......Page 330
13.1 Z......Page 331
13.2 Hehner's Method for Data Refinement......Page 340
13.3 Back's Refinement Calculus......Page 345
14 - Refinement Methods due to Abadi and Lamport and to Lynch......Page 353
14.1 Auxiliary Variables and Refinement Mappings......Page 354
14.2 Possibilities Mappings......Page 371
14.3 Historical Background......Page 374
Appendix A - An Introduction to Hoare Logic......Page 376
Appendix B - A Primer on Ordinals and Transfinite Induction......Page 400
Appendix C - Notational Convention......Page 407
Appendix D - Precedences......Page 415
Bibliography......Page 417
Index......Page 432