Using Z: Specification, Refinement, and ProofThis book contains enough mnaterial for three complete courses of study. It provides an introduction to the world of logic, sets and relations. It explains the use of the Znotation 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. The essentials of specification, refinement and proof are covered, revealing techniques never previously published. Exercises, Solutions and set of Tranparencies are available via http://www.comlab.ox.ac.uk/usingz.html |
Common terms and phrases
abstract data type array assignment introduction backwards simulation bijection binding box office system BoxOffice buffer calculated Cartesian product Chapter component concrete constraint corresponding count Customer declaration defined definition denote described digits domain element empty empty set equivalent Example existential existential quantifier expression file system FileDoesNotExist finite flatten following schema formal forwards simulation free type global induction initialisation injective functions introduce invariant KeyRead language ListRetrieveSet logical constant mailbox maplet mathematical mod max_size natural numbers notation nullPId one-point rule operation schema pair postcondition precondition predicate PriData promotion schema proof quantified record refinement refinement calculus relational composition requires result retrieve relation san_francisco save_area schema type SchemaOne SchemaTwo secondary seq Bit sequence specification statement stack status subset succ surjective function target ticket total function totalised true tuple universal quantification variables Z notation zero