Re: [CZT-Users] Help with getting started II

[<pe...@cs...>]

Hi Pablo,

> When I tryed to load the following specification, I
> received parsing errors related to the /defs latex command.

CZT implements ISO standard Z, which doesn't use "/defs"; please use "=="
instead.

> Then, I tried with the following, and I received typechecking errors that
> undoubtely are related to the InitBirthdayBook schema.
> [...]
> \begin{schema}{InitBirthdayBook}
>     BirthdayBook '
> \where

The decoration on the BirthdayBook reference must be separated from the
schema name.  It is not sufficient to just have a space there, you need to
have a hard space: "BirthdayBook~".

See also http://www-users.cs.york.ac.uk/~ian/cadiz/standard.html for a
list of differences between ISO Z and Spivey's Z Reference Manual.

Hope that helps,
Petra