Re: [CZT-Devel] Re: Object Z questions

[Timothy M. <ti...@cs...>]

Hi Petra,

> Hmm, then the oz_toolkit should not use the Z toolkit at all.
> For instance, we cannot use \fun but this shouldn't be a problem.
>
This is no problem... we can remove this. Although, I do seem to 
remember polymorphism and containment being added to the XML schema as 
("primitive") expressions, so no definition will be necessary in the oz 
toolkit. I don't seem to have included these in the scanner and parser 
yet though. It shouldn't be too difficult.

> Are you proposing to remove the given paragraph introducing \bool in the 
> Object-Z toolkit as well?
> This means we just do not support Object-Z specifications using \bool. 
> What is so complex about \bool?
> 
Yes, we should either remove it, or declare it something like:
   TRUE == [| true]
   FALSE == [| false]
   \bool == \{ TRUE , FALSE \}

The literals 'true' and 'false' are predicates and not expressions. 
Using these as expressions more or less makes Object-Z higher-order, and 
introduces many complexities. Even in the corejava class, for example, 
we would need TrueExpr and FalseExpr. For now it is fine to use the 
above definition, but I believe the reason languages such as Z and B do 
not have a boolean type is also that there is a philosophy that they do 
not provide anything useful. In the case where one might use a boolean 
type, a free type with the members 'PASS' and 'FAIL', or 'VALID' and 
'INVALID' make the specification more self-documenting. So maybe having 
a boolean type is not useful at all?

Cheers,
Tim