Nipkow: Grundlagen der Programm- und Systementwicklung SS02
 TU München  Informatik  Software & Systems Engineering Lehre SS02


Sommersemester 2002
Grundlagen der Programm- und Systementwicklung


Prof. Tobias Nipkow, Ph.D.


 Übungen  Literatur  Links

Bereich: I, Vorlesung: 3 Std.
Zeit und Ort: Dienstag 10:30-12:00, Raum 1100
Freitag 12:15-13:00, Raum 1100
Beginn: Dienstag, 16. April 2002
Sprechstunde: Im Semester Mittwoch 12:00-13:00, im Büro 2550
Zentralübung: Mi 14:00-16:00, Raum N1080, 2-stündig
Beginn: Mittwoch, 24. April 2002
Übungsleitung: Gertrud Bauer



Aktuell:

Die Semestral-Prüfung findet am 19. Juli 2002 in Form einer mündlichen Prüfung statt.
13:30 Uhr Christian Trübswetter
13:55 Uhr Maria Bazus
14:20 Uhr Florian Haftmann
14:45 Uhr Adrian Rodriguez Monedero
15:10 Uhr Michal Ziemski
15:35 Uhr Sonia Camba
16:00 Uhr Nikolai Mamirov
16:25 Uhr Thomas Rieger



Beweis für die Korrektheit von itf (n,0,1) von Chaieb Amine.
concat(rev xss) = f(concat xss) ist widersprüchlich

Es ist sinnvoll, sich mit den Übungsaufgaben auseinanderzusetzen und die Übung zu besuchen, 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.

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. Einführung: Formale Methoden, Vorgehensmodelle.
  2. Funktionale Programmierung (in ML)
    1. Einführung
    2. Listen
      1. Spezifikation von Listenfunktionen mit Prädikatenlogik (map, take, prefix, sublist)
      2. Verifikation mit struktureller Induktion
      3. Wichtige Rechengesetze für Listenfunktionen (rev (map f xs) = map f (rev xs), etc) und ihre funktionale Formulierung (map f o rev = rev o map f).
      4. Die Funktionale foldl und foldr
    3. Eigenschaften von Spezifikationen: Eindeutigkeit, Unterspezifikation, Widersprüchlichkeit.
    4. Die Spezifikationssprache: Prädikatenlogik + ML + Mathematik
    5. Die Beweismittel: Prädikatenlogik für totale Funktionen, Induktion, Extensionalität.
    6. Rekursive Datentypen (datatype): Syntax, Axiomatik (Verschiedenheit und Injektivität der Konstruktoren, strukturelle Induktion) und Pattern Matching. Strukturelle Rekursion und strukturelle Induktion. Fundierte Rekursion und fundierte Induktion (wellfounded induction).
    7. Modularisierung
      1. Programmierung: Signaturen, Strukturen und Funktoren. Datenabstraktion mit Strukturen: Transparent and opaque signature matching. Datenabstraktion mit Funktoren. Beispiel: Funktor für Matrix-Arithmetik über Struktur mit Null, Addition und Multiplikation. Anwendung: Transitive Hülle von booleschen Matrizen. Systementwicklung mit Signaturen und Funktoren. Sharing constraints. Beispiel: Modularisierung einer Kühlungssteuerung.
      2. Axiomatische Spezifikation: Stacks, Sets, etc. Induktionsaxiome: Notwendig um bestimmte Funktionen als Erzeuger (Konstruktoren) auszuzeichnen. Konsistenz (notwendig für Implementierbarkeit) axiomatischer Spezifikationen und typische Beispiele von Inkonsistenz.
      3. Datentypimplementierung/Datenverfeinerung. Beispiel: Implementierung endlicher Mengen durch Listen ohne Duplikate. Der formale Beweis in Isabelle/HOL. Verallgemeinerung: Synthese, Abstraktion, Invariante, abstrakte Gleichheit, Beweis der Axiome.
  3. Verifikation imperativer Programme
    1. Die Technik von Floyd.
    2. Die Sprache IMP: Syntax, Hoare-Tripel, partielle und totale Korrektheit, Hoare-Logik, schwächste Vorbedingungen, Verifikationsbedingungen. Regel für totale Korrektheit. Hilfsvariablen. Behandlung ein- und mehrdimensionaler Felder durch explizite update-Funktion auf ganzem Feld. Problemfeld Prozeduren. Regel für rekursive Prozeduren ohne Parameter. Behandlung von Referenzen durch explizite Zustandsvariable vom Typ Adresse -> Wert.


Hörerkreis: Studenten der Informatik nach dem Vordiplom

Voraussetzungen: Informatik bis zum Vordiplom

Empfehlenswert als Grundlage für Programmierung und Software Engineering.

Literatur (wird während des Semesters erweitert)


  Gertrud Bauer, Last modified: Tue Jul 9 15:01:22 MEST 2002