文档介绍：Using Z
Specification, Refinement, and Proof
Jim Woodcock
University of Oxford
Jim Davies
University of Oxford
Copyright: this hypertext version of Using Z is easily copied, distributed, and
printed; if you choose to do this, we would ask you to remember that it is under
copyright: if you reproduce any of the material, please include an appropriate
acknowledgement, and—if you find the material useful—please encourage us
(and our publishers) by buying a copy of the book.
Contents
Foreword xi
Using this Book xiii
Acknowledgments xv
1 Introduction 1
Formal methods 1
The CICS experience 2
The Z notation 3
The importance of proof 4
Abstraction 5
2 Propositional Logic 9
Propositional logic 9
Conjunction 10
Disjunction 13
Implication 14
Equivalence 17
Negation 20
Tautologies and contradictions 23
3 Predicate Logic 27
Predicate calculus 28
Quantifiers and declarations 30
Substitution 34
vi
Universal introduction and elimination 36
Existential introduction and elimination 40
Satisfaction and validity 43
4 Equality and Definite Description 45
Equality 45
The one-point rule 48
Uniqueness and quantity 50
Definite description 52
5 Sets 57
Membership and extension 57
prehension 61
Power sets 65
Cartesian products 66
Union, intersection, and difference 68
Types 69
6 Definitions 73
Declarations 73
Abbreviations 74
Generic abbreviations 75
Axiomatic definitions 77
Generic definitions 79
Sets and predicates 81
7 Relations 83
Binary relations 83
Domain and range 85
Relational inverse 88
position 91
Closures 94
8 Functions 99
Partial functions 99
Lambda notation 101
Functions on relations 103
Overriding 105
Properties of functions 107
Finite sets 111
vii
9 Sequences 115
Sequence notation 115