Re: [CZT-Users] typchecking oz error mesages + convert oz to java/c++

[Tim M. <tm...@un...>]

Hi Janine,

> I am a beginner in OZ and the CZT eclipse plugin. I am writing an
> Object-Z specification in latex, but the typchecker reports some errors.
> Could someone please explain me the error messages?
>
The CZT tools (including the Object-Z ones) are based on the Z standard. 
Much of the Object-Z literature was written prior to the Z standard, so 
there are some catches that you'll have to be aware of.

The errors you see are:

- There is no "\real" set in standard Z. You can create one using:

%%Zword \real real

\begin{axdef}
   \real : \power \arithmos
\end{axdef}

  The first line tells the parser some stuff, and the paragraph below 
declares \real as a power set of 'arithmos' -- the base numbers in 
standard Z.

- The problem with the 'colour' variable is that all paragraphs in an 
Object-Z specification must be declared as standard Z paragraphs. So 
you'll need to use an axdef for that the same way that you did for the 
variable 'perim'.

Fixing these results in another problem: you'll need a '\where' symbol 
between the line that declares dx? and dy?, and the predicate that uses 
them.

> Am I right that the CTZ Tools are not able to convert the OZ code to
> Java/C++ ? If thats the case, could you point me to a tool or lib that
> is able to accomplish that task? I not only need to typecheck my OZ code
> but also have to convert it to C++ code/classes.
>
You're right that CZT doesn't do this. I've not heard of a tool that 
does, and in any case, the conversion would be highly restricted because 
Object-Z is undecidable.

I hope this helps.

Regards,
Tim