## 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 |

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### Contents

Introduction | 1 |

Propositional Logic | 9 |

Predicate Logic | 27 |

Copyright | |

24 other sections not shown

### Common terms and phrases

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