Evaluation der Proof-Script-Sprache für KeY
Forschungsthema: | KeY, Usability |
---|---|
Typ: | BA |
Datum: | 2017-06-01 |
Betreuer: |
Sarah Grebing Mattias Ulbrich |
Aushang: |
Beschreibung
Die Interaktion zwischen Benutzer und System ist in Expertensystemen im Bereich computer-gestütztes Beweisen
ein wichtiges Kriterium für eine effiziente Beweisführung.
Um geeignet mit dem System interagieren zu können, muss viel Wert auf die Benutzbarkeit gelegt werden.
Es gibt verschiedene Ansätze, wie der Benutzer das System beim Führen eines Beweis lenkt.
Dies kann durch Klicken mit der Maus auf einer graphischen Darstellung (Proof by pointing) geschehen oder durch
eine textuelle Formulierung des Beweises in sogenannten Beweisskripten (z. B. Isar, s.u.).
Beide Ansätze haben ihre Vorzüge und Nachteile.
Am Lehrstuhl wurde hierzu ein Ansatz entwickelt, der es erlaubt, Mausinteraktion mit
Beweisskripten zu kombinieren, so dass der Benutzer das beste aus beiden Interaktionstechniken nutzen kann und
zu jedem Zeitpunkt im Beweis zwischen ihnen hin- und herwechseln kann.
Dieses Konzept wurde für das interaktive Beweiser- und Verifikationssystem KeY,
das am Institut entwickelt wird, prototypisch umgesetzt, indem die existierende Mausinteraktion um eine
Skript-Komponente erweitert wurde.
Innerhalb dieser Arbeit soll nun dieser Ansatz anhand des entwickelten Prototyps sowohl auf praktische
Ausdrucksmächtigkeit, Stabilität bezüglich Wiederverwendbarkeit und dem Laden von Beweisen,
sowie der sprachlichen Prägnanz für eine effiziente Beweisführung evaluiert werden.
Eine Ausarbeitung in englischer Sprache wird bevorzugt, ist jedoch nicht zwingend notwendig.
Voraussetzungen
Interesse an Arbeit in forschungsnahem Umfeld. Grundkenntnisse in formalen Methoden, wie sie z. B. in der Vorlesung Formale Methoden vermittelt werden. Programmierkenntnisse in Java für die Implementierung.
Kontakt
Interesse? Weitergehende Fragen? Dann melden Sie sich unverbindlich bei uns:
- Sarah Grebing (Raum 202, Geb. 50.34)
- Dr. Mattias Ulbrich (Raum 229, Geb. 50.34)
Literatur
- Leslie Lamport (2012). How to write a 21st century proof. Journal of Fixed Point Theory and Applications 11(1):43–63.
- Yves Bertot, Gilles Kahn, and Laurent Théry (1994). Proof by pointing. TACS 1994, volume 789 of LNCS, pages 141–160. Springer.
- Markus Wenzel (1999). Isar – a generic interpretative approach to readable formal proof documents. TPHOLs 1999, volume 1690 of LNCS, pages 167–184. Springer.
- Robert Geisler, Marcus Klar, Felix Cornelius, InterACT: An interactive theorem prover for algebraic specifications, AMAST’ 96, LNCS 1101, pages 563-566, Springer