Programmverifikation

1. Begriff der Informatik:
(1) formale Vorgehensweise mit dem Ziel, die Korrektheit eines Programms bzw. Moduls zu beweisen;
(2) Forschungsgebiet, das sich mit Methoden des Korrektheitsbeweises beschäftigt.

2. Motivation: Da mit dem gebräuchlichen Testen eines Programms die Korrektheit nicht garantiert werden kann, wurde nach Möglichkeiten gesucht, als Ersatz oder in Ergänzung die Korrektheit durch theoretische Analyse des Programmtexts zu beweisen.

3. Voraussetzungen:
(1) eine formale Spezifikation der Aufgabe des Programms bzw. Moduls;
(2) eine formale Beschreibung der Semantik einer Programmiersprache.

4. Vorteil: Korrektheit wird bewiesen, nicht nur unterstellt wie beim Testen.

5. Nachteil: Programmverifikation von Hand ist extrem aufwendig; lässt sich nur bei sehr kleinen Programmen anwenden, bei größeren Programmen nicht praktikabel. Intensive Forschungsbemühungen in der Informatik, die Programmverifikation so weit wie möglich zu automatisieren.