Home | english  | Impressum | Sitemap | KIT

A Calculus for Data Abstraction

A Calculus for Data Abstraction
Typ:Diplomarbeit
Datum:2009
Betreuer:

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

Bearbeiter:

Roman Krenický

Links:PDF

Im Bereich der Programmverifikation stehen Informatiker immer wieder vor neuen Herausforderungen. Eine der wichtigsten ist als frame problem bekannt. Es ist die Frage danach, welche Teile des Programmzustands (der im wesentlichen im Heap gespeichert ist) durch eine gegebene Aktion verändert werden, oder vielmehr, welche nicht, bzw. wie diese Information abgeleitet oder spezifiziert werden kann. Im Zusammenhang mit abstrakten Spezifikationen, wie sie sich z. B. im objektorientierten Umfeld durch Vererbung ergeben können, bekommt das frame problem eine neue Qualität. Spezifikationen für Elternklassen sollen oft auch das Verhalten aller (potentiellen) Kindklassen umfassen, ohne letztere explizit zu kennen. Ein vielversprechender Lösungsansatz ist die Benutzung von Datenabstraktion zusammen mit expliziten Abhängigkeiten. Hierbei werden für Spezifikationszwecke spezielle Variablen, Funktionen oder Prädikate eingeführt, die keine konkreten Programmdaten modellieren (Datenabstraktion), und mithilfe spezieller Konstrukte kann man angeben, welche Daten oder Aktionen ihrenWert beeinflussen (explizite Abhängigkeiten). Dieser Ansatz wird u. a. für das  Programmverifikationswerkzeug KeY in Erwägung gezogen.

Inhalt dieser Diplomarbeit ist die Untersuchung, inwiefern solche abstrakten Spezifikationsfunktionen (Observer) und expliziten Abhängigkeiten in KeY genutzt werden können, um auf syntaktischer Ebene logische Ausdrücke zu vereinfachen und mit rein syntaktischen Mitteln logische Schlüsse zu ziehen. Hierzu wird ein bereits eingesetztes Termersetzungssystem erweitert und anschließend analysiert.

BibTeX

@misc{Krenicky2009,
  author       = {Roman Krenick\'y},
  title        = {A Calculus for Data Abstraction},
  howpublished = {Diplomarbeit, Fakult{\"a}t f{\"u}r Informatik, Universit\"at Karlsruhe},
  year         = {2009}
}