12.11.01: Informationen über die von HOL-CASL ausgeführten Beweisschritte erhält man, indem man unter [Options | Isabelle Options] die Isabelle-Konsole öffnet und "Trace simplification" aktiviert. Eine Beispiel-Sitzungsdatei für die in der Vorlesung vorgeführten Beweise ist hier abrufbar. Diese Datei sollte als HOL-CASL/git/sessions/casl_win/ListNat.1
abgespeichert werden. Falls in diesem Verzeichnis noch keine (versteckte) Datei .last
existiert, sollte diese angelegt werden, z.B. mit
echo ListNat > .last
Ein bedeutsames und derzeit noch unbefriedigend beherrschtes Problem im Entwicklungsprozess technischer Systeme ist die Zuverlässigkeit der produzierten Software. Diese ist gegeben, wenn ein Softwaresystem im Sinne der Aufgabenstellung funktioniert und auch auf Fehler angemessen reagiert. Besonders in sicherheitskritischen Anwendungsgebieten, wie etwa bei medizinischen Anwendungen, bei Zahlungssystemen, elektronischer Kommunikation, Zugangskontrollsystemen, aber auch Gasbrennersteuerungen im Haushalt, ist es entscheidend, dass die verwendeten Programmsysteme zuverlässig und sicher arbeiten. Die Vorlesung gibt eine Einführung in Methoden und Techniken zum Entwurf sicherer Systeme. Besonderes Gewicht wird dabei auf Techniken der Spezifikation und der Verfeinerung von Spezifikationen gelegt, die die Grundlage f�r moderne Validierungs- und Verifikationswerkzeuge bilden. Insbesondere werden folgende Themen behandelt:
Die Vorlesung wendet sich an Studierende im Haupt- und Nebenfach Informatik. Der Schein gilt für die Diplom-Hauptprüfung im Haupt- und Nebenfach Informatik. Der Schein gilt auch für die Hauptprüfung für das Lehramt an Gymnasien im Erweiterungsfach Informatik.
Prof. Dr. Martin Wirsing
Adresse: Raum 058, Oettingenstr. 67 Telephon: 2178 2154 Email-Adresse: wirsing@informatik.uni-muenchen.de
Dr. Stephan MerzDie Übungen werden betreut von
Adresse: Raum E0.9, Oettingenstr. 67 Telephon: 2178 2182 Email-Adresse: merz@informatik.uni-muenchen.de Sprechstunde: Mo, 10-11 Uhr und nach Vereinbarung
Dr. Piotr Kosiuczenko
Adresse: Raum E9, Oettingenstr. 67 Telephon: 2178 2133 Email-Adresse: kosiucze@informatik.uni-muenchen.de Sprechstunde: Do, 14-15 Uhr und nach Vereinbarung
Vorlesung: montags, 14-16 Uhr Raum 1.27 mittwochs, 10:40-12:10 Uhr Raum 1.27 Übungen: dienstags, 12-14 Uhr Raum 1.27Beginn der Vorlesung am 15.10.2001, Beginn der Übungen am 23.10.2001.
Warnung: Das Skript ist noch nicht korrigiert. Für Hinweise auf Fehler und Verbesserungsvorschläge wären wir dankbar.
CASL-Spezifikationen müssen für HOL-CASL im Verzeichnis HOL-CASL/examples/
liegen, Sitzungsdateien im Verzeichnis HOL-CASL/git/sessions/casl-win/
. Der Name von Spezifikation und .casl
-Datei muss übereinstimmen, der Name der Sitzungsdatei ist beliebig.
Warnung: Die offizielle Kommentarsyntax für CASL hat sich gegenüber der Syntax der Vorlesung geändert. CASL-Parser ab Version 0.7 liefern Fehlermeldungen. HOL-CASL basiert aber noch auf der in der Vorlesung verwendeten Syntax.
~/lib/xemacs/z-eves.el
abspeichern und folgende Zeilen in die Datei
.emacs
aufnehmen:
(setq auto-mode-alist (append auto-mode-alist '(("\\.z$" . z-latex-mode) ("\\.zed$" . z-latex-mode)))) (autoload 'z-latex-mode "~/lib/xemacs/z-eves" "Z-EVES LaTeX mode." t) (autoload 'run-z-eves "~/lib/xemacs/z-eves" "Run Z-EVES." t) (setq z-eves-program "z-eves")