English website

Hörerkreis:

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

Termin der Vorlesung und großen Übung (im Wechsel): Mi 14:00 Uhr - 15:15 Uhr, HS1

Es wird 6 Vorlesungen und 6 große Übungen im Wechsel geben: Die Übungen zu dieser Vorlesung werden mir betreut. Ich gebe 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 steht für die Aufarbeitung des Lernstoffs in Kleingruppen ein Tutor zur Verfügung. Er bietet zwei Tutorien an, die im 2-Wochen-Rhythmus jeweils nach der großen Übung stattfinden. Die Tutorien starten nach der ersten großen Übung ab 15.04. Der Tutor korrigiert 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 (14.04.) 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.

Diese Vorlesung legt das theoretische Fundament zur Vorlesung Programmieren 1 und darauf aufbauender Programmierveranstaltungen und wendet sich an die Anfänger aller Informatikstudiengänge. Es gibt in den Inhalten Überschneidungen nicht nur zu Programmieren 1, sondern auch zur Vorlesung Diskrete Mathematik, die aus Gründen der inhaltlichen Geschlossenheit gewünscht sind.

Diese Vorlesung behandelt nicht alle Themen der Theoretischen Informatik, sondern beschränkt sich auf die beiden Themen Formale Logik und Verifikation von Programmen.

Das in der theoretischen Informatik ebenfalls wichtige Teilgebiet der Algorithmik und Komplexitätstheorie wird im Rahmen der Vorlesung Automaten und Formale Sprachen behandelt, welche als Fortsetzung dieser Vorlesung angesehen werden kann. Praktische Anwendungen von Algorithmik werden auch in der Vorlesung Programmiersprachen sowie systematischer in der Vorlesung Algorithmen und Datenstrukturen in C behandelt.

Da die Vorlesung Automaten und Formale Sprachen bereits Kenntnisse der Diskreten Mathematik voraussetzt, empfehlen Herr Lang und ich, diese entgegen dem offiziellen Studienplan nicht schon gleichzeitig mit dieser Vorlesung, sondern erst im 3. Semester zu besuchen, was von Stundenplan her ermöglicht wird

Der im Folgenden präsentierte Foliensatz fasst den Inhalt der Vorlesung 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.

Die reinen Vorlesungen finden statt am 14.04., 28.04., 12.05., 26.05., 16.06. und 30.06. 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 (14.04.)

1. Logik

    1.1 Aussagenlogik (14.04.: bis Algorithmus zu KNF, Rest am 21.04. nach der Aufgabenbesprechung der 1. Übung)

    1.2 Prädikatenlogik (28.04.)

2. Verifikationstechniken

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

    2.2 Verifikation von Verzweigungen (26.05.)

    2.3 Verifikation von Schleifen (26.05., 16.06.) (Beispielaufgaben)

    2.4 Verifikation von rekursiven Prozeduren (30.06.) (Übersicht über Prozeduren mit der in GTI verwendeten Notation)

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