Praxis der Softwareentwicklung (PSE)
Thema: Innovative interaktive Oberfläche für SMT-Beweiser
Prof. Dr. Bernhard Beckert, Dr. Mattias Ulbrich, Alexander Weigl
Aktuelles
Die Lehrveranstaltung wird online stattfinden, weitere Informationen auf den Seiten des Lehrstuhls für Programmierparadigmen!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. Außerdem gibt es für PSE in diesem Semester einen (allgemeinen) ILIAS-Kurs.
Beschreibung:
In diesem PSE entwickeln Sie einen innovativen interaktiven Beweiser für prädikatenlogische Problemstellungen.
Ziel ist es, für Eingabedateien, für die Beweiser nicht vollautomatisch einen Beweis finden können, eine grafische Visualisierungsoberfläche zur Verfügung zu stellen, mit der der Grund des Nicht-schließens genauer untersucht werden kann und der Beweis ggf. durch geschickte Interaktion geschlossen werden kann.
Es gibt bereits eine Reihe mächtiger automatische Beweiser (sogenannte SMT-Solver), so dass Sie sich bei diesem PSE-Projekt auf die Darstellungs- und Interaktionskonzepte und deren Implementierung konzentrieren können.
Sinnvolle innovative Beweisinteraktionen umfassen z.B.
- interaktive Fallunterscheidungen
- Anwendung von Induktionen
- Quantoren-Instanziierung
- “Was-wäre”-Analysen
- Interaktive Vereinfachungen durch Benutzereingabe
- Auswahl von zu beachtetenden Klauseln.
- Trigger
- Propagieren von Gleichheiten
- Umbenennen von Bezeichnern.
- Schnellsuche von Bezeichern.
SMT-Solver (Satisfiability Modulo Theories) untersuchen logische Formelmengen auf Erfüllbarkeit. Formeln liegen dabei in Prädikatenlogik vor, die aber um “fest eingebaute” Datentypen und Symbole ergänzt wird (insbesondere für ganze Zahlen). Das wichtigste Standardformat für solche Beweiser ist SMTLIB, ein LISP-Derivat.
Die Aufgabe dieses PSEs umfasst:
- das Parsen von SMT-Eingabedateien,
- eine gut verständliche Darstellung von SMT-Problemstellungen
- die Implementierung von interaktiv anwendbaren logischen Schlussregeln.
- die Ansteuerung von externen SMT-Solver.
Aufgabenbeschreibungen
... zu den Phasen werden in den Veranstaltungen verteilt.
Hinweise und Erwartungen
- Aktives Source Code Management mittels eines Versionsverwaltungssystems
- Automatische Softwaretests
- Kontinuierliche Integration
- Anwendung bzw. Einhaltung von Design Patterns, Best Practices, und Style-Konventionen
- Kommentierter Quellcode, sowie Dokumentation und Testprotokolle