Recording Requirements in Z

JMU

Recording Requirements in Z
A Brief Introduction

Prof. David Bernstein
James Madison University

Computer Science Department

bernstdh@jmu.edu

Overview

Pronunciation:
- zed
Approach:
- Uses first-order predicate logic and set theory
Problems:
- Impossible for clients/customers to learn

An Example State Space Schema

known is the set of names in the book
birthday is a function that maps from names to birthdays
Invariant: known is always the domain of the set birthday

An Example Operation Schema

The operation results in a state change
Their are two inputs (name? and date?)
Precondition: name? must not be known
If Precondition Satisfied: birthday is extended to include the new mapping