English website

Hörerkreis:

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

Termin der Vorlesung und großen Übung (im Wechsel): Do 11:00 Uhr - 12:15 Uhr, Audimax

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 stehen für die Aufarbeitung des Lernstoffs in Kleingruppen zwei Tutoren zur Verfügung. Sie bieten jeweils einmal pro Woche einen Übungstermin an, der freiwillig ist und bei Verständnisschwierigkeiten besucht werden kann. Die Tutorien starten in der 3. Woche ab 19.10. 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. Jeder Tutor hält 2 Übungsgruppen, die 2-wöchentlich im Wechsel stattfinden. 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 in der 2. Vorlesungswoche 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.

Bisher hatte die Lehrveranstaltung 7 Vorlesungen und 5 Übungen. Da die Übungsaufgaben in der Vergangenheit von zu wenigen Studierenden bearbeitet wurden, was sich in hohen Durchfallquoten bei der Klausur niederschlug, habe ich den Zuschnitt der Lehrveranstaltung etwas geändert: Der Stoff wird noch mehr auf die Lösung konkreter Aufgaben konzentriert, wodurch eine Vorlesung wegfallen kann und mehr Zeit für die Übung bleibt. Es wird statt 5 großen Übungsblättern 6 kleinere geben. Der Gesamtaufwand für die Übung wird dadurch nicht größer, aber regelmäßiger verteilt. Ich empfehle, die verbesserte Möglichkeit der regelmäßigen Nacharbeitung und Übung des Vorlesungsstoffs wahrzunehmen und in jeder Übungsstunde, die alle 2 Wochen stattfindet, auch wirklich Lösungen abzugeben.

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.

In diesem Semester konzentriert sich die Vorlesung 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 2. Semester 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.

Der im Folgenden präsentierte Foliensatz fasst den Inhalt der Vorlesung zusammen. Er hat nicht den Anspruch eines Skriptes. Wegen des neuen Zuschnitts der Vorlesung werde ich die Folien erst im Laufe des Semesters, aber immer rechtzeitig vor dem jeweiligen Vorlesungstag, an dem der Stoff durchgenommen wird, auf diese Webseite stellen.

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

Einführung (08.10.)

1. Logik

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

    1.2 Prädikatenlogik (22.10., beendet am 05.11.) (S. 13 verändert am 05.11, noch einmal hochgeladen am 06.11.)

2. Verifikationstechniken

    2.1 Verifikation mit Hoare-Tripeln (angefangen am 12.11., beendet am 19.11.) (Beispiele mit Lösungen für Übungsblatt 3)

    2.2 Verifikation von Verzweigungen (19.11.)

    2.3 Verifikation von Schleifen (10.12.) (Beispielaufgaben)

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

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