Suche

Formale Methoden


Die Entwicklung beweisbar korrekter Software ist eines der wichtigsten Ziele des Software-Engineering. Für einen Korrektheitsnachweis sind einerseits die Anforderungen, gemäß deren sich die Software verhalten soll, formal zu spezifizieren und andererseits das Verhalten der Software in einem adäquaten semantischen Modell zu erfassen. Die Vorlesung legt die mathematischen Grundlagen für die Spezifikation und die Semantik von sequentiellen Programmen, stellt Beweismethoden und ihre Umsetzung in einem Theorembeweiser vor und gibt eine Einführung in die methodische Entwicklung korrekter sequentieller Programme.

Schlagwörter: Aussagenlogik, Prädikatenlogik, Beweiskalküle, Induktion, algebraische Spezifikationen, operationale Semantik, Hoare-Logik, dynamische Logik, abstrakte Datentypen, Verfeinerung; Theorembeweiser (z. B. KIV)

Literatur:

  • Heinz-Dieter Ebbinghaus, Jörg Flum, Wolfgang Thomas. Einführung in die mathematische Logik. Spektrum Akademischer Verlag, 2007.
  • Hans-Dieter Ehrich, Martin Gogolla, Udo Walter Lipeck. Algebraische Spezifikation abstrakter Datentypen. B. G. Teubner, 1989.
  • Volker Sperschneider, Grigorios Antoniou. Logic - A Foundation for Computer Science. Addison-Wesley, 1991.
  • Joseph Maria Bocheński. Formale Logik. Karl Alber, 2002.

Folien