This book contains enough material for three complete courses of study. It provides an introduction to the world of logic, sets and relations. It explains the use of the Z notation in the specification of realistic systems. It shows how Z specifications may be refined to produce executable code; this is demonstrated in a selection of case studies.
This book is both authoritative and comprehensive. It strikes the right balance between the formality of mathematics and the practical needs of industrial software development. It is faithful to the draft ISO standard for Z. It covers the essentials of specification, refinement, and proof, revealing techniques never previously published.
This book is based upon the experience of the authors in teaching Z to a wide variety of audiences. Many of their students have produced large, industrial specifications in Z; some have even produced their own textbooks. Sets of exercises, solutions, and transparency masters are available on the World-Wide Web.
| text | slides | exercises | solutions | cards | contents |