Vorlesung Diskrete Mathematik, Teile Logik und Verifikation (ehemals GTI)

English website

Hörerkreis:

1. Semester aller Bachelor-Informatikstudiengänge (Inf, TInf, MInf, WInf, ECom)

Arbeitsaufwand: 2 ECTS-Punkte (sind in den 7 ECTS-Punkten für Diskrete Mathematik enthalten)

Termine der Vorlesung und großen Übung (im Wechsel):
Vorlesung:
Do, 13.10., 27.10., 10.11., 24.11., 15.12., 05.01., jeweils 17:00 - 18:15 Uhr (HS 6)
Große Übung: Do, 20.10., 03.11., 17.11., 01.12., 22.12., 12.01., jeweils 17:00 - 18:15 Uhr (HS 6)

Die Übungen zu diesem Vorlesungsteil werden von mir betreut. Ich gebe in jeder Vorlesung ein Übungsblatt heraus und führe die Lösungen in der Regel eine Woche später in der großen Übung vor.

Zusätzlich stehen für die Aufarbeitung des Lernstoffs in Kleingruppen Tutoren zur Verfügung. Sie bieten jeweils Tutorien an, die im 2-Wochen-Rhythmus jeweils nach der großen Übung stattfinden. Die Tutorien starten nach der ersten großen Übung. Die Tutoren korrigieren auch die Übungsaufgaben. Jeder Übungsteilnehmer muss sich aus diesem Grund in genau einem Tutorium eintragen, auch wenn er nicht an den Übungsstunden teilnimmt. Die Teilnehmerzahl in den Gruppen sollte ungefähr gleichverteilt sein, damit sich eine echte Kleingruppenarbeit einstellen kann. Daher werden die Gruppen getrennt verwaltet (auch wenn sie zum selben Tutor gehören). Details werden am 1. Vorlesungstag bekanntgegeben.

Die Übungsaufgaben sollen selbständig bearbeitet und in der nächsten großen Übung abgegeben werden (mit Angabe der Übungsgruppe). Der Tutor streicht die Fehler an und bespricht die wichtigsten Schwierigkeiten im darauf folgenden Tutorium. Außerdem werden Fragen zum laufenden Vorlesungsstoff beantwortet.

Dieser Vorlesungsteil ersetzt für 6-semestrige Bachelorstudienordnungen die Vorlesung GTI und ist mit dieser inhaltlich identisch: Er wird in diesem Semester letztmalig in dieser Form angeboten. In zukünftigen Semestern wird dieser Teil in die Hauptvorlesung Diskrete Mathematik integriert. Daher sollten alle Studierende aus einem 6-semestrigen Bachelorstudiengang, die GTI noch nicht belegt haben, an diesem Vorlesungsteil unbedingt teilnehmen. Prüfungen können in GTI noch später abgelegt werden, aber dann müssen sich die Teilnehmer ohne eigene Vorlesung darauf vorbereiten.

 

 

 

 

Vorlesungsinhalte

Dieser Vorlesungsteil wendet die Inhalte der Diskreten Mathematik auf die Verifikation der Inhalte der Vorlesung Programmiersprachen 1 an. Als Vorbereitung wird der Umgang mit formaler Logik geübt.

Der im Folgenden präsentierte Foliensatz fasst den Inhalt dieses Vorlesungsteils zusammen. Er hat nicht den Anspruch eines Skriptes.

In den Vorlesungseinheiten werden nicht nur die Folien präsentiert, sondern auch an der Tafel weitere Erklärungen abgegeben und Beispiele erläutert.

 

Vorlesungsgliederung

Die reinen Vorlesungen finden statt am 13.10., 27.10., 10.11., 24.11., 15.12., 05.01. 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). In Ausnahmefällen wird in der Vorlesung noch nicht geschaffter Stoff in der Übungsstunde nachgeholt. Für das 1. Kapitel ist das von vornherein so vorgesehen. Die in der jeweils nächsten Übung abzugebenden Übungsaufgaben beziehen sich aber immer nur auf den Stoff des Vorlesungstags davor.

Einführung (13.10.)

Teil Logik

    1. Aussagenlogik (13.10., 27.10.)

    2. Prädikatenlogik (27.10., 10.11.) (am 22.11. wurde Folie 14 neu eingefügt)

Teil Verifikation

    1. Verifikation mit Hoare-Tripeln (10.11., 24.11.)

    2. Verifikation von Verzweigungen (24.11.)

    3. Verifikation von Schleifen (15.12.)
        (Beispielaufgaben)

    4. Verifikation von rekursiven Prozeduren (05.01.)
        (Übersicht über Prozeduren mit der in dieser Vorlesung verwendeten Notation)        
        (Übungsaufgaben)

Literatur für diesen Vorlesungsteil

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 2004 (6. Auflage), ISBN  3-486-27389-2

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