Praxis der Softwareentwicklung (PSE)

Hintergrund

Programmbeweise zeigen die Konformanz von Programmen gegenüber ihrer Spezifikation. Die automatisierte Beweissuche stößt bei der Auswahl von zielführenden Schritten schnell an ihre Grenzen. In diesen Fällen sind Benutzer-Interaktionen, wie die Einführung von Lemmata oder Quantoreninstanziierungen, unabdingbar. Eine Mechanisierung dieser Interaktionen ist im Interesse des Nutzenden, um einen Beweis reproduzieren zu können. Dies wird durch Beweisskripte ermöglicht.

Beweisskripte sind Programme, die die Beweisesuche steuern und dabei die notwendigen Interaktionen zum Finden des Beweises dokumentieren. Beweisskripte bestehen aus Anweisungen für den Beweiser zur Steuerung des Kontrollfluss sowie Zuweisung von Variablen. Auf der anderen Seite führen Beweisskripte aber auch eine neue Indirektionsebene ein mit einem neuen Zustand. Z. B. gibt es damit drei Arten von Variablen, die es auseinander zu halten gilt: Logik-, Programm- und Skriptvariablen. Die Anwendenden müssen (a) das Programm und seine Zustände verstehen, (b) eine Beweisidee finden, sowie nun auch (c) diese Idee als Beweisskript umsetzen.

Dabei können Beweisskripte, analog zu Programmen, Fehler enthalten. Neben üblichen Syntaxfehler, können hier auch semantische Fehler auftreten, die sich durch ein falsches, unerwartetes Ergebnis manifestieren. Dies wäre in Beweiskripten das Anwenden von nicht-zielführenden Beweiserbefehlen. Um solche Fehler zu finden, benötigt der Nutzende die Möglichkeit, wie bei Programmen auch, Beweisskripte zu debuggen und dabei die Zustände, die durch das Beweissystem erzeugt werden nachzuvollziehen und zu inspizieren.

Aufgabenbeschreibung

Ziel dieses Projektes ist die Entwicklung eines Debuggers für Beweisskripte mit grafischer Benutzeroberfläche. Der Debugger soll folgende Komponenten umfassen:

• Interpreter für die Skriptsprache
• Editor für Beweisskripte
• Ansicht des Programmquelltextes
• Darstellung des Interpreter- und Beweiszustandes

Das Produkt sollte das Setzen von Breakpoints, und die typischen Navigationbefehle eines Debuggers (step-into, run to cursor, step return, step over, step-back) unterstützen. Des Weiteren müssen die Skript- und Beweiszustände für den Benutzenden grafisch aufbereitet werden. Dafür müssen die Elemente des Zustands geeignet dargestellt werden, z. B. Variablenbelegungen, die aktuelle Zeile im Skript und die ausgeführten Zeilen im Programm.

Umgesetzt werden soll dieses Projekt aufbauend auf die am Institut entwickelte Java-Verifikationsplattform KeY. Eine Schnittstelle zur Anbindung an KeY wird zur Verfügung gestellt.

Anforderungen

Die Softwareentwicklung soll nach den aktuellen Best-Practises umgesetzt werden unter Einsatz von

• Source Code Management,
• automatische Build-Tools,
• automatisierte Tests,
• kontinuierliche Integration (CI),
• Style Checkers und
• Design Patterns.

Dieses PSE-Projekt ist ein Forschungs-PSE und Teil des Forschungsvorhabens um das Softwareverifikationssystem KeY.