Schwergewichtige Blockkontrakte für KeY

Forschungsthema:KeY
Typ: BA / MA
Datum: 2017-07-13
Betreuer: Mattias Ulbrich
Michael Kirsten
Bearbeiter:
Aushang:

Ziel

Beweise über komplexe und größere Programme werden schnell sehr unübersichtlich und unhandlich, insbesondere wenn der erfolgreiche Beweis erst durch mehrere Iterationen zwischen Spezifikationsänderungen und Beweisführungen gefunden werden kann.

Um Beweise über komplexere und größere Methoden zu führen, ist es also hilfreich wenn der Beweis in verschiedene (unabhängig bearbeitbare) Teilbeweise aufgetrennt werden kann, die sich jeweils nur auf Teile der zu beweisenden Methode beziehen.

Innerhalb dieser Abschlussarbeit soll ein Weg gefunden und implementiert werden, solche Auftrennungen korrekt vorzunehmen. Hierzu sollen sogenannte Block-Verträge, eine bereits bestehende JML-Erweiterung, genutzt werden, mittels derer sich beliebige Programmteile innerhalb von Methoden spezifizieren lassen.

Voraussetzungen

  • Erfahrung im Programmieren mit Java
  • Kenntnisse, wie sie in der Vorlesung Formale Systeme vermittelt werden, sind hilfreich

Betreuung und Kontakt