- Forward


Recording Requirements in Z
A Brief Introduction


Prof. David Bernstein
James Madison University

Computer Science Department
bernstdh@jmu.edu

Print

Overview
Back Forward
  • Pronunciation:
    • zed
  • Approach:
    • Uses first-order predicate logic and set theory
  • Problems:
    • Impossible for clients/customers to learn
An Example State Space Schema
Back Forward
  • images/zedexample1a.gif
  • 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
Back Forward
  • images/zedexample1b.gif
  • 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
There's Always More to Learn
Back -