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.
Permanent Research Commons link: http://hdl.handle.net/10289/71
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.