Umfang

Dieses Thema kann als Bachelorarbeit oder Teil einer Projektarbeit bearbeitet werden.

Empfohlene Vorkenntnisse

  • Grammatiken
  • Objektorientierte Programmierung
  • Optional: B, .NET

Problemstellung

Bei der Programmsynthese geht es darum für eine gegebene Spezifikation ein ausführbares Programm zu generieren. Die Spezifikation eines Programms kann hierbei beliebige Darstellungen haben, z.B. mathematische oder logische Formeln, textuelle Beschreibungen oder explizite Ein- und Ausgabebeispiele. Letztlich ist das Ziel, dass eine Spezifikation für ein Programmsynthesetool um einiges einfacher zu erstellen sein soll als das Programm selbst in der zugrundeliegenden Programmiersprache zu schreiben. Einsatzmöglichkeiten für Programmsynthese sind zum Beispiel automatische Programmreparatur, Codeoptimierung, Malwareerkennung, Textextraktion oder Textransformation (z.B. Microsoft Azure) oder die Möglichkeit Nicht-Programmierern das Programmieren kleinerer Funktionen anhand von einfachen Beispielen zu ermöglichen (z.B. Microsoft Excel’s Flash Fill / Autocomplete).

Wir haben eine constraintbasierte Methode der Programmsynthese für klassisches B implementiert und innerhalb eines (interaktiven) Prozesses mit dem ProB Model Checker verknüpft, um somit Invariantenverletzungen und Deadlocks in B Maschinen automatisch zu reparieren (https://link.springer.com/chapter/10.1007/978-3-319-98938-9_20, gerne schicken wir Ihnen das PDF auf Anfrage). Neben der Reparatur von Fehlern kann ebenso gänzlich neuer Code synthetisiert werden. Als Programmspezifikation werden explizite Ein- und Ausgabebeispiele verwendet. Eines der Probleme bei der Programmsynthese ist jedoch die Laufzeit. Für jeden Operator den wir in unserere Bibliothek and Programmkomponenten aufnehmen, wächst der Suchraum im schlimmsten Fall exponentiell.

In den letzten Jahren hat die Forschung im Bereich der Programmsynthese einige Fortschritte gemacht. So kann beispielsweise die Verwendung von Version Space Algebra die Performance von Programmsyntheseverfahren enorm erhöhen. Letztlich ist es aber sehr viel Aufwand ein Programmsyntheseverfahren für eine gewisse Sprache zu implementieren. Microsoft hat ein äußerst ausgereiftes SDK zur freien Verfügung veröffentlicht: https://microsoft.github.io/prose/

Im Rahmen dieser Arbeit soll eine Schnittstelle zwischen dem Microsoft PROSE SDK und ProB erstellt werden. Bezüglich dem Microsoft PROSE SDK gibt es einige Tutorials seitens der Entwickler von Microsoft.

Minimalanforderungen

  • Erarbeitung der theoretischen Hintergründe der grundlegenden im PROSE SDK implementierten Syntheseverfahren
  • Anbindung von dem PROSE SDK an ProB
  • Unterstützung einer Teilmenge von B
  • empirische Auswertung einzelner Fallbeispiele

Erweiterungen

Kontakt

Joshua Schmidt
Raum 25.12.02.52 · joshua.schmidt@hhu.de