The Way of Z: Practical Programming with Formal Methods

Front Cover
Cambridge University Press, 1997 - Computers - 350 pages
1 Review
This 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.
 

What people are saying - Write a review

User Review - Flag as inappropriate

GOOD

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
Bibliography
328
Index
340
Copyright

Other editions - View all

Common terms and phrases

References to this book

Software-Qualität
Dirk W. Hoffmann
No preview available - 2008
All Book Search results »

About the author (1997)

Jonathan Jacky is a research scientist at the University of Washington in Seattle. He is experienced in embedded control systems, safety-critical systems, signal processing, and scientific computing. He has taught at the Evergreen State College and has been a visiting researcher at Microsoft Research. He is the author of The Way of Z: Practical Programming with Formal Methods.

Bibliographic information