Vorlesung Formale Logik und Verifikation im SS 2018

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

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

Vorlesungstermine: 
   Do 08:00 - 09:15, HS 1, im Wechsel mit der Übung
   1. Vorlesung am 12.04.
   2. Vorlesung am 19.04.
   3. Vorlesung am 03.05.
   4. Vorlesung am 24.05.
   5. Vorlesung am 14.06.
   6. Vorlesung am 28.06.
   7. Vorlesung am 05.07.

Große Übung:   
   wird noch bekannt gegeben, im Wechsel mit der Vorlesung
   1. Übung am 19.04. (erst Aufgabenbesprechung, dann neue Vorlesung)
   2. Übung am 26.04.
   3. Übung am 17.05.
   4. Übung am 07.06.
   5. Übung am 21.06.
   6. Übung am 05.07. (erst Aufgabenbesprechung, dann neue Vorlesung)
   7. Übung am 12.07.

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

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.

Die Vorlesung Grundlagen der Theoretischen Informatik findet in dieser Form in diesem Semester letztmalig statt. Studierende, welche sie erst ab 2019 belegen wollen, bekommen einen neuen Dozenten. Der Inhalt wird sich vermutlich auf Automaten und Formale Sprechen beschränken. Prof. Lang und ich stellen zum letzten Mal im WS 2018/2019 die Prüfung mit diesen Inhalten. Ab dem SS 2019 wird die Prüfung nur noch mit dem neuen Inhalt gestellt.

 

 

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 (12.04.)

    1. Aussagenlogik (12.04., 19.04.)

    2. Prädikatenlogik (19.04., 03.05.) (Prädikatenlogische Aufgaben)

    3. Verifikation mit Hoare-Tripeln (24.05., 14.06.)

    4. Verifikation von Verzweigungen (14.06.)

    5. Verifikation von Schleifen (14.06., 28.06.)
        (Beispielaufgaben)

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