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
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.