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

[Janine S. <ma...@ja...>]

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