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

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

Hi Janine,

Sure. Decidability is not a small topic, and it is not one that I have a 
good handle on myself. Basically, Object-Z is built on a first-order 
logic that is not decidable. This means that there is no algorithm than 
can determine whether an Object-Z predicate is true or not, for all 
Object-Z predicates. There are algorithms that can determine that *some* 
predicates are true, but it is impossible that an algorithm can 
determine this for all predicates in the language. You can read about 
decidability on wikipedia: http://en.wikipedia.org/wiki/Decidability_(logic)

The consequence for you is that, if we cannot determine whether some 
predicates are true, then automatically translating such predicates into 
programs that terminate would also be impossible.

I hope that helps.

Regards,
Tim

On 01/06/12 07:34, Janine Seifert wrote:
> 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 <mailto:tm...@un...>
>     *To:* Janine Seifert <mailto:ma...@ja...>
>     *Cc:* czt...@li...
>     <mailto: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