Die Aufgabenblätter für die Zentralübung werden regelmäßig in der Vorlesung verteilt. Sie enthalten Hausaufgaben H und Programmieraufgaben P, die nicht abgegeben werden müssen.  Es ist unverzichtbar, sich mit den Aufgaben auseinanderzusetzen, um sich den Vorlesungsstoff zu erarbeiten; dazu empfiehlt sich auch ein Blick in die Literatur. Für Fragen stehen die Übungsleiter nach der Zentralübung zur Verfügung. Ferner sind Aufgaben Ü enthalten, die in der Zentralübung behandelt werden. Bei Bedarf werden in der Vorlesung auch Arbeits- und Merkblätter ausgeteilt. In den beiden ersten Zentralübungen wird eine Einführung in die funktionale Programmiersprache ML gegeben.

Inhalt: Ziel der Vorlesung ist es, Methoden der Spezifikation, Modularisierung, Abstraktion, Verfeinerung und Verifikation sowohl in der funktionalen als auch der imperativen Programmierung zu vermitteln. Dabei spielen sowohl die formale Anforderungsdefinition (Spezifikation) als auch der Korrektheitsbeweis (Verifikation) von Implementierungen bezüglich ihrer Spezifikation eine zentrale Rolle.

1. Grundlegende Begriffe
1. Der Kern des Programmierproblems
2. Strukturierung und Abstraktion in der Systementwicklung
3. Modellierung in der Systementwicklung
4. Der Einfluß der Notation und Formalität
5. Deskriptive und operationelle Beschreibung
6. Nutzungs- und Realisierungssicht
2. Rechenstrukturen
1. Zur Bedeutung von Rechenstrukturen
2. Beschreibung von Daten- und Rechenstrukturen
3. Daten als Rechenstrukturen
1. Datenmodellierung im Software Engineering
1. Algebraische Spezifikation
2. Spezielle Rechenstrukturen
4. Funktionale Programmierung
1. Konzepte
2. Fixpunkttheorie
3. Beweisprinzipien für Rekursion
4. Spezifikation funktionaler Programme
5. Unterspezifikation und Nichtdeterminismus
6. Techniken funktionaler Programmierung
5. Zustandsorientierte, sequentielle Programme
1. Zustände und Zustandsübergänge
2. Logik zuweisungsorientierter Programme
6. Referenzen und organisierte Speicher
1. Referenzen
2. Zyklische Referenzstrukturen
3. Referenzen und Programmvariable
4. Funktionen für organisierte Speicher
7. Objektorientierung
1. Objektorientierte Programmierung
2. Objektorientierter Entwurf
3. Objektorientierte Analyse
8. Grundlagen der Methodik
1. Schrittweise Verfeinerung
2. Abstraktionsebenen

Voraussetzungen: Informatik bis zum Vordiplom

Empfehlenswert als Grundlage für Programmierung und Software Engineering. Das Praktikum Spezifikation und Verifikation im kommenden Semester dient der werkzeuggestützten Anwendung der Techniken. Die Vorlesung wird im nächsten Semester fortgesetzt. In diesem zweiten Teil werden verteilte, interaktive Systeme behandelt.

Zur Programmierung: SML ist in der HP-Halle installiert. Sie können SML einfach mit 'sml' aufrufen. Mit dem Befehl 'use "datei.ml"' können Sie eigene Programme laden. Informationen zum Thema ML sind online verfügbar.