Using Z.Specification,refinement,and proof

Jim Woodcock, Jim Davies9780139484728, 0139484728

This book contains enough mnaterial for three complete courses of study. It provides an introduction to the world of logic, sets and relations. It explains the use of the Znotation in the specification of realistic systems. It shows how Z specifications may be refined to produce executable code; this is demonstrated in a selection of case studies. The essentials of specification, refinement and proof are covered, revealing techniques never previously published. Exercises, Solutions and set of Tranparencies are available via http://www.comlab.ox.ac.uk/usingz.html

---

Table of contents :
Cover……Page 1
Contents……Page 3
Foreword……Page 9
Using this Book……Page 11
Acknowledgments……Page 13
Formal methods……Page 15
The CICS experience……Page 16
The Z notation……Page 17
The importance of proof……Page 18
Abstraction……Page 19
Propositional logic……Page 23
Conjunction……Page 24
Disjunction……Page 27
Implication……Page 28
Equivalence……Page 31
Negation……Page 34
Tautologies and contradictions……Page 37
Predicate Logic……Page 41
Predicate calculus……Page 42
Quantifiers and declarations……Page 44
Substitution……Page 48
Universal introduction and elimination……Page 50
Existential introduction and elimination……Page 54
Satisfaction and validity……Page 57
Equality……Page 59
The one-point rule……Page 62
Uniqueness and quantity……Page 64
Definite description……Page 66
Membership and extension……Page 71
Set comprehension……Page 75
Power sets……Page 79
Cartesian products……Page 80
Union, intersection, and difference……Page 82
Types……Page 83
Declarations……Page 87
Abbreviations……Page 88
Generic abbreviations……Page 89
Axiomatic definitions……Page 91
Generic definitions……Page 93
Sets and predicates……Page 95
Binary relations……Page 97
Domain and range……Page 99
Relational inverse……Page 102
Relational composition……Page 105
Closures……Page 108
Partial functions……Page 113
Lambda notation……Page 115
Functions on relations……Page 117
Overriding……Page 119
Properties of functions……Page 121
Finite sets……Page 125
Sequence notation……Page 129
A model for sequences……Page 133
Functions on sequences……Page 136
Structural induction……Page 138
Bags……Page 142
The natural numbers……Page 147
Free type definitions……Page 149
Proof by induction……Page 154
Primitive recursion……Page 156
Consistency……Page 159
The schema……Page 161
Schemas as types……Page 166
Schemas as declarations……Page 168
Schemas as predicates……Page 172
Renaming……Page 174
Generic schemas……Page 176
Conjunction……Page 179
Decoration……Page 182
Disjunction……Page 188
Negation……Page 191
Quantification and hiding……Page 192
Composition……Page 196
Factoring operations……Page 199
Promotion……Page 207
Free and constrained promotion……Page 210
The initialisation theorem……Page 215
Precondition investigation……Page 217
Calculation and simplification……Page 220
Structure and preconditions……Page 224
A programming interface……Page 231
Operations upon files……Page 232
A more complete description……Page 234
A file system……Page 236
Formal analysis……Page 241
Refinement……Page 247
Relations and nondeterminism……Page 250
Data types and data refinement……Page 255
Simulations……Page 258
Relaxing and unwinding……Page 262
Relations and schema operations……Page 271
Forwards simulation……Page 273
Backwards simulation……Page 284
Retrieve functions……Page 297
Functional refinement……Page 299
Calculating data refinements……Page 300
Refining promotion……Page 305
Refinement Calculus……Page 311
The specification statement……Page 312
Assignment……Page 313
Logical constants……Page 318
Sequential composition……Page 320
Conditional statements……Page 323
Iteration……Page 325
Specification: the external view……Page 335
Design: the sectional view……Page 336
Relationship between external and sectional views……Page 339
Enriching the model……Page 342
Processes……Page 345
Specification……Page 346
Chains……Page 350
Design……Page 353
Correctness of the design step……Page 358
Specification……Page 361
Design……Page 365
A retrieve relation……Page 366
Implementation……Page 374
Executable code……Page 377
Specification……Page 379
Design……Page 382
Further design……Page 386
Refinement to code……Page 390
Index……Page 395
Notation……Page 401
Resources……Page 403
This Book……Page 405
Thanks……Page 407