Grundlagen der Programm- und Systementwicklung
Wintersemester 1998/99
(Prof. Tobias Nipkow)

Bereich: I, Vorlesung: 3 Std.

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

Die Vorlesung am 16.2. fällt wegen Fasching aus.

Zentralübung: Mo 14.15-15.45 in Raum 1546
Die erste Übung findet am 9. November statt.
Übungsleitung: Wolfgang Naraschewski und Birgit Schieder.

Die Aufgabenblätter für die Zentralübung werden regelmäßig in der Vorlesung verteilt. Sie enthalten Hausaufgaben H, Programmieraufgaben P und Aufgaben Ü, die in der Zentralübung behandelt werden. Lösungsvorschläge und der Programmcode für die Lösungsvorschläge werden bereitgestellt. Bei Bedarf werden in der Vorlesung auch Arbeits- und Merkblätter ausgeteilt.

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.

Inhalt: Ziel der Vorlesung ist es, Methoden der Spezifikation, Modularisierung, Abstraktion und Verifikation sowohl in der funktionalen als auch der imperativen Programmierung zu erlernen. 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. ML vs. Haskell
    2. Polymorphismus
    3. Funktionen höherer Stufe: Funktionen als Argumente (Sortieren), Funktionen als Ergebnisse, eta-Äquivalenz.
    4. Listen
      1. Basisfunktionen (map, filter, concat, take, drop, zip etc)
      2. Spezifikation mit Prädikatenlogik (map, take, prefix, dsublist)
      3. Verifikation mit struktureller Induktion (map f (xs @ ys) = map f xs @ map f ys, (xs@ys)@zs = xs@(ys@zs), etc)
      4. Wichtige Vertauschungseigenschaften von Basisfunktionen (z.B. map f (rev xs) = rev(map f xs) und ihre funktionale Formulierung (z.B. map f o rev = rev o map f).
      5. Die Funktionale foldl und foldr
      6. Fallstudie: Spezifikation einer Sortierfunktion.
      7. Eigenschaften von Spezifikationen: Eindeutigkeit, Unterspezifikation, Widersprüchlichkeit.
      8. Die Spezifikationssprache: Prädikatenlogik + ML + Mathematik
      9. Die Beweismittel: Prädikatenlogik für totale Funktionen, Induktion, Extensionalität.
    5. 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).
    6. Modularisierung
      1. Programmierung: Strukturen und Signaturen. 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 auszuzeichnen. Eigenschaften axiomatischer Spezifikationen: Konsistenz (notwendig für Implementierbarkeit) und Konservativität (notwendig für getrennte Implementierbarkeit).
      3. Datentypimplementierung/Datenverfeinerung: Beispiel: Implementierung endlicher Mengen durch Listen ohne Duplikate. 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\"achste 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.
  4. Modellorientierte Spezifikation
    1. Das Prinzip modellorientierter Spezifikationen am Beispiel der Priority Queue.
    2. Die Spezifikationssprache Z: Einführendes Beispiel: Das Birthday Book von Spivey. Syntax von Formeln und Mengen in Z. Mengen und Typen. Definition und axiomatische Spezifikation in Z. Freie Datentypen. Operationen auf Mengen, binären Relationen und Funktionen. Spezifikation von E/R-Diagrammen in Z. Beschreibung zustandsbasierter Systeme mit Schemas. Beispiel: Theaterkasse, 8 Damen. Listen in Z. Beispiel: Polygone.
Hörerkreis: Studenten der Informatik nach dem Vordiplom

Voraussetzungen: Informatik bis zum Vordiplom

Empfehlenswert als Grundlage für Programmierung und Software Engineering. Das Praktikum Spezifikation und Verifikation dient der werkzeuggestützten Anwendung der Techniken.

Anzeige

Praktikum Spezifikation und Verifikation
Sommersemester 1999
Prof. Tobias Nipkow, Ph.D.
Wolfgang Naraschewski


Wir suchen Studierende

   mit Grundkenntnissen in

  • Logik,
  • einer typisierten funktionalen Programmiersprache (z.B. Gofer oder ML)

   und Interesse an

  • formaler Programmentwicklung,
  • logisch präzisen Beweisen

Unsere Praktikumsinhalte sind

   die Einführung in formale Techniken

  • zur Modellierung von funktionalen Systemverhalten,
  • zum maschinengestützten Nachweis der Korrektheit von Systemen

   die Behandlung praktischer
   Anwendungsbeispiele aus den Bereichen

  • Spezifikation des Unix-Filesystems
  • Effiziente Datenstrukturen
  • Arithmetik von Hardware
  • Operationelle Semantik von Java

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


Tobias Nipkow, 20.01.1999
Birgit Schieder, 21.01.1999