Formale Grundlagen der Informatik III
Wintersemester 2011/2012

Für die praktischen Übungen verwenden wir das Verifikationswerkzeug VeriFun 3.4.

Formale Grundlagen der Informatik III

Wintersemester 2011/2012

Prof. Dr. Christoph Walther

Visar Januzaj – Nathan Wasser

VeriFun

Dokumentation

Ziehen Sie zusätzlich zu den Vorlesungsfolien auch die Dokumentationsdateien von VeriFun zu Rate. Insbesondere folgende Dateien werden für Sie hilfreich sein:

Der L 1.0 Primer beschreibt die Programmiersprache L mit Beispielen. Lesen Sie hier nach, um die genaue Syntax für Datentypen, Prozeduren und Lemmata zu erfahren.

Das Tutorial präsentiert einen Einstieg in die Arbeit mit VeriFun 2.x.
Achtung: Die Syntax sowie manche Bedienschritte haben sich in der Version 3.4 geändert.

Der User Guide beschreibt die Bedienung von VeriFun 2.x. Lesen Sie hier nach, um beispielsweise zu erfahren, wie man mittels Use Lemma ein Lemma interaktiv anwendet.
Achtung: Manche Bedienschritte haben sich in der Version 3.4 geändert.

What's New in VeriFun dokumentiert die neuen Features der Version 3.4 sowie Änderungen in der Benutzung des Systems.

Falls Sie weitergehende Fragen haben, die sich nach Lektüre dieser Dokumente nicht geklärt haben, nutzen Sie bitte das Forum oder die Poolbetreuung.

Vorlesung

Foliensatz Version Einzelfolien 4 Folien pro Seite
Inhaltsverzeichnis V1 iv 10-10-11.pdf (wird in neuem Tab geöffnet) iv 10-10-11_2auf1.pdf (wird in neuem Tab geöffnet)
Kapitel 1 V1 k1 11-03-24.pdf (wird in neuem Tab geöffnet) k1 11-03-24_4auf1.pdf (wird in neuem Tab geöffnet)
Kapitel 2 V1 k2 10-10-10.pdf (wird in neuem Tab geöffnet) k2 10-10-10_4auf1.pdf (wird in neuem Tab geöffnet)
Kapitel 3 V1 k3 10-10-10.pdf (wird in neuem Tab geöffnet) k3 10-10-10_4auf1.pdf (wird in neuem Tab geöffnet)
Kapitel 4 V1 k4 11-03-24.pdf (wird in neuem Tab geöffnet) k4 11-03-24_4auf1.pdf (wird in neuem Tab geöffnet)
Kapitel 5 V1 k5 11-03-24.pdf (wird in neuem Tab geöffnet) k5 11-03-24_4auf1.pdf (wird in neuem Tab geöffnet)
Kapitel 6 V1 k6 09-10-11.pdf (wird in neuem Tab geöffnet) k6 09-10-11_4auf1.pdf (wird in neuem Tab geöffnet)
Kapitel 7 V1 k7 11-03-24.pdf (wird in neuem Tab geöffnet) k7 11-03-24_4auf1.pdf (wird in neuem Tab geöffnet)
Kapitel 8 V1 k8 11-03-24.pdf (wird in neuem Tab geöffnet) k8 11-03-24_4auf1.pdf (wird in neuem Tab geöffnet)
Kapitel 9 V1 k9 10-10-11.pdf (wird in neuem Tab geöffnet) k9 10-10-11_4auf1.pdf (wird in neuem Tab geöffnet)
Kapitel 10 V1 k10 09-10-22.pdf (wird in neuem Tab geöffnet) k10 09-10-22_4auf1.pdf (wird in neuem Tab geöffnet)
Kapitel 11 V1 k11 10-10-11.pdf (wird in neuem Tab geöffnet) k11 10-10-11_4auf1.pdf (wird in neuem Tab geöffnet)
Kapitel 12 V1 k12 10-02-02.pdf (wird in neuem Tab geöffnet) k12 10-02-02_4auf1.pdf (wird in neuem Tab geöffnet)

Präsenzübungen

Bitte bringen Sie zu jedem Übungstermin das jeweilige Übungsblatt (auf Papier oder einem Laptop) mit!

Das Datum in der Tabelle ist jeweils der Dienstag einer Übungswoche.

Hausübungen

Übung Ausgabedatum Abgabedatum Aufgaben Lösungsvorschlag
Hausübung 1 Di, 22.11.2011 Di, 06.12.2011 H1-2011-11-22.pdf (wird in neuem Tab geöffnet) H1-L-2012-01-17.pdf (wird in neuem Tab geöffnet)
Hausübung 2 Di, 06.12.2011 Di, 20.12.2011 H2-2011-12-06.pdf (wird in neuem Tab geöffnet) H2-L-2012-01-17.pdf (wird in neuem Tab geöffnet)
Hausübung 3 Di, 20.12.2011 Di, 10.01.2012 H3-2011-12-20.pdf (wird in neuem Tab geöffnet) H3-L-2012-02-10.pdf (wird in neuem Tab geöffnet)
Hausübung 4 (Teil 1) Di, 17.01.2012 Di, 24.01.2012 H4-2012-01-17.pdf (wird in neuem Tab geöffnet) H4.1-L-2012-02-10.pdf (wird in neuem Tab geöffnet)
Hausübung 4 (Teil 2) Fr, 27.01.2012 Mo, 06.02.2012 H4-2012-01-27.pdf (wird in neuem Tab geöffnet) H4.2-L-2012-02-10.pdf (wird in neuem Tab geöffnet)
Termine in Klammern sind vorläufig und spiegeln den jetzigen Planungsstand wider.

Praktische Übungen

Übung Ausgabedatum Aufgaben Lösungsvorschlag
Praktische Übung 1 28.10.2011 Praxis1.zip Loesung1.vf
Praktische Übung 2 18.11.2011 Praxis2.zip Loesung2.vf
Praktische Übung 3 09.12.2011 Praxis3.zip Loesung3.vf
Praktische Übung 4 16.01.2012 Praxis4.zip Loesung4.vf
Termine in Klammern sind vorläufig und spiegeln den jetzigen Planungsstand wider.