Home | english  | Impressum | Sitemap | KIT

Funktionsabschlüsse in Dynamischer Logik

Funktionsabschlüsse in Dynamischer Logik
Typ:Studienarbeit
Datum:2010
Betreuer:

Prof. P. H. Schmitt
Mattias Ulbrich
Benjamin Weiß

Bearbeiter:

Gregor Bethlen

Links:PDF
Errata

Funktionen sind Werte – dieser Gedanke liegt dem Konzept der Funktionstypen und Funktionsabschlüsse in imperativen Programmiersprachen zugrunde.

Diese Studienarbeit untersucht drei Entwürfe für Funktionsabschlüsse in Java, die derzeit diskutiert werden. In Ermangelung einer Entscheidung über die endgültige Umsetzung werden auch die Konzepte der Funktionsabschlüsse in C# und Scala betrachtet.

Eine einfache Sprache mit Funktionsabschlüssen wird definiert, um die Semantik von Funktionsabschlüssen verstehen zu können.

Außerdem wird eine Dynamische Logik für Programme dieser Sprache entwickelt, die also mithin Funktionsabschlüsse enthalten dürfen. Funktionsabschlüsse in Dynamischer Logik halten ein mehr oder weniger subtiles Problem bereit, aufgrund dessen es vorteilhaft ist, in der Logik eine Datenhalde zu modellieren.

Im Hinblick auf Kalkülregeln zur automatischen Verifikation von Programmen mit Funktionsabschlüssen werden Schemata äquivalenter Formeln dieser Logik aufgestellt und bewiesen. Die Funktionsabschlüsse werden hierbei durch das Ausrollen der Rümpfe behandelt.