State-Based Formal Methods for Distributed Processing: From Z to Object-Z

In this paper, we look at state-based specification notations and how they may be extended with concepts from object orientation. In particular, we focus on the Z specification language and one of its object-oriented extensions Object-Z. The state-based paradigm is introduced by specifying an ODP trader object in Z. The paper provides an overview of other state-based notations and discusses how such notations have been extended to support object orientation. Finally, we present a specification of the ODP trading function in Object-Z