Durch systematisches Testen eines Programms kann man versuchen, Fehler zu finden. Aber im Allgemeinen ist es nicht möglich, alle möglichen Fälle durchzuspielen, weil es zu viele sind, meist unendlich viele. Ein Programm, das den größten gemeinsamen Teiler von zwei natürlichen Zahlen a und b berechnen soll, müsste mit allen unendlich vielen Zahlenpaaren (a, b) getestet werden. "Testing can only show the presence of errors, not their absence" (E.W. Dijkstra).
Im Folgenden wird gezeigt, dass es im Prinzip möglich ist, die Korrektheit einer Implementierung, also eines Programmcodes, formal zu beweisen.