The Way of Z: Practical Programming with Formal MethodsThis self-contained tutorial on Z presents realistic case studies emphasizing safety-critical systems, with examples drawn from embedded controls, real-time and concurrent programming, computer graphics, games, text processing, databases, artificial intelligence, and object-oriented programming. It motivates the use of formal methods and discusses practical issues concerning how to apply them in real projects. It also teaches how to apply formal program derivation and verification to implement Z specifications in real programming languages with examples in C. The book includes exercises with solutions, reference materials, and a guide to further reading. |
Contents
Formal methods | 3 |
12 What formal methods are not | 5 |
14 How can we use formal methods? | 6 |
15 Are formal methods too difficult? | 11 |
16 Formal methods at work | 12 |
Why Use Formal Methods? | 14 |
21 True stories | 15 |
22 Some popular fallacies | 16 |
153 Checking specifications | 154 |
154 Precondition calculation | 155 |
155 Formal reasoning and intuition | 159 |
Further reading | 161 |
Studies in Z | 163 |
Document control system | 165 |
Text processing | 169 |
172 A word counting utility | 171 |
23 Some hopeful alternatives | 18 |
Formal methods and project management | 21 |
32 Gathering requirements | 23 |
33 From informal requirements to formal specifications | 25 |
34 Validating formal specifications | 26 |
Further reading | 27 |
Introducing Z | 29 |
What is Z? | 31 |
A first example in Z | 33 |
From prose to Z control console | 39 |
61 Informal requirements | 40 |
62 Data flow diagram | 44 |
63 State transition diagram | 45 |
64 State transition table | 46 |
65 Z | 47 |
Introducing schemas text editor | 49 |
72 Axiomatic descriptions | 50 |
74 Initialization schemas | 51 |
75 Operation schemas | 52 |
76 Implicit preconditions | 53 |
77 Schema calculus | 55 |
78 The Way of Z | 56 |
Further reading | 59 |
Elements of Z | 61 |
Elements | 63 |
82 Expressions and operators | 71 |
83 Predicates equations and laws | 74 |
Structure | 78 |
92 Relations tables and databases | 80 |
93 Pairs and binary relations | 81 |
94 Functions | 88 |
95 Sequences | 93 |
96 Operators | 94 |
Logic | 96 |
103 Relations as predicates | 98 |
104 Logical connectives | 100 |
105 Logic and natural language | 105 |
106 Quantifiers | 106 |
107 Z and Boolean types | 108 |
108 Predicates and undefined expressions | 110 |
Synthesis | 112 |
112 Lambda expressions | 114 |
113 Some simple formal specifications | 115 |
114 Conveniences and shortcuts | 116 |
115 Modelling systems and change | 119 |
Schemas and schema calculus | 122 |
conjunction and disjunction | 127 |
123 Schemas everywhere | 132 |
124 Other schema calculus operators | 134 |
Schema types and bindings | 138 |
132 Using schema types and bindings | 142 |
Generic definitions and free types | 146 |
142 Free types | 148 |
Formal reasoning | 149 |
151 Calculation and proof | 150 |
152 Laws | 152 |
Eight queens | 174 |
Computer graphics and computational geometry | 180 |
Rulebased programming | 189 |
201 Elements of rulebased programming | 190 |
203 Deducing new facts | 191 |
204 Checking the rules | 193 |
205 Specifying rulebased programs | 194 |
206 Conclusion | 198 |
Graphical user interface | 199 |
212 Displays and dialogs | 200 |
213 Selecting a display | 202 |
214 Changing a setting value | 203 |
215 Z and state transition systems | 206 |
216 Changing the machine state | 208 |
217 Conclusions | 209 |
Safetycritical protection system | 211 |
222 Refinement | 214 |
223 Enforcing the safety requirements | 217 |
Modelling large systems | 218 |
232 Many subsystems | 221 |
233 Some useful idioms | 225 |
234 Subsystems conditions and modes | 227 |
235 Conclusion | 230 |
Objectoriented programming | 231 |
243 Objectoriented Z dialects | 233 |
Concurrency and real time | 234 |
252 Events | 237 |
253 Real time | 239 |
Further reading | 241 |
Programming with Z | 245 |
Refinement | 247 |
262 A refinement example | 248 |
263 Generalizing refinement | 251 |
264 Refinement strategies | 252 |
Program derivation and formal verification | 254 |
271 Axiomatic program derivation and verification | 255 |
272 Refinement calculus | 262 |
From Z to code | 265 |
282 State schemas | 268 |
283 Refinement from Z to code | 270 |
284 Functions and relations | 280 |
286 Schema expressions | 284 |
287 Modules and programs | 285 |
288 A larger example | 287 |
289 A final example | 290 |
Further reading | 297 |
A Glossary of Z notation | 299 |
B Omitted features | 304 |
C Operator precedence | 305 |
D The Z mathematical toolkit | 308 |
E Selected Laws | 316 |
F Solutions to selected exercises | 322 |
G Other formal notations | 326 |
| 328 | |
| 340 | |
Other editions - View all
Common terms and phrases
abbreviation appear apply assignment axiomatic definition beam binary relations bindings Boolean bound variable calculation called Chapter CHAR components conjunction cursor cyclotron data structures data type declarations deduce define describe diagram dialog disjunction display document domain doug Editor elements equation errors event example facts false formal methods formal notations formal specification formal verification formula free types Function application implemented integer integer square root interlock intlk iroot iroot(a logical connectives mainfld mathematical tool-kit maxsize mode mutex natural numbers nmax numbers object-oriented object-oriented programming operation schema pairs Param power supply precondition predicate problem programming language proof quantified predicate refinement calculus refinement law requirements rule-based programs schema calculus schema expression schema type segments sequence set comprehension setup Software Engineering subsystem symbol syntax transition true tuples usually write Z notation