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:
Project partners: Prof. Francesco Parisi-Presicce and Dr. Pietro Cenciarelli at the Universitá di Roma ``La Sapienza'',
Contact: Dr. Alexander Knapp, Dr. Dirk Pattinson.