Ludwig-Maximilians-Universität München, Institute of Computer Science
Department of Programming and Software Engineering

DAAD Project VIGONI

Denotational Semantics for Concurrent Object-Oriented Languages

Our goal is to develop a denotational semantics of a concurrent object-oriented language and prove its adequacy and correctness. The use of monads and coalgebras as a basis for this semantics will ensure a high degree of modularity. We will also investigate an appropriate equivalence notion for programs of this language. Our results will be applied to Java as far as possible.

Object-oriented programming languages have been developed since the 1980's and have become indispensable for modern, distributed applications. Concerning their foundations by denotational (mathematical) and axiomatic (logical) semantics, however, no standard comparable to that for the traditional paradigmas of functional and imperative programming has been attained. These deficiencies become all the more apparent when concurrency and distribution enter the scene. We believe that disposing of a denotational semantics is most advantageous for understanding the underpinnings of the development of concurrent object-oriented systems and for its support by formal techniques. For example, the definition of a denotational semantics for the Object Constraint Language (OCL), which is part of the widely used Unified Modelling Language (UML), and formal investigations inspired by this definition, have uncovered several problems with OCL.

The goal of this project is therefore to develop a denotational semantics of an exemplary imperative, object-oriented language that includes concurrency. The language will embody the main concepts of Java and will be called L in the following. Our semantics will conform to standard criteria of quality, in particular it will be correct and adequate with respect to the operational semantics of L, and it will respect an appropriate notion of program equivalence. Concretely, we will address the following problems:

• Further development of the operational semantics of Java developed by our group, in particular the investigation of the relationship between our notion of event spaces and the standard concept of event structures. Replacing event spaces by a domain theoretic structure may suggest a denotational treatment of threads.
• denotational semantics
  • Definition of a (domain theoretic) denotational semantics for L.
  • Proof of correctness and adequacy of the denotational semantics with respect to the operational semantics.
  • We regard a modular approach as indispensable for the usability of our semantics. For this reason, we find it useful to base our theory on category-theoretic concepts such as computational monads for modularity and coalgebras for concurrency and encapsulation.
• observational equality
  • Definition of a notion of observational equality for L.
  • Proof of full abstractness, based on a suitable context lemma for L.
• analysis of the relevance of our results on L for Java

Project partners: Prof. Francesco Parisi-Presicce and Dr. Pietro Cenciarelli at the Universitá di Roma ``La Sapienza'',

Contact: Dr. Alexander Knapp, Dr. Dirk Pattinson.