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