Formale Methoden des Systementwurfs![](Lambda.gif)
Skript mit Index; 232 Seiten
- PDF
letzter Update: 24. September 2015
Inhalt (Die LV beschränkt
sich auf die roten Abschnitte)
- 1 Wozu formale Methoden?
- 2 Programmiersprachen und -konzepte
- 2.1 Der Zustandsbegriff
- 2.2 Die klassische CPO-Theorie
- 3 Konkrete und abstrakte
Syntax
- 4 Mehrsortige
Prädikatenlogik
- 4.1 Syntax und Semantik
- 4.2 Logische Programme,
Kalküle und Herbrandmodelle
- 5 Funktional-logische Spezifikation und Termersetzung
- 5.1 Konstruktorbasierte
Spezifikationen
- 5.2 Terminations- und Konfluenzkriterien
- 6 Strukturierungskonzepte
- 6.1 Relative Konsistenz (außer 6.1.5-6.1.8)
- 6.2 Coprädikate
- 6.3 Parametrisierung
- 6.4 Refinement
- 6.5 Ausnahmen und Nichtdeterminismus
- 6.6 Partiell-rekursive Funktionen
- 6.7 Strukturierte Sorten und
λ-Terme
- 6.8 Monaden
- 7 Programmverifikation
- 7.1 Natürliches Beweisen
- 7.2 Induktion
- 7.3 Coinduktion
- 7.4 Invarianzbeweise
- 7.5 Schleifeninvarianten
- 8 Deduktive Programmsynthese
- 8.1 Funktionskomposition
- 8.2 Tuplung
- 8.3 Entrekursivierung
- 8.4 Parallelisierung
durch λ-Abstraktion
- 8.5 Differenzenbildung
- 8.6 Tabellierung
- 9 Zustandsorientierte Modellierung
- 9.1 Modallogik und ihre
Derivate
- 9.2 Spezifikationen mit
versteckten Sorten (bis 9.2.1)
- 10 CPO-Theorie
- 10.1 CPO-Semantik
- 10.2 Zusicherungslogik
- 10.3 Reduktionssemantik rekursiver Programme
- 11 λ-Terme, Typen und Bereiche
- 11.1 Typen und λ-Kalkül
- 11.2 Rekursive Bereiche
- 11.3 Funktionale Bereiche
- 11.4 Polymorphe Bereiche
- 11.5 Coalgebren
- Literatur
- Index
Teilweise in der Vorlesung behandelte Haskell-Programme:
Beispiele mit Expander2
Übungen
im WS 05/06
Übungen
im WS 04/05
Übungen
im WS 03/04
Übungsblätter vom WS 01/02:
Übungsblätter vom WS 00/01:
Übungsblätter
vom WS 98/99
Übungsblätter vom WS 96/97:
Buchempfehlungen (Formale Methoden, Diskrete Mathematik
und Theoretische Informatik):
- Ehrig,
Mahr, Cornelius, Große-Rhode, Zeitz, Mathematisch-strukturelle
Grundlagen der Informatik, Springer-Verlag 1999
- Goos,
Vorlesungen über Informatik, Band 1: Grundlagen und funktionales
Programmieren, Springer 2000
- J.-F.
Monin, Understanding Formal Methods, Springer 2003
- Grassmann,
Tremblay, Logic and Discrete Mathematics: A Computer Science Perspective,
Prentice Hall 1996
- Hopcroft,
Motwani, Ullman, Introduction to Automata Theory, Languages, and
Computation, Addison Wesley 2001
- Huth, Ryan, Logic in
Computer Science: Modelling and Reasoning about Systems, Cambridge
University Press 2000
- Pareigis,
Lineare Algebra für Informatiker, Springer 2000
- Steger,
Diskrete Strukturen 1, Springer 2001
- Schickinger,
Steger, Diskrete Strukturen 2, Springer 2001
- Schöning,
Algorithmik, Spektrum Akademischer Verlag 2001
- Schöning,
Logik für Informatiker, Spektrum Akademischer Verlag 2000
- Schöning,
Theoretische Informatik - kurz gefasst, Spektrum Akademischer
Verlag 2001