[CZT-Users] Problem typechecking OZ

[Stefan N. <Ste...@df...>]

Hi

I am a beginner in Z/OZ.
I used the czt eclipse plugin to write some Object-Z specification in
latex.
But it seems the typechecker for OZ has some problems with subclasses.

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}

\begin{class}{SList}
List
\begin{state}
\where
 head \in SElement\\
\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?

best regards
stefan