AktuellIntegration von JML in das KIV-System
Ansprechpartner: Kurt Stenzel
Ausgangssituation:
JML, die Java Modeling Language, ist ein Spezifikationssprache zur Annotation von Java Programmen. Die Idee ist, Eigenschaften von Java Programmen formal im Code zu beschreiben (der Code wird annotiert). Die Spezifikationssprache hat dabei die gleich Syntax wie Java selbst, sollte daher für Java-Programmierer leicht erlernbar sein. Beispiele für Eigenschaften sind etwa, dass ein bestimmter Wert immer größer 0 ist, dass eine Methode korrekt eine Liste sortiert, oder dass eine Methode niemals eine NullPointerException wirft. JML hat eine große internationale Community und wird weltweit auf unterschiedlichste Art und Weise eingesetzt.
Das KIV-System ist ein Verifikationssytem, das am Lehrstuhl entwickelt wurde und wird, und die Verifikation von Java-Programmen erlaubt. Das KIV-System unterstützt aber nicht JML, sondern Eigenschaften werden in einer eigenen Syntax separat (d. h. nicht direkt im Source-Code) formuliert.
Ziel der Arbeit:
In dieser Arbeit soll das KIV-System um JML erweitert werden, d. h. es soll möglich sein, in JML Java Source-Code zu annotieren und die Eigenschaften mit dem KIV-System nachzuweisen. Konkrete Aufgaben sind
- Anschluss eines existierenden (als open source verfügbaren, in Java programmierten) JML Parsers
- Umsetzung der JML-Sprachkonstrukte in semantisch äquivalente KIV-Konstrukte
- Validierung der Implementierung durch das Beweisen kleiner Beispiele
Voraussetzungen:
- Sehr gute Java-Kenntnisse
- Kenntnisse im Bereich formaler Methoden / Lehrveranstaltung Beweisbar korrekte Software
Zeitrahmen:
Beginn: ab Oktober