Formale Programmtests

Dieses Papier schlägt eine praktikable Alternative zur Programmverifikation vor – die als formales Programmtesting bezeichnet wird – mit ähnlichen, aber weniger ambitionierten Zielen. Wie ein Programmverifikator nimmt ein formales Testsystem ein Programm mit formalen Spezifikationen als Eingabe, generiert die entsprechenden Verifizierungsbedingungen und leitet sie durch einen Vereinfacher. Nach dem Vereinfachungsschritt bewertet ein formales Testsystem jedoch einfach die Verifizierungsbedingungen anhand eines repräsentativen Satzes von Testdaten, anstatt zu versuchen, sie zu beweisen. Formales Testen liefert starke Beweise dafür, dass ein Programm korrekt ist, garantiert dies jedoch nicht. Die Stärke der Beweise hängt von der Angemessenheit der Testdaten ab.