[CZT-Users] Help with getting started II

[Pablo R. M. <rod...@gm...>]

Hi czt'ers,
I'm interested in exploit the power of zlive but I had problems trying to
load some .zed files.  When I tryed to load the following specification, I
received parsing errors related to the /defs latex command.

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


\begin{document}

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


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

\begin{schema}{InitBirthdayBook}
    BirthdayBook '
\where
    known' = \{ \}
\end{schema}

\begin{schema}{AddBirthday}
    \Delta BirthdayBook \\
    name?: NAME \\
    date?: DATE
\where
    name? \notin known
\\
    birthday' = birthday \cup \{name? \mapsto date?\}
\end{schema}

\begin{schema}{FindBirthday}
    \Xi BirthdayBook \\
    name?: NAME \\
    date!: DATE
\where
    name? \in known
\\
    date! = birthday(name?)
\end{schema}

\begin{schema}{Remind}
    \Xi BirthdayBook \\
    today?: DATE \\
    cards!: \power NAME
\where
    cards! = \{ n: known | birthday(n) = today? \}
\end{schema}

\begin{schema}{RemindOne}
    \Xi BirthdayBook \\
    today?: DATE \\
    card!: NAME
\where
    card! \in known \\
    birthday ~ card! = today?
\end{schema}


\begin{zed}
    REPORT ::= ok | already\_known | not\_known
\end{zed}

\begin{schema}{Success}
    result!: REPORT
\where
    result! = ok
\end{schema}

\begin{schema}{AlreadyKnown}
    \Xi BirthdayBook \\
    name?: NAME \\
    result!: REPORT
\where
    name? \in known \\
    result! = already\_known
\end{schema}


\begin{schema}{NotKnown}
    \Xi BirthdayBook \\
    name?: NAME \\
    result!: REPORT
\where
    name? \notin known \\
    result! = not\_known
\end{schema}

\begin{zed}
    RAddBirthday \defs (AddBirthday \land Success) \lor AlreadyKnown \\
    RFindBirthday \defs (FindBirthday \land Success) \lor NotKnown \\
    RRemind \defs Remind \land Success
\end{zed}


\end{document}




Then, I tried with the following, and I received typechecking errors that
undoubtely are related to the InitBirthdayBook schema.



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


\begin{document}

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


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


\begin{schema}{InitBirthdayBook}
    BirthdayBook '
\where
    known' = \{ \}
\end{schema}

\end{document}


Any help??
Thanks,
Pablo