Isabelle Praktikum Spezifikation und Verifikation

Prof. Tobias Nipkow
Gertrud Bauer
Markus Wenzel

Fragen Sie sich auch immer wieder, ob Ihr Programm wirklich funktioniert?
Wollten Sie schon immer verstehen, was Ihr Programm eigentlich macht?

Dann sind Sie hier richtig!

Zeit:
Mittwochs 16-18 Uhr
Ort:
1546 ("McKinsey-Raum")
Beginn:
10. Mai 2000
Anmeldung:
Bei der zentralen Praktikumsanmeldung am Semesteranfang.
Zuordnung:
Das Praktikum zählt sowohl zum Bereich Theoretische als auch Praktische Informatik.


Voraussetzungen

Wir suchen Studierende mit Grundkenntnissen in und Interesse an

So sollten Sie z.B. ein rekursives funktionales Programm schreiben können, das die natürlichen Zahlen 1, ..., n aufsummiert. Der Begriff der vollständigen Induktion sollte kein Fremdwort sein, und der Beweis, daß der von obigem Algorithmus berechnete Wert gleich n(n+1)/2 ist, keine fundamentalen Schwierigkeiten bereiten.


Motivation und Inhalt

Die Korrektheit von sicherheitskritischen Hard- und Softwaresystemen zu gewährleisten, ist immer noch ein ernstes Problem. Die zentralen Ziele dieses Praktikums sind das Erlernen

Konkret werden einige Anwendungsbeispiele behandelt, wobei wir aus Zeitgründen von vielen Details abstrahieren. Vorgesehen sind u.a.

An jedem dieser Beispiele werden spezifische Modellierungs- und Beweistechniken geübt. Die Spezifikation und Verifikation erfolgt in Isabelle/HOL.

In einer das Praktikum speziell begleitenden Vorlesungsreihe werden die Grundlagen zu Isabelle/HOL vermittelt:

HOL
ist - in erster Näherung - die Anreicherung einer polymorphen funktionalen Programmiersprache um logische Konzepte wie Quantoren und Mengen. HOL ist damit eine ideale Sprache zur Beschreibung funktionaler Programme.
Isabelle
ist ein generischer Theorembeweiser. Eine Ausprägung, Isabelle/HOL, unterstützt Spezifikation und Verifikation in HOL. Im Praktikum werden verschiedene Beweisverfahren (Termersetzung, Induktion, etc.) vorgestellt und ihre Funktion innerhalb des Beweisprozesses erläutert.


Durchführung

In der ersten Hälfte des Semesters findet eine Vorlesung statt, in der die nötigen Isabelle/HOL Kenntnisse vermittelt werden. Die Aufgaben sind jeweils innerhalb von 1-3 Wochen zu bearbeiten und bei der Praktikumsleitung zu präsentieren (Termin nach Vereinbarung). Ferner bieten wir zu den folgenden Zeiten im Raum 1533 eine Beratung durch studentische Mitarbeiter an:

Montag 12:30 Uhr - 14:00 Uhr Johannes Pfeifroth
Montag 16:00 Uhr - 18:00 Uhr Sebastian Nanz
Donnerstag 13:30 Uhr - 16:00 Uhr Johannes Pfeifroth
Donnerstag 16:00 Uhr - 18:00 Uhr Sebastian Nanz

Alle Praktikumsteilnehmer und Betreuer sind unter psv@mailbroy.in.tum.de erreichbar. Hier können auch allgemeine Fragen zu Isabelle gestellt und beantwortet (!) werden.

Als Arbeitsumgebung stehen am Lehrstuhl üblichen Sparc/Solaris und x86/Linux Plattformen zur Verfügung. Die Isabelle Distribution wird außerdem als Source und Binär-Pakete zum Download angeboten. Achtung: Verwenden Sie nur Isabelle_09-May-2000, oder eine neuere Version!


Aktuelle Hinweise

(5) Termine für die abschließende Präsentation

Stefan Baptist, Roger Rosette 19. Juli 15:30 Uhr - 15:55 Uhr Raum 1575
Sebastian Nanz 26. Juli 13:30 Uhr - 13:55 Uhr Raum 1546
Andreas Bauer, Jan-Thomas Czornack 26. Juli 14:00 Uhr - 14:25 Uhr Raum 1546
Matthias Kramm, Martin Okrslar, Christina Stan 26. Juli 14:30 Uhr - 14:55 Uhr Raum 1546
Carmen Barth, Mark Kiwitz 26. Juli 15:00 Uhr - 15:25 Uhr Raum 1546
Tobias Erlacher, Hanspeter Hagg 26. Juli 15:30 Uhr - 15:55 Uhr Raum 1546
Axel Ruder, Phillip Zerelles 26. Juli 16:00 Uhr - 16:25 Uhr Raum 1546

Im Anschluß daran (26. Juli, ca. 17 Uhr) sind alle Praktikumsteilnehmer herzlich ins Park Cafe eingeladen!

(4) Arithmetische Vereinfachung in Isabelle

Die automatische Vereinfachung arithmetischer Ausdrücke in Isabelle wurde kürzlich von Larry Paulson (Cambridge University) geändert. Diese Neuerungen sind in die im Praktikum verwendete Version Isabelle_09-May-2000 eingeflossen.

Wie wir jetzt festgestellt haben, kann das neue Verhalten leicht zu Komplikationen führen, insbesondere können verschiedene Zahl-Darstellungen plötzlich gemischt auftauchen: z.B. eine 'gewöhnliche' 1 = Suc 0 vs. eine #1 in Binärdarstellung.

Folgender ML-code deaktiviert die neuen Prozeduren in der aktuellen Theorie:

ML_setup {*
  Delsimprocs Nat_Numeral_Simprocs.cancel_numerals;
  Delsimprocs [Nat_Numeral_Simprocs.combine_numerals];
*};
Dadurch kann man sich einige Verwirrung ersparen.

(3) Isabelle und Proof General

Wer sich neben der eigentlichen Isabelle Distribution auch die Proof General Oberfläche installieren möchte, sollte eine neuere Vorversion von Proof General 3.2 verwenden. Ferner bietet sich das X-Symbol Paket zur Darstellung mathematischer Symbole auf dem Bildschirm an. Als zugrundeliegende Emacs Umgebung sollte in jedem Fall XEmacs-21 verwendet werden (wird bei den üblichen Linux-Distributionen bereits mitgeliefert).

Weitere Hinweise zur Installation der einzelnen Komponenten befinden sich am Anfang des Isabelle/Isar Reference Manual.

(2) Starten von Isabelle

Auf den sunbroy und sunhalle Rechnern läßt sich Isabelle (zusammen mit der Proof General Benutzeroberfläche) wie folgt starten:

        /usr/proj/isabelle/bin/Isabelle
      

Unter KDE kann man sich auch ein Application Desktop-Objekt zum Anklicken erzeugen:

        /usr/proj/isabelle/bin/isatool install -k
      

Für zügiges Arbeiten mit Isabelle sollte man eine relativ robuste Maschine verwenden, am Lehrstuhl etwa die sunbroy60, sunbroy61, sunbroy1, oder einen sunhalle Rechner.

(1) Rechnerbenutzung

Sie erhalten von der Praktikumsleitung eine Kennung auf den Unix Systemen des Lehrstuhls Broy. Die entsprechenden Rechnerräume sind 1533 und 1545.


Literatur

  1. Tobias Nipkow. Isabelle/HOL - The Tutorial, TU München, 2000.
  2. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle's Logics: HOL, TU München, 2000.
  3. Markus Wenzel. The Isabelle/Isar Reference Manual, TU München, 2000.
  4. Lawrence C. Paulson. ML for the working programmer, Cambridge University Press, 1991.
  5. Daniel J. Velleman. How to Prove it: A Structural Approach, Cambridge University Press, 1996.

Last modified: Thu Jul 27 16:46:29 MET DST 2000