Vorlesung Formale Logik und Verifikation im SS 2015

Diese Vorlesung ist eine Teilleistung des Moduls Grundlagen der Theoretischen Informatik. Die andere Teilleistung ist die Vorlesung Automaten und Formale Sprachen, die von Prof. Lang angeboten wird. Beide Teilleistungen werden durch eine Klausur geprüft, die für beide Teile am selben Tag abgelegt werden muss. Sie zählen gleichgewichtig. 

Hörerkreis:

2. Semester B_Inf, B_WInf mit bestandener Prüfung Diskrete Mathematik

Arbeitsaufwand: 2,5 ECTS-Punkte für diese Teilleistung

Vorlesungstermine: 
   normaler Termin: Di 17:00-18:15 Uhr, HS 3, im Wechsel mit der Übung
   1. Vorlesung am 21.04., 14 Uhr (geändert wegen Ausfall des Teils Automaten und Formale Sprachen)
   2. Vorlesung am 28.04., 14 Uhr (geändert wegen Ausfall des Teils Automaten und Formale Sprachen)
   3. Vorlesung am 12.05., 17 Uhr
   4. Vorlesung am 26.05., 17 Uhr
   5. Vorlesung am 16.06., 17 Uhr
   6. Vorlesung am 30.06., 17 Uhr
   7. Vorlesung am 07.07., 17 Uhr

Große Übung:   
   normaler Termin: Di 17:00-18:15, HS 3, im Wechsel mit der Vorlesung
   1. Übung am 28.04., 14 Uhr (erst Aufgabenbesprechung, dann neue Vorlesung)
   2. Übung am 05.05., 17 Uhr
   3. Übung am 19.05., 17 Uhr
   4. Übung am 09.06., 17 Uhr
   5. Übung am 23.06., 17 Uhr
   6. Übung am 07.07., 17 Uhr (erst Aufgabenbesprechung, dann neue Vorlesung)
   7. Übung am 14.07., 17 Uhr

Tutorien in Kleingruppen:   
   jeweils 2-wöchentlich
   weitere Details mit kurzfristigen Änderungen auf der zugehörigen Übungsseite

Jeder Teilnehmer sollte sich zur Abgabe der Übungen und individuellen Besprechung von Verständnisschwierigkeiten in genau einer Übungsgruppe einschreiben. Die Anmeldung erfolgt über das online-Sekretariat ab der 2. Vorlesungswoche.

Hinweis für höhere Semester, die nicht die Prüfungsordnung gewechselt haben (gilt dann auch für die Studiengänge TInf, MInf und ECom):

Diese Vorlesung ist identisch mit der früheren Anwendungsvorlesung zur Diskreten Mathematik. Studierende, die noch eine Prüfung in Diskrete Mathematik nach der alten Prüfungsordnung machen müssen, werden zusätzlich zum gegenwärtigen Stoff der Diskreten Mathematik (frühere Grundvorlesung) auch zu dieser Vorlesung geprüft, haben also eine größere Prüfung in Diskreten Mathematik als die Studierenden der neuesten Prüfungsordnung. Der Vorlesungsteil Automaten und Formale Sprachen ist dafür nicht relevant.

Studierende, die noch eine Prüfung zu Automaten und Formale Sprachen nach der alten Prüfungsordnung brauchen, müssen lediglich den Vorlesungsteil Automaten und Formale Sprachen dieses Semesters belegen und darin eine Klausur schreiben. Sie bekommen dafür die vollen 4 ECTS-Punkte angerechnet. Der Prüfungsteil Formale Logik und Verifikation ist für diese nicht relevant. Sie haben also lediglich die Teilklausur von Prof. Lang zu absolvieren.

 

 

Vorlesungsgliederung und Folien im Detail

Die Vorlesungen und Übungen finden in der Regel im Wechsel 14-tägig statt (genaue Termine siehe oben). Die angegebenen Tage hinter den Kapiteln sind als ungefähre Richtwerte zu verstehen und könnten sich noch geringfügig ändern. Ebenso werden unter Umständen noch kurzfristig Folien geändert (wird in rot hinter dem Kapitel vermerkt). Die in der jeweils nächsten Übung abzugebenden Übungsaufgaben beziehen sich aber immer nur auf den Stoff des Vorlesungstags davor.

Einführung (21.04.)

    1. Aussagenlogik (21.04., 28.04.)

    2. Prädikatenlogik (28.04., 12.05.)

    3. Verifikation mit Hoare-Tripeln (12.05., 26.05.)

    4. Verifikation von Verzweigungen (26.05.)

    5. Verifikation von Schleifen (16.06., 30.06.)
        (Beispielaufgaben)

    6. Verifikation von rekursiven Prozeduren (30.06., 07.07.)
        (Übersicht über Prozeduren mit der in dieser Vorlesung verwendeten Notation)        
        (Übungsaufgaben)

Literatur

Roland Backhouse: Programmkonstruktion und Verifikation, Hanser 1989 (vergriffen, auf Handoutserver erhältlich nur für Angehörige der FH Wedel, 25 MB), ISBN 3-446-15056-0
Englische Neuauflage: Program Construction: Calculating Implementations from Specifications, Wiley 2003, ISBN 0470848820

Helmut Balzert: Lehrbuch Grundlagen der Informatik, Spektrum 2005 (2. Auflage), ISBN 3-8274-1410-5
in unserer Bibliothek: Spektrum 1999 (1. Auflage), ISBN 3-8274-0358-8

Heinz-Peter Gumm / Manfred Sommer: Einführung in die Informatik, Oldenbourg 2011 (9. Auflage), ISBN  978-3-486-59711-0
und viele ältere Auflagen

Gerhard Goos: Vorlesungen über Informatik, Band1: Grundlagen und funktionales Programmieren, Springer 2000 (3. Auflage), ISBN 3-540-67270-2

David Harel / Yishai Feldman: Algorithmik, Springer 2006, ISBN 3-540-24342-9

Michael Huth / Mark Ryan: Logic in Computer Science, Cambridge University Press 2004 (2. Auflage), ISBN 052154310X

Uwe Schöning: Logik für Informatiker, Spektrum 2000 (5. Auflage), ISBN 3-8274-1005-3