The Semantics of Object-Oriented Specification
Gordon Rose
Department of Computer Science,
University of Queensland,
Queensland 4072, Australia.
rose@cs.uq.oz.au
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.