The Z Notation: A Reference Manual (Prentice-Hall International Series in Computer Science)

The Z Notation......Page 1
Table of Contents......Page 3
1.1 What is a formal specification?......Page 11
1.2 The birthday book......Page 13
1.3 Strengthening the specification......Page 17
1.4 From specifications to designs......Page 20
1.5 Implementing the birthday book......Page 21
1.6 A simple checkpointing scheme......Page 27
2.1 Objects and types......Page 34
2.1.2 Tuples and Cartesian product types......Page 35
2.1.3 Bindings and schema types......Page 36
2.1.4 Relations and functions......Page 37
2.2 Properties and schemas......Page 38
2.2.1 Combining properties......Page 39
2.2.2 Decorations and renaming......Page 40
2.2.3 Combining schemas......Page 41
2.3 Variables and scope......Page 44
2.3.1 Nested scopes......Page 45
2.3.2 Schemas with global variables......Page 46
2.4 Generic constructions......Page 48
2.5 Partially-defined expressions......Page 50
3.1 Syntactic conventions......Page 52
3.1.2 Operator symbols......Page 53
3.1.3 Layout......Page 56
3.2.1 Basic type definitions......Page 57
3.2.3 Constraints......Page 58
3.2.4 Schema definitions......Page 59
3.3 Schema references......Page 60
3.4 Declarations......Page 61
3.4.1 Characteristic tuples......Page 62
3.5 Schema texts......Page 63
3.6 Expressions......Page 64
3.7 Predicates......Page 77
3.8 Schema expressions......Page 84
3.9.1 Generic schemas......Page 89
3.9.2 Generic constants......Page 90
3.10 Free types......Page 92
3.10.1 Example: binary trees......Page 93
3.10.2 Consistency......Page 94
4 The Mathematical Tool-kit......Page 96
4.1 Sets......Page 99
4.2 Relations......Page 105
4.3 Functions......Page 115
4.4 Numbers and Finiteness......Page 118
4.5 Sequences......Page 125
4.6 Bags......Page 134
5.1 States and operations......Page 138
5.2 The delta and ksi conventions......Page 141
5.3 Loose specifications......Page 143
5.4 Sequential composition and piping......Page 144
5.5 Operation refinement......Page 145
5.6 Data refinement......Page 147
5.7 Functional data refinement......Page 150
6 Syntax Summary......Page 152
A Changes from the first edition......Page 157
B Glossary......Page 159
C Index of symbols......Page 163
Index......Page 164