PhD Thesis

This project received awards/funding from:

Richard Jago Memorial Prize (1995),
Australian Postgraduate Award (93-95),
UQ Computer Science Top-up Scholarship (93-95),
Germany NATO Science Committee Scholarship (1994),
SVRC Travel Scholarship (1994),
UQ Computer Science Conference Travel Support (93-95).

Under Roger Duke's supervision, the PhD project was completed in about two and half years.

Title: Formal Object Modelling Techniques and Denotational Semantics Study
thesis available in postscript

Abstract:

Formal descriptions of programming languages support language standardisation, program verification and software reliability. State-based formal specification languages such as VDM and Z have been used to define the denotational semantics of programming languages. Usually, the abstract syntax, static semantics and dynamic semantics of a programming language are defined separately and involve the construction of distinct formal structures. However, if the programming language is enhanced, extending the semantics may require modifications to each of the above structures. The general lack of modularity and reusability of the traditional denotational semantics representations has been recognised in the literature as a drawback. The main aim of this thesis is to apply an object-oriented approach to specify programming language semantics using the Object-Z notation. The key idea of this approach is to view programming language constructs, such as expressions and statements, as objects. With this approach, the abstract syntax, static semantics and dynamic semantics of an individual language construct are typically defined in one class such that the semantics representation is structural. Not only does this help the readability of the semantics, but if the language is enhanced the corresponding semantic modifications can be captured by minimal disruption of the existing semantics. Furthermore, it is also possible with this approach to reuse parts of the semantics specification of one programming language to define another.
Specifying programming languages in Object-Z not only leads to a more structured language semantic representation but also aids the development of the Object-Z notation itself. For instance, the use of the Object-Z notation to specify programming languages motivates the development of a generalised polymorphic construct, class-union, and the development of notations for capturing object containment in Object-Z. These new extensions to Object-Z not only play important roles in the object-oriented definition of programming languages but also prove to be useful for modelling object-oriented systems in general. This thesis presents these extensions together with the Object-Z specifications of programming languages.