Grundlagen der Programm- und Systementwicklung 1997/98
(Prof. Tobias Nipkow)

Bereich: I, Vorlesung: 3 Std.

Zeit und Ort: Dienstag 11:15-12:45 in S 1128 und Dienstag 14:15-15:00 in S 1128.

Zentralübung: Di 15:15-16:45 in 0670
Übungsleitung: Wolfgang Naraschewski und Radu Grosu.

Inhalt:

  1. Einführung
    1. Programm- und Systementwicklung
    2. Formale Methoden
    3. Strukturierung und Modellierung
    4. Spezifikation und Verfeinerung
  2. Algebren
    1. Signaturen
    2. Algebren
    3. Terme, Auswertung von Termen
    4. Modellorientierte und axiomatische Spezifikation
  3. Axiomatische Spezifikation
    1. Syntax: sorts/ops/axioms, evtl. hierarchisch aufgebaut; Syntax der Prädikatenlogik; generated-by.
    2. Semantik: nur für genareted-by präzise definiert; Modellbegriff.
    3. Homomorphismen und Isomorphismen
    4. Gleichungen und Induktion: Strukturelle Induktion als Gegenstück von generated-by; Fundierte Induktion.
    5. Eine Basisbibliothek von Spezifikationen: Bool, Nat, Int, List, Stack, Queue, Tree, Pair, Set, Mulitset, Map.
    6. Axiomatische Beschreibung konkreter Datentypen
      1. Datentypen in Programmiersprachen: Reduktion von Aufzälungstypen, Records und Unions auf data in Gofer; Axiomatische Beschreibung von data.
      2. Das E/R-Modell: Beschreibung von Entitäten und Relationen mit Hilfe der Spezifikationen Set und Pair; Axiomatisierung von Integritätsbedingungen.
    7. Eigenschaften von Spezifikationen
      1. Konsistenz: Beweis durch Angabe eines Modells; Typische Ursachen von Inkonsistenz an Fallbeispielen.
      2. Konservativität: fehlende Konservativität verhindert getrennten Implementierbarkeit.
    8. Vorgehehensweise: Anforderungsspezifikationen sollten generisch, implizit, minimal und hierarchisch sein.
  4. Implementierung von Spezifikationen
    1. Datentypimplementierung: Beispiel Set durch List (ohne Duplikate); allgemeines Prinzip mit Invariante und Abstraktionsfunktion.
    2. Implementierung von Funktionen: implizit -> explizit -> effizient.
  5. Funktionale Programmierung
    1. Sprachkonzepte (Wiederholung und Ergänzung)
    2. Funktionen höherer Stufe
      1. Lambda-Notation
      2. Eta-Konversion
      3. Funktionen als Argumente
    3. Listen
      1. Die Basis-Bibliothek: null, head, tail, (++), reverse, length, concat, map, elem, take, drop, takeWhile, dropWhile, zipWith, zip, filter.
      2. Fold left/right
      3. Listenkomprehension
    4. Spezifikation und Verifikation
      1. Rekursion und Induktion: Primitive Rekursion = strukturelle Induktion, terminierende Rekursion = fundierte Induktion; geschachtelte Rekursion.
  6. Verifikation imperativer Programme
    1. While-Sprachen
      1. Floyds Ansatz.
      2. Eine einfache While-Sprache und ihre Hoare Logik.
      3. Partielle und totale Korrektheit.
      4. Berechnung von Verifikationsbedingungen und schwächsten Vorbedingungen für annotierte Programme.
      5. Hilfsvariablen und Notation für Werte einer Variablen vor und nach Ausführung.
      6. Korrektheit und Vollständigkeit (Skizze)
    2. Erweiterungen
      1. Arrays
      2. Prozeduren: Problematik von call-by-reference und Aliasing.
      3. Hoare-Logik für rekursive Prozeduren ohne Parameter.

Hörerkreis: Studenten der Informatik nach dem Vordiplom

Voraussetzungen: Informatik bis zum Vordiplom

Empfehlenswert für: Grundlage für Programmierung und Software Engineering

Literatur: (Zum Teil in Semesterapparat verfügbar; wird im Laufe der Vorlesung verfeinert)

Sprechstunde: Mittwoch 11-12 im Raum S 2233 (Dienstzimmer von Prof. Nipkow)


Wolfgang Naraschewski, 19-02-1998, Tobias Nipkow, 25-11-1997,