I have written a Z specification and drawn boxes around the schemas. I'm trying to work out how to draw an arrow from schema to schema.
\documentclass{article}
\usepackage{zdra}
\begin{document}
\zlemma{
\begin{schema}{BirthdayBook}
known: \power NAME \\
birthday: NAME \pfun DATE
\where
\postcon{known=\dom birthday}
\end{schema}
}
\text{
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.}
\zlemma{
\begin{schema}{InitBirthdayBook}
BirthdayBook~'
\where
\postcon{known' = \{ \}}
\end{schema}
}
\end{document}
I've got the boxes around the schema's fine it's just the arrow i need from box to box.
The packages needed for this to compile can be found here http://www.macs.hw.ac.uk/~lb89/packages/