Using Z: Specification, Refinement, and Proof
This book covers all aspects of the Z notation, including specification, rigorous and formal proof, and refinements into code. It sets out to explain the principles and practice of formal development of programs using Z.
What people are saying - Write a review
We haven't found any reviews in the usual places.
abstract data type AMemory array bijection binding box office system BoxOffice buffer calculated Cartesian product Chapter component concrete conjunction constraint contains corresponding count Customer declaration defined definition described digits disjunction domain element empty empty set equivalent Example existential quantifier expression f f f false FileDoesNotExist finite flatten following schema formal formal methods forwards simulation free type global implementation induction inference rules initialisation injective functions input introduce invariant ListRetrieveSet logical logical constant mailbox maplet mathematical mod maxsize natural numbers notation nullPId object one-point rule operation schema output p a q pair postcondition precondition predicate proof proposition prove Purchaseo record refinement refinement calculus relational composition requires result retrieve relation schema type SchemaTwo seating secondary seq Bit sequence seqX sold specification statement stack status subset surjective surjective function symbol target ticket total function true tuple universal quantifier variable write zero