Ludwig-Maximilians-Universität München, Institut für Informatik,
Lehr- und Forschungseinheit für Programmierung und Softwaretechnik

DAAD Projekt VIGONI

Denotationelle Semantik für objekt-orientierte Sprachen mit Nebenläufigkeit

Eine denotationelle Semantik einer nebenläufigen objektorientierten Sprache soll entwickelt und deren Adäquatheit und Korrektheit bewiesen werden. Durch die Verwendung von Monaden und Koalgebren soll ein hoher Grad an Modularität erreicht werden. Ein geeigneter Äquivalenzbegriff für Programme dieser Sprache ist ebenfalls Gegenstand der Untersuchungen. Die Ergebnisse werden soweit möglich auf Java übertragen.

Objektorientierte Programmiersprachen sind seit den 80er Jahren entwickelt worden und inzwischen aus modernen, verteilten Anwendungen der industriellen Informationstechnik nicht mehr wegzudenken. Im Gegensatz zu den traditionellen Paradigmen der funktionalen und imperativen Programmierung ist, was die denotationelle (mathematische) und die axiomatische (programmlogische) Semantik betrifft, hier allerdings noch kein vergleichbarer Standard erreicht worden. Dies trifft um so mehr zu, wenn man Nebenläufigkeit und Verteiltheit einbezieht. Eine denotationelle Semantik ist jedoch äußerst vorteilhaft, um die Entwicklung objektorientierter und verteilter Systeme besser verstehen und formale Techniken zu ihrer Unterstützung einsetzen zu können. Als Beispiel sei hier die Object Constraint Language (OCL) genannt, die Teil der weitverbreiteten Modellierungs- und Softwarebeschreibungssprache UML (Unified Modeling Language) ist; durch Angabe einer denotationellen Semantik und die daraus folgenden Untersuchungen konnten einige Schwierigkeiten aufgedeckt werden.

Ziel des Projektes ist es daher, eine denotationelle Semantik einer beispielhaften objektorientierten imperativen Sprache mit Nebenläufigkeit zu entwickeln. Die Sprache soll konzeptionell die wichtigsten Eigenschaften von Java enthalten und wird im folgenden mit L bezeichnet. Die denotationelle Semantik soll dabei gewissen Qualitätskriterien genügen, d.h. korrrekt und adäquat bzgl. der operationellen Semantik sein und verträglich mit einem geeigneten Begriff von Programmäquivalenz. Dazu sollen folgende Teilaufgaben untersucht werden.

• Weiterentwicklung der in angegebenen operationellen Semantik von Java, d.h. Untersuchung der Beziehung zwischen den dort verwendeten Ereignisräumen und den klassischen Event Structures. Das Ersetzen der Ereignisräume durch eine bereichstheoretische Struktur könnte Hinweise für eine denotationelle Behandlung der Threads geben.
• Denotationelle Semantik
  • Definition einer (bereichstheoretischen) denotationellen Semantik für L.
  • Beweise der Korrektheit und Adäquatheit der denotationellen Semantik bzgl.der operationellen Semantik.
  • Bei obengenannten Punkten wäre zum Zwecke einer einfacheren Handhabnung ein modularer Ansatz wünschenswert. Wir erachten den Einsatz kategorieller Hilfsmittel wie Monaden (Computational Monads) für die Modularität sowie Koalgebren für die Nebenläufigkeit und für die Datenkapselung als nützlich und werden diese soweit möglich auch verwenden.
• Beobachtbare Gleichheit
  • Entwicklung eines Begriffs von beobachtbarer Gleichheit für L.
  • Beweis der vollen Abstraktheit unter geeigneter Definition eines Kontextlemmas für L.
• Für alle Punkte: Analyse der Bedeutung der Ergebnisse über L für Java.

Projektpartner: Prof. Francesco Parisi-Presicce und Dr. Pietro Cenciarelli von der Universitá di Roma ``La Sapienza'',

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