Using Z: Specification, Refinement, and Proof
This 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
What people are saying - Write a review
We haven't found any reviews in the usual places.
24 other sections not shown
abstract appear apply array associated begin binding booking bound BoxOffice buffer calculated called Chapter component concrete conjunction consider constant constraint contains corresponding count Customer data type defined definition denote described domain effect element empty equal equivalent Example exists expression false Figure finite formal function given global input introduce involves language logical london mathematical max_size means natural numbers notation object obtain operation output pair partial Person precondition predicate present produce promotion proof proposition prove quantifier range record refinement relation represent requires result retrieve rule satisfy schema seating secondary sequence simple simulation sold specification stack statement status successful Suppose symbol Table tree true variable write zero