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

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

nelis wrote:
> I want to define something like:
> 
> \begin{schema}{SUBSTRUCTURE}\\
>  components : \power COMPONENT \\
>  connectors : \power CONNECTORS \\
>  links : \power LINKS \\
>  interfaceMappings : \power INTERFACEMAPPING
> \end{schema}
> 
> \begin{schema}{COMPONENT}\\
>  identifier : IDENTIFIER \\
>  description : TEXT \\
>  interfaces : \power INTERFACE \\
>  subStructure : SUBSTRUCTURE
> \end{schema}
> 
> But I get the follow problem: the typechecker seems unable to handle a 
> schema definition that relies on a schema that is specified further in 
> the document. Like in the example, Substructure can not rely on the 
> definition of component.
> 
Just as a note, the above is not permitted by Z. The scope of the
schema SUBSTRUCTURE is restricted only to the paragraphs that have
been declared before it; that is, Z does not permit use before
declaration, except in the special case of recursive given types.

However! ... I have implemented the CZT typechecker such that it
allows users to turn on use before declaration. I'm not sure how
to turn this on from the jedit plugin (I don't use that particular
plugin -- someone else on the project may be able to answer that),
but for now, the easiest way is if you change the file extension
of your specifications to .oz (e.g. from file.tex to file.oz).
Then the jedit plugin will automatically use the Object-Z
typechecker, which has use before declaration enabled by default,
and the above should then typecheck without problems.

Cheers,
Tim