Spezifikation und Verifikation objektorientierter Programme (2V + 2Ü) im SS 2005
Inhalt
In der Vorlesung werden zunächst die Grundlagen interaktiven Theorembeweisens mit Systemen wie HOL oder Isabelle/HOL präsentiert. Darauf aufbauend werden Kenntnisse zur formalen Spezifikation und Verifikation objektorientierter Programme vermittelt. Inhalte sind unter anderem:
- Logik höherer Ordnung
- Terme, Theoreme, Regeln, Taktiken als softwaretechnische Konstrukte
- Definition neuer Konstanten und Typen
- taktisches Theorembeweisen
- Kenntnisse zur Spezifikation mit Sprachen höherer Ordnung
- Formale Spezifikation objektorientierter Programme und ihre Semantik
- Hoare-Logik für objektorientierte Programme
- Formale Verifikation von OO-Programmen
