Re: [CZT-Users] Problem typechecking OZ

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

Hi Stefan,

You wrote:
> To reproduce my problem here a little spec:
> 
> \begin{class}{Element}
> \end{class}
> 
> \begin{class}{SElement}
> Element
> \end{class}
> 
> \begin{class}{List}
> \begin{state}
>  head : Element\\
>  tail : \power Element\\
> \end{state}
> \end{class}
> 
> The type checker returns
> 
> Type mismatch in membership predicate
>    Predicate: head \in SElement
>    LHS type: Element
>    RHS type: \power SElement
> 
> Is this a problem with the type checker in OZ or
> how can I define that the head of a SList is always a SElement?
> Thanks in advance?
> 
This is the correct behaviour, because head is in the class SElement, 
not in class Element. To declare head as an SElement, you can just use 
head : SElement, however, it is important that you understand the 
different between the Object-Z type system, and that of other 
object-oriented languages.

In your case, head \in SElement is not type-correct because the classes 
SElement and Element define disjoint sets of objects -- that is, an 
object cannot be of type SElement and Element. To declare that head is 
in either SElement OR Element, you can use class union

   head : SElement \classuni Element

which defines the union of all objects in SElement with all objects in 
Element.

Or better yet, use polymorphism:

   head : \poly Element

The above says that head is in the class Element *or any of Element's 
subclasses*. I think this is the semantics that you were intending.

Hope this helps,
Tim