Vorlesung Formale Logik und Verifikation im SS 2016

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. Wer die Diskrete Mathematik vor dem SS 2016 noch nicht bestanden hat, kann die Prüfung für Grundlagen der Theoretischen Informatik im SS 2016 nicht mitschreiben.

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

Vorlesungstermine: 
   Mi 14:00-14:15 Uhr, HS 4, im Wechsel mit der Übung
   1. Vorlesung am 20.04.
   2. Vorlesung am 27.04.
   3. Vorlesung am 11.05.
   4. Vorlesung am 25.05.
   5. Vorlesung am 15.06.
   6. Vorlesung am 29.06.
   7. Vorlesung am 06.07.

Große Übung:   
   Di 14:00-15:15, HS 4, im Wechsel mit der Vorlesung
   1. Übung am 27.04. (erst Aufgabenbesprechung, dann neue Vorlesung)
   2. Übung am 04.05.
   3. Übung am 18.05.
   4. Übung am 01.06.
   5. Übung am 22.06.
   6. Übung am 06.07. (erst Aufgabenbesprechung, dann neue Vorlesung)
   7. Übung am 13.07.

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 noch in einer älteren Prüfungsordnung als 14.0 studieren (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 (20.04.) (geändert am 20.04.: Organisationsformen des SS 2015 entfernt)

    1. Aussagenlogik (20.04., 27.04.)

    2. Prädikatenlogik (27.04., 11.05.)

    3. Verifikation mit Hoare-Tripeln (11.05., 25.05.)

    4. Verifikation von Verzweigungen (25.05.)

    5. Verifikation von Schleifen (15.06., 29.06.)
        (Beispielaufgaben) (Übungsaufgabe vom 29.06.)

    6. Verifikation von rekursiven Prozeduren (29.06., 06.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