[CZT-Users] define a lattice in Object-Z

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

Hello, 

I am writing an Object-Z specification in latex and want to define a lattice. 
Could someone please look at the example below and tell me if this is correct?


\begin{class}{Test}
\\
\begin{state}
r :  \mathbb{P} \ ROLE\\
rh: (r, \geq)
\ST
rh : nurse \geq doctor  \geq chief physician
\end{state} \\
\begin{init}
r = \left\{nurse, doctor, chief physician\right\}\\
rh = \left\{(nurse, doctor), (doctor, chief physician)\right\}
\end{init} \\
\end{class}

r : set of roles in a hospital 
RH : role hierarchy in a hospital (lattice)


Thanks a lot for your help!





Kind regards, 

Janine