|
From: Janine S. <ma...@ja...> - 2012-05-31 21:46:48
|
Hi Tim,
thanks a lot for the quick and useful reply. I did not got the point regarding the undecidability of Object-Z. Could you please explain this more in detail or point me to a resource that could help me in understanding it.
Regards,
Janine
----- Original Message -----
From: Tim Miller
To: Janine Seifert
Cc: czt...@li...
Sent: Thursday, May 31, 2012 3:45 AM
Subject: Re: [CZT-Users] typchecking oz error mesages + convert oz to java/c++
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
|