Projektarbeit: Portierung einer Java-Integer-Formalisierung von Isabelle2003 auf Isabelle2005

Aufgabenstellung

Bei dieser Projektarbeit handelt es sich um die Portierung einer Theorie von der Version 2003 des Theorembeweisers Isabelle auf die Version 2005. Bei der Theorie handelt es sich um eine Formalisierung der Java Integer. Diese stützt sich auf die in Isabelle vorhandenen unbeschränkten ganzen Zahlen ab, die in der bei Isabelle mitgelieferten Theorie Intg vorliegen. Die Theorie Intg wurde beim Wechsel von 2003 auf 2004 stark überarbeitet (z. B. Lemmata wurden zusammengefasst, ihre Namen wurden geändert, der Simplifier wurde leistungsfähiger gemacht etc.). Daher funktionieren viele der in der Java-Integer-Formalisierung vorliegenden Beweisskripte nicht mehr, da Lemma-Namen nicht mehr passen, Beweise evtl. früher fertig sind u. ä. Die Kernaufgabe der Projektarbeit ist es, diese Beweisskripte auf Isabelle 2004 anzupassen. Diese Kernaufgabe lässt sich in verschiedene Richtungen erweitern. Eine mögliche Erweiterung wäre ein Beweis-Reengineering, so dass die vorliegenden Beweise z. B. kürzer, schneller, besser lesbar und/oder besser wartbar werden. Eine andere Erweiterung wäre die Ausdehnung der Formalisierung auf bisher noch nicht betrachtete Aspekte der Java Integer, z. B. die Bitoperationen, die Shiftoperationen oder die Vergleichsoperationen. Diese Erweiterungen können je nach Interesse im Rahmen der Projektarbeit ausgewählt werden.

Voraussetzungen

Gute Kenntnisse in Logik sind empfehlenswert.
Kenntnisse im Theorembeweisen sind wünschenswert, aber nicht Voraussetzung. Eine entsprechende Einarbeitung in die Benutzung des Theorembeweisers Isabelle ist im Rahmen der Projektarbeit zu leisten.

Weitere Informationen / Ansprechpartner

%NICOLE_LINK%