Programmverifikation ist ein mühsames und aufwendiges Unterfangen. Wenn auf formal Grundlage durchgeführt, also mittels mathematischer Beweise und auf Grundlage einer (formalen) Semanik der verwendeten Programmsprache, ist der Umfang der Details, letzten Endes die Anzahl der möglichen verschiedenen Verhaltenweisen und die Gröẞe des Zustandsraums eine Hürde für die Verifikation bzw. die Prüfung der Korrektheit eine gegebenen Programms, die unüberwindlich ist.
Unüberwindlich insbesondere dann, wenn man eine manuelle Überprüfung, mit Papier und Bleistift, versucht, schlicht wegen der Größe der Problemstellung, bei nicht vollkommen trivialen Programmen.
Natürlich kann man versuchen, die Aufgabe ganz oder teilweise Rechnern bzw. darauf spezialisierten Programmen anzuvertrauen. Dabei ist die Verwendung von Beweisprüfern oder Beweisassistenten ein Weg. Diese sind im wesentlichen Implementierungen von einer Logik, und sie unterstützen die Verifikation indem sie Details des Beweisprozesses managen, der allerdings im wesentlichen von dem “Verifikationsingenieur” durchgeführt wird. Das unterscheidet sie von sogenannten automatischen Theorembeweisern. Das sind Werkzeuge, die selbst nach einem Beweis suchen, die allerdings schnell an ihre Grenzen stoßen und angesichts des Suchraums meist rasch kapitulieren müssen. Beweisassistenten, hingegen, unterstützen “nur” die Suche nach einem Beweis, in dem sie beispielsweise die noch offen Ziele und Unterziele managen, und natürlich, daß die den vom Menschen durchgeführten Beweis maschinell, in all seinen Details, überprüfen.
In dieser Arbeit verwenden wir Hoare-Logik, eine altbekannte und viel verwendete (Art von) Standardlogik für die Verifikations imperativer Programme, die auf Logik erster Stufe basiert. Wir verwendent den Beweisprüfer Lego, ein Beweisprüfer der auf einer inuitionistischen Logik höherer Ordnung basiert, genauer gesagt, dem Kalkül der Konstruktionen (calculus of constructions). Wir verwenden diesen Ramen umd dqie Formeln und Regeln der Hoare-Logik zo kodieren, und verwenden das Werkzeug dann um Beweise einfacher imperativer Programme computerunterstützt durchzuführen.