\documentclass{article}
\usepackage{oz}   % oz or z-eves or fuzz styles
\newenvironment{machine}[1]{
    \begin{tabular}{@{\qquad}l}\textbf{\kern-1em machine}\ #1\\ }{
    \\ \textbf{\kern-1em end} \end{tabular} }
\newcommand{\machineInit}{\\ \textbf{\kern-1em init} \\}
\newcommand{\machineOps}{\\ \textbf{\kern-1em ops} \\}

\begin{document}
This is the BirthdayBook specification, from 
Spivey~\cite{spivey:z-notation2}.  We extend it slightly
by adding an extra operation, $RemindOne$, that is non-deterministic.

%    [NAME, DATE] 
\begin{zed}
   NAME == 1 \upto 5
\end{zed}
\begin{zed}
   DATE == 10 \upto 15
\end{zed}

The $BirthdayBook$ schema defines the \emph{state space} of 
the birthday book system. 

\begin{schema}{BirthdayBook}
    known: \power NAME \\
    birthday: NAME \pfun DATE
\where
    known=\dom birthday
\end{schema}

This $InitBirthdayBook$ specifies the initial state
of the birthday book system.  It does not say explicitly that
$birthday'$ is empty, but that is implicit, because its domain
is empty.

\begin{schema}{InitBirthdayBook}
    known: \power NAME \\
    birthday: NAME \pfun DATE
\where
    known =\dom birthday \\
    known = \{ \}
\end{schema}

Next we have several operation schemas to define the normal (non-error)
behaviour of the system.

\begin{schema}{AddBirthday}
    known, known': \power NAME \\
    birthday, birthday': NAME \pfun DATE \\
    name?: NAME \\
    date?: DATE
\where
    known = \dom birthday \\
    known' = \dom birthday' \\
    name? \notin known
\\
    birthday' = birthday \cup \{name? \mapsto date?\}
\end{schema}

\begin{schema}{FindBirthday}
    known, known': \power NAME \\
    birthday, birthday': NAME \pfun DATE \\
    name?: NAME \\
    date!: DATE 
\where
    known = \dom birthday \\
    known' = \dom birthday' \\
    known' = known \\
    birthday' = birthday \\
    name? \in known
\\
    date! = birthday(name?)
\end{schema}

\begin{schema}{Remind}
    known, known': \power NAME \\
    birthday, birthday': NAME \pfun DATE \\
    today?: DATE \\
    cards!: \power NAME
\where
    known = \dom birthday \\
    known' = \dom birthday' \\
    known' = known \\
    birthday' = birthday \\
    cards! = \{ n: known | birthday(n) = today? \}
\end{schema}

This $RemindOne$ schema does not appear in Spivey, but is
included to show how non-deterministic schemas can be animated.
It reminds us of just one person who has a birthday on the given 
day.
\begin{schema}{RemindOne}
    known, known': \power NAME \\
    birthday, birthday': NAME \pfun DATE \\
    today?: DATE \\
    card!: NAME
\where
    known = \dom birthday \\
    known' = \dom birthday' \\
    known' = known \\
    birthday' = birthday \\
    card! \in known \\
    birthday ~ card! = today?
\end{schema}


% \bibliographystyle{plain}
\bibliography{spec}
\begin{thebibliography}{1}
\bibitem{spivey:z-notation2}
J.~Michael Spivey.
\newblock {\em The Z Notation: A Reference Manual}.
\newblock International Series in Computer Science. Prentice-Hall International
  (UK) Ltd, second edition, 1992.
\end{thebibliography}
\end{document}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: t
%%% End: