Re: [CZT-Users] how to ?

[Petra M. <Pet...@ec...>]

Hi Massimo,

Object-Z supports polymorphism via class union and polymorphic
declarations (see Object-Z books for details). In the example

\begin{class}{Account}
\end{class}

\begin{class}{SavingsAccount}
Account
\end{class}

\begin{class}{Bank}
\begin{state}
  accts: \power (\poly Account)
\end{state}
\end{class}

accts can contain SavingsAccounts as well as normal Accounts.

There are polymorphic extensions to Object-Z
(see Waheed, Khan, Nadeem: Polymorphic Extensions to Object-Z
specifications), which claim to provide better support for polymorphism
but are not supported in CZT yet.

Hope this helps,
Petra