Invited Presentation:

The Semantics of Object-Oriented Specification

Gordon Rose
Department of Computer Science, University of Queensland, Queensland 4072, Australia.
rose@cs.uq.oz.au

Abstract

Object orientation offers a scaleable means of implementing complex systems and provides a medium for reuse. As systems become more complex so do their specifications so that object orientation is also relevant to structuring specifications. It is not essential that an object-oriented specification be realised with an object-oriented implementation, although it is easier to relate a specification and its implementation if they have similar structures. The benefits of a library of class specifications are similar to those of class libraries for languages such as C++ or Eiffel, namely a source for direct reuse, for derivation using inheritance or for inclusion as attributes in other classes. However, there are additional benefits in a formal specification library in that properties (provable through the mathematical quality of formal specifications) can also be associated with retained classes.

The role of formal specification in modern software development is vital. The specification is the basis for validation with respect to requirements and for verification with respect to implementation. Verification in particular is a formal process and so requires a formal expression of the specification. The semantics of the formal specification language is therefore an essential aspect of a formal development methodology. If the language expressing what is required is not itself well defined, there is little hope that the developed system will behave as intended.

The presentation will outline some of the semantic issues of object-oriented formal specification as exemplified by the semantics of Object-Z, an object-oriented extension of Z, developed at the University of Queensland. The key issues of object orientation are encapsulation, object identity, inheritance, polymorphism and concurrency. Many people have contributed to Object-Z and research continues on library policy and retrieval, refinement, proofs based on axiomatic semantics and further semantic issues.

The numerous aspects of object orientation have provided a rich source for research. Moreover, the potential benefits of the combination of object orientation and formality, particularly for complex systems with critical components, have provided ample motivation. The need for tools has become apparent: a static-semantic checker (type checker) has been completed recently and further tools will follow.

Specific topics to be discussed are value vs reference semantics, the role of object identity, the implications of object identity aliases, containment relationships between objects, the interpretation of inheritance in the presence of renaming and redefinition, and the semantics of operations. The presentation will also cite axiomatic-semantic research and an Object-Z theory as a basis for proof construction assisted by a proof aid.

The presentation concludes with a cautionary note on the amount of time and effort required to develop, define and provide support for languages such as Z, CSP, CCS, etc. A particular challenge is to find a `good' semantic model. The Object-Z experience has been no exception to this.

Conference Home Page