Utting, M. & Wang, S. (2002). Object orientation without extending Z. (Working paper series. University of Waikato, Department of Computer Science. No. 12/02/2002). Hamilton, New Zealand: University of Waikato.
Abstract
The good news of this paper is that without extending Z,
we can elegantly specify object-oriented systems, including encapsulation,
inheritance and subtype polymorphism (dynamic dispatch). The
bad news is that this specification style is rather different to normal
Z specifications, more abstract and axiomatic, which means that it is
not so well supported by current Z tools such as animators. It also enforces
behavioural subtyping, unlike most object-oriented programming
languages. This paper explains the proposed style, with examples, and
discusses its advantages and disadvantages.
