Parallele Systeme
Logische Charakterisierung relationaler Semantik
| Beginn: Ab sofort möglich. AnsprechpartnerIn: Eike.Best Voraussetzungen: Keine besonderen Vorkenntnisse erforderlich. Kurzbeschreibung: In dieser theoretischen Arbeit sollen logische Charakterisierungen relationaler Semantiken entwickelt werden. |
Beschreibung
Die relationale Semantik eines sequentiellen Programms P ist die Relation zwischen Eingangs- und Ausgangszuständen, die durch P hergestellt wird. Man möchte die Enthaltenseinsbeziehung der Relationen zweier Programme logisch dadurch charakterisieren, daß eine Aussage über die Eigenschaften gemacht wird, die von den beiden Programmen erfüllt werden. In der Literatur sind viele solcher Charakterisierungen bekannt. In Eike Best and Kerstin M. Richter: Relational Semantics Revisited. Berichte aus dem Fachbereich Informatik 2/99 (Februar 1999) sind drei neuartige Definitionen relationaler Semantik zu finden, deren Besonderheit darin besteht, daß der Error-Zustand so wenig wie möglich vorkommt. Für diese Semantiken sind logische Charakterisierungen anzugeben.
Als Studienarbeit stellt dies eine einfache
Anwendung bekannter Verfahren (Hoare-Logik)
auf existierende Definitionen dar.
Als Diplomarbeit kommt noch die Untersuchung des
Gesamtspektrums der relationalen Semantiken hinzu.
Es sind auch Überlegungen anzustellen, wie
die einzelnen Definitionen sich aus Prinzipien
ergeben, so daß sie weniger ad hoc erscheinen.