Unerwartete Nebenwirkungen von Prozeduren und Funktionen,
Mehrfache Benutzung der gleichen Variablen,
Numerische Überraschungen (z. B. Rundungsfehler oder Auslöschung
führender Ziffern bei der Subtraktion benachbarter Zahlen).
Die überprüfung eines Programms auf Erfüllung seiner Spezifikation
kann also nach zwei verschiedenen Methoden erfolgen:
Formale Methode (Korrektheitsbeweis).
Mittels logischer Herleitungen wird die Einhaltung der Bedingungen
an die Zwischen- und Endergebnisse des Programms nachgewiesen.
Empirische Methode (Testen).
Mit bestimmten ausgesuchten Daten, für die das Ergebnis bekannt
ist, wird das Programm ausprobiert. Dabei kann nur das Vorhandensein von
Fehlern, nicht die Fehlerfreiheit nachgewiesen werden.
DIENSTE
