lisb: mehr Front- und Backends
Umfang
Dieses Thema kann als Bachelorarbeit oder Teil einer Projektarbeit oder auch im Rahmen einer Masterarbeit bearbeitet werden.
Empfohlene Vorkenntnisse
- gute Clojure Kenntnisse (z.B. durch Besuch der Veranstaltung “Funktionale Programmierung”)
- optional: Kenntnisse in Compilerbau
Problem
Mit Hilfe von lisb ist es möglich, die recht unflexible Sprachen B und Event-B aufzuweichen. Mittels einer DSL wird es ermöglicht Prädikate zu schreiben, die in die klare Semantik nach B übersetzt werden und dann von ProB gelöst werden.
Dazu ist lisb in drei Ebenen getrennt:
- ein Frontend, was derzeit sehr an B angelehnt ist,
- eine Zwischenrepräsentation (IR), die ebenso an B angelehnt ist,
- ein Backend, was ein B-AST erstellt und von ProB lösen lässt.
Minimalanforderungen
- Implementierungen von weiteren Frontends und Backends. Dies kann auch für Teilmengen der Sprachen geschehen (z.B. Alloy, SMT / Z3, SAT / Kodkod, …)
Variationen
- verschiedene Front- und Backends
- Evaluation der IR
Kontakt
Philipp KörnerRaum 25.12.02.56
p.koerner@hhu.de