Formale Methoden des Systementwurfs

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

• Data
• Differentiation
• Interpreter
• Struct
• Unification (siehe Skript, Seite 14 und 32)
• Baumparser: parse str übersetzt den String str in ein Objekt vom Typ Term (siehe Unification)

• Logische Programme aus Skript, Beispiel 4.2.2
• Ableitung aller Lösungen von Aufgabe 5.4
• Roboter-Programm, Roboter-Goal
• Queens-Programm, Queens-Goal

• Übung 0 Übung 1 Übung 2 Übung 3 Übung 4 Übung 5 Übung 6 Übung 7 Übung 8 Übung 9 Übung 10 Übung 11 Übung 12 Übung 13 Übung 14

• Übung 1 Übung 2 Übung 3 Übung 4 Übung 5 Übung 6

• Übung 1 Übung 2 Übung 3 Übung 4 Übung 5 Übung 6 Übung 7 Übung 8 Übung 9 Übung 10 Übung 11

• 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