Bug-freier Code ist kein Traum

Tony Hoare (das ist derjenige, der den Quicksort-Algorithmus erfunden hat) hat auf einer Informatikveranstaltung an der TU München sein Konzept zu Werkzeugen für die Erstellung von 100% fehlerfreiem Code vorgestellt. Sein Konzept bezieht sich auf einen Verifying Compiler, also ein Compiler der nicht nur die Syntax checkt, sondern auch auf Semantik und Fehlerfreiheit testet.

Die Idee ist folgende: Man wandle das Programm in eine mathematische Formel um und versuche diese zu beweisen. Wenn die Formel nicht beweisbar ist, ist der Code fehlerhaft. Damit das funktioniert muss das Programm Assertions beinhalten, um die entsprechende Formel zu bilden. Erfahren habe ich darüber in der Computer Zeitung Nr. 45 vom 5.11.2007. Noch mehr Informationen zu diesem speziellen Compiler gibt es hier.

Interessant ist, das die langweilige Beweisführung die wir in Logik und KI und Lineare Algebra ständig machen, einen (mir endlich) ersichtlichen, praktischen Nutzen hat.