\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: