Using Z: Specification, Refinement, and Proof

Cover......Page 2
Contents......Page 4
Foreword......Page 10
Using this Book......Page 12
Acknowledgments......Page 14
Formal methods......Page 16
The CICS experience......Page 17
The Z notation......Page 18
The importance of proof......Page 19
Abstraction......Page 20
Propositional logic......Page 24
Conjunction......Page 25
Disjunction......Page 28
Implication......Page 29
Equivalence......Page 32
Negation......Page 35
Tautologies and contradictions......Page 38
Predicate Logic......Page 42
Predicate calculus......Page 43
Quantifiers and declarations......Page 45
Substitution......Page 49
Universal introduction and elimination......Page 51
Existential introduction and elimination......Page 55
Satisfaction and validity......Page 58
Equality......Page 60
The one-point rule......Page 63
Uniqueness and quantity......Page 65
Definite description......Page 67
Membership and extension......Page 72
Set comprehension......Page 76
Power sets......Page 80
Cartesian products......Page 81
Union, intersection, and difference......Page 83
Types......Page 84
Declarations......Page 88
Abbreviations......Page 89
Generic abbreviations......Page 90
Axiomatic definitions......Page 92
Generic definitions......Page 94
Sets and predicates......Page 96
Binary relations......Page 98
Domain and range......Page 100
Relational inverse......Page 103
Relational composition......Page 106
Closures......Page 109
Partial functions......Page 114
Lambda notation......Page 116
Functions on relations......Page 118
Overriding......Page 120
Properties of functions......Page 122
Finite sets......Page 126
Sequence notation......Page 130
A model for sequences......Page 134
Functions on sequences......Page 137
Structural induction......Page 139
Bags......Page 143
The natural numbers......Page 148
Free type definitions......Page 150
Proof by induction......Page 155
Primitive recursion......Page 157
Consistency......Page 160
The schema......Page 162
Schemas as types......Page 167
Schemas as declarations......Page 169
Schemas as predicates......Page 173
Renaming......Page 175
Generic schemas......Page 177
Conjunction......Page 180
Decoration......Page 183
Disjunction......Page 189
Negation......Page 192
Quantification and hiding......Page 193
Composition......Page 197
Factoring operations......Page 200
Promotion......Page 208
Free and constrained promotion......Page 211
The initialisation theorem......Page 216
Precondition investigation......Page 218
Calculation and simplification......Page 221
Structure and preconditions......Page 225
A programming interface......Page 232
Operations upon files......Page 233
A more complete description......Page 235
A file system......Page 237
Formal analysis......Page 242
Refinement......Page 248
Relations and nondeterminism......Page 251
Data types and data refinement......Page 256
Simulations......Page 259
Relaxing and unwinding......Page 263
Relations and schema operations......Page 272
Forwards simulation......Page 274
Backwards simulation......Page 285
Retrieve functions......Page 298
Functional refinement......Page 300
Calculating data refinements......Page 301
Refining promotion......Page 306
Refinement Calculus......Page 312
The specification statement......Page 313
Assignment......Page 314
Logical constants......Page 319
Sequential composition......Page 321
Conditional statements......Page 324
Iteration......Page 326
Specification: the external view......Page 336
Design: the sectional view......Page 337
Relationship between external and sectional views......Page 340
Enriching the model......Page 343
Processes......Page 346
Specification......Page 347
Chains......Page 351
Design......Page 354
Correctness of the design step......Page 359
Specification......Page 362
Design......Page 366
A retrieve relation......Page 367
Implementation......Page 375
Executable code......Page 378
Specification......Page 380
Design......Page 383
Further design......Page 387
Refinement to code......Page 391
Index......Page 396
Notation......Page 402
Resources......Page 404
This Book......Page 406
Thanks......Page 408