Re: [CZT-Users] Typechecker: cyclic definition of schema's

[Tim M. <T.M...@li...>]

nelis wrote:
> Thank you for your quick answer. Alas this does not seem to work. I 
> changed the extension of the file, and it still refuses to accept this 
> definition. I think JEdit is correctly using the Object-z parser (since 
> it mentions the parser in the status bar when it is finished).
> 
I've just installed the jEdit plugin, and you are right: it is 
using the Object-Z parser, but use before declaration is not 
enabled. I had a quick look at the code, and I can't figure out 
where this property is set.

Petra, are you able to help with this? Also, if this property is 
not able to be changed via the interface, do you object to me 
adding this to the options in the zsidekick?

> Questions:
> 2. Are there constructs that only exist in Object-z so that I can test 
> that it effectively uses the Object-z parser?

I think you are using the Object-Z tools, but try the following 
specification:

\begin{class}{C}
\end{class}

\begin{zed}
   D == C
\end{zed}

The Object-Z typechecker will allow this, but the Z typechecker 
will raise an error that the name "C" is undeclared.

> 3. If you don't use this JEdit plugin, how do you specify your Z 
> documents in a practical way?
> 
I use a text editor and then typecheck the specification on the 
command line (in unix):

java -jar czt.jar zedtypecheck filename.tex

If you want to enable use before declaration, use the -d flag, 
like so:

java -jar czt.jar zedtypecheck -d filename.tex

The above reports no errors for your example.

The other option is to use the CZT plugin for Eclipse 
(http://www.cs.waikato.ac.nz/~marku/czt/eclipse.html), but I'm not 
sure whether that will solve your use before declaration problem.

Cheers,
Tim