Table of contents
1Introduction 1
1.1Formal methods 1
1.2The CICS experience 2
1.3The Z notation 3
1.4The importance of proof 4
1.5Abstraction 5
2Propositional Logic9
2.1Propositional logic 9
2.2Conjunction 10
2.3Disjunction 13
2.4Implication 14
2.5Equivalence 17
2.6Negation 20
2.7Tautologies and contradictions 23
3Predicate Logic 27
3.1Predicate calculus 28
3.2Quantifiers and declarations 30
3.3Substitution 34
3.4Universal introduction and elimination 36
3.5Existential introduction and elimination 40
3.6Satisfaction and validity 43
4Equality and Definite Description 45
4.1Equality 45
4.2The one-point rule 48
4.3Uniqueness and quantity 50
4.4Definite description 52
5Sets 57
5.1Membership and extension 57
5.2Set comprehension 61
5.3Power sets 65
5.4Cartesian products 66
5.5Union, intersection, and difference 68
5.6Types 70
6Definitions 73
6.1Declarations 73
6.2Abbreviations 74
6.3Generic abbreviations 75
6.4Axiomatic definitions 77
6.5Generic definitions 79
6.6Sets and predicates 81
7Relations 83
7.1Binary relations 83
7.2Domain and range 85
7.3Relational inverse 88
7.4Relational composition 91
7.5Closures 93
8Functions 99
8.1Partial functions 99
8.2Lambda notation 101
8.3Functions on relations 103
8.4Overriding 105
8.5Properties of functions 107
8.6Finite sets 111
9Sequences 115
9.1Sequence notation 115
9.2A model for sequences 119
9.3Functions on sequences 122
9.4Structural induction 124
9.5Bags 128
10Free Types 133
10.1The natural numbers 133
10.2Free type definitions 135
10.3Proof by induction 140
10.4Primitive recursion 142
10.5Consistency 145
11Schemas 147
11.1The schema 147
11.2Schemas as types 152
11.3Schemas as declarations 154
11.4Schemas as predicates 158
11.5Renaming 160
11.6Generic schemas 162
12Schema Operators 165
12.1Conjunction 165
12.2Decoration 168
12.3Disjunction 174
12.4Negation 176
12.5Quantification and hiding 178
12.6Composition 182
13Promotion 185
13.1Factoring operations 185
13.2Promotion 193
13.3Free and constrained promotion 196
14Preconditions 201
14.1The initialisation theorem 201
14.2Precondition investigation 203
14.3Calculation and simplification 206
14.4Structure and preconditions 210
15A File System 217
15.1A programming interface 217
15.2Operations upon files 218
15.3A more complete description 220
15.4A file system 222
15.5Formal analysis 227
16Data Refinement 233
16.1Refinement 233
16.2Relations and nondeterminism 236
16.3Data types and data refinement 241
16.4Simulations 244
16.5Relaxing and unwinding 248
17Data Refinement and Schemas 257
17.1Relations and schema operations 257
17.2Forwards simulation 259
17.3Backwards simulation 270
18Functional Refinement 281
18.1Retrieve functions 281
18.2Functional refinement 283
18.3Calculating data refinements 284
18.4Refining promotion 289
19Refinement Calculus 295
19.1The specification statement 296
19.2Assignment 297
19.3Logical constants 302
19.4Sequential composition 304
19.5Conditional statements 307
19.6Iteration 309
20A Telecommunications Protocol 319
20.1Specification: the external view 319
20.2Design: the sectional view 320
20.3Relationship between external and sectional views 323
20.4Enriching the model 326
21An Operating System Scheduler 329
21.1Processes 329
21.2Specification 330
21.3Chains 334
21.4Design 337
21.5Correctness of the design step 342
22A Bounded Buffer Module 345
22.1Specification 345
22.2Design 349
22.3A retrieve relation 350
22.4Implementation 358
22.5Executable code 361
23A Save Area 365
23.1Specification 365
23.2Design 368
23.3Further design 372
23.4Refinement to code 376
Index 381
Notation 385
Resources 387
This Book 389
Thanks 391
text slides exercises solutions cards contents