Java-Spezifikationen mit eingebetteten Beweisen

Typ:	MA
Datum:	2023-01-21
Betreuer:	Mattias Ulbrich Wolfram Pfeifer
Aushang:

Hintergrund

Ziel bei der deduktiven Programmverifikation ist es, mithilfe formaler Methoden zu beweisen, dass Software eine gegebene Spezifikation erfüllt. KeY ist ein am Lehrstuhl entwickeltes Tool zur deduktiven Verifikation von Java-Programmen.

Herausforderung

Obwohl das Finden eines Beweises im Allgemeinen ein unentscheidbares Problem ist, können in der Praxis oftmals mithilfe von Heuristiken automatisch Beweise gefunden werden. In vielen Fällen ist KeY aber auch auf Benutzerinteraktion angewiesen, um die nötigen Schritte, die einen Beweis schließen, zu finden. KeY unterstützt solche Interaktionen in seiner grafischen Oberfläche. Oftmals muss nahezu derselbe Beweis aber mehrfach geführt werden, z. B. während des Entwickelns einer korrekten Spezifikation. Um das möglichst weit zu automatisieren, wurde am Lehrstuhl eine Skriptsprache entwickelt, die die nötigen Interaktionen beschreibt. Diese arbeitet allerdings mit der internen Logik von KeY und ist deshalb schwierig zu bedienen.

In dieser Arbeit möchten wir die Beweissteuerung in die Spezifikationssprache einbetten. Das erlaubt es dem Benutzer, Beweissteuerung und Spezifikation auf derselben logischen Ebene durchzuführen.

Aufgabe:

Ziel der Arbeit ist die Konzeption und Ausarbeitung eines Formats für eine in die Java Modeling Language (JML) eingebettete Skriptsprache für Beweise sowie die Implementierung dieser Art der Beweissteuerung in KeY. Dabei kann auf eine existierende Beweis-Skriptsprache zurückgegriffen werden.

Ihr Profil:

Sie sollten solide Java-Kenntnisse besitzen sowie das Modul Formale Systeme erfolgreich abgeschlossen haben.