Sommersemester 2017

Praxis der Softwareentwicklung

Prof. Dr. Bernhard Beckert
Sarah Grebing, Alexander Weigl

Aktuelles

  • 20.03.2017: Bekanntgabe des Themas

Allgemeines

In "Praxis der Softwareentwicklung" (PSE) lernen die Teilnehmer, ein vollständiges Softwareprojekt nach dem Stand der Softwaretechnik in einem Team mit etwa 5 bis 6 Teilnehmern durchzuführen. Ziel ist es insbesondere, Verfahren des Software-Entwurfs und der Qualitätssicherung praktisch einzusetzen, Implementierungskompetenz umzusetzen, und arbeitsteilig im Team zu kooperieren.

Allgemeine Informationen zum Bachelor-Modul inklusive formaler Voraussetzungen und Prüfungsmodalitäten sind auf den Seiten des Lehrstuhls für Programmierparadigmen am IPD zu finden.

Projektbeschreibung

Debugger für Beweisskripte

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.

Skizze einer möglichen Implementierung

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.

Gruppentermine


Termin Zeit Inhalt Ort
15.05.2016 13:00 Uhr Erstes Gruppentreffen
Kick-Off Folien
Geb. 50.34, Raum 211

Weiterführende Informationen

Dokumente

Weiteres Material