Die formale Verifikation von Programmen ist ein zentraler Aspekt der Softwareentwicklung, besonders in sicherheitskritischen Bereichen wie der Medizintechnik, Luftfahrt und Finanzsoftware. Die klassische Methode der Verifikation basiert auf Hoare-Logik, einem formalen System, das es ermöglicht, Programme auf Korrektheit gegenüber bestimmten Vor- und Nachbedingungen zu prüfen. In Kombination mit modernen SMT-Solvern (Satisfiability Modulo Theories) ergibt sich ein mächtiges Werkzeug zur automatischen Überprüfung komplexer Programme. Über das Projekt "Tiny Hoare-Logik-Verifizierer mit SMT" wurde ein minimalistisches, dennoch leistungsfähiges System entwickelt, welches die theoretischen Grundlagen der Hoare-Logik mit den praktischen Vorteilen heutiger SMT-Technologie verbindet. Hoare-Logik bietet eine strukturierte Herangehensweise, um die Korrektheit eines Programms formal zu beweisen.
Hierbei werden sogenannte Hoare-Tripel verwendet, die in der Form {P} S {Q} notiert werden. P steht für die Vorbedingung, also was vor Ausführung des Programms gilt, S ist das Programm oder Programmstück und Q die Nachbedingung, die nach erfolgreicher Ausführung zutreffen soll. Das System definiert Regeln, um zu prüfen, ob ein solches Tripel gültig ist, was im Umkehrschluss beweist, dass das Programm S bei erfüllter Vorbedingung garantiert die Nachbedingung erreicht. Die Herausforderung bei der Verifikation besteht darin, aus komplexen Programmen überprüfbare Bedingungen abzuleiten. Hier kommt der "Tiny Hoare-Logik-Verifizierer" ins Spiel, der auf einer einfachen imperativen Programmiersprache namens IMP basiert.
Diese Sprache umfasst grundlegende Operationen wie Variablenzuweisungen, bedingte Anweisungen, Schleifen mit Invarianten sowie arithmetische und boolesche Ausdrücke. Der Verifizierer arbeitet durch die Berechnung der schwächsten Vorbedingung (weakest precondition, kurz WP). Diese bezeichnet die minimalste Bedingung, die vor Ausführung der Anweisung gelten muss, um eine gegebene Nachbedingung sicherzustellen. Interessanterweise erzeugt das Tool während der Verarbeitung des Programms automatisch Verifikationsbedingungen (verification conditions, VCs), die in einem einzigen Durchlauf generiert werden. Dies führt zu einer besonders effizienten Verifikation.
Die Kernfunktion arbeitet rekursiv auf der Programmstruktur und unterscheidet verschiedene Konstrukte: Bei "Skip" bleibt die Nachbedingung unverändert, bei der Zuweisung einer Variable substituiert sie die Nachbedingung entsprechend. Sequenzen werden durch sukzessive Berechnung behandelt, bedingte Anweisungen evaluieren den Zusammenhang zwischen dem Wahrheitswert der Bedingung und den jeweiligen Zweigen. Schleifen sind der einzige Fall, die neue Verifikationsbedingungen erzeugen, um die Korrektheit der Schleifeninvarianten sicherzustellen. Diese Invarianten sind essenziell, um zu garantieren, dass der Schleifenrumpf die Nachbedingung erfüllt, wenn die Schleife endet. Der so generierte Verifikationsprozess baut auf der Erkenntnis auf, dass ein Hoare-Tripel gültig ist, wenn die Vorbedingung die schwächste Vorbedingung impliziert.
Das führt dazu, dass alle erzeugten VCs als logische Formeln formuliert werden, welche mit einem SMT-Solver wie Z3 geprüft werden können. SMT-Solver erweitern klassische SAT-Solver um die Möglichkeit, innerhalb spezieller Theorien wie Arithmetik auf Ganzzahlen oder Booleschen Formeln zu arbeiten. Dies macht sie besonders leistungsfähig bei der Arbeit mit Programmverifikation. Als praktisches Beispiel veranschaulicht das Projekt die Verifikation eines kleinen Programms, das den größeren von zwei Zahlen findet. Die Vorbedingung ist trivial wahr, während die Nachbedingung aussagt, dass die Variable m entweder eins der Eingabewerte ist und gleichzeitig größer oder gleich beiden ist.
Durch WP-Berechnung und Einsetzen der Ausdrücke wird eine komplexe logische Formel generiert, die von Z3 automatisiert geprüft wird. Gelingt dieser Test, ist das Programm hinsichtlich der Spezifikation korrekt. Das Projekt ist in Scala geschrieben und steckt voller Potenziale für Erweiterungen. Beispielsweise zeigt es auch die Möglichkeit der Synthese, bei der SMT-Solver zur automatischen Generierung von Programmteilen verwendet werden können. Das Open-Source-Projekt bietet somit nicht nur ein Lehrbeispiel, sondern auch eine Plattform zur Erforschung und praktischen Anwendung der formalen Programmverifikation.
Die Integration mit SMT-Solvern bringt enorme Vorteile. Die automatische Beweisführung entlastet Entwickler und verhindert Fehler, die in manuellen Verifikationsprozessen leicht übersehen werden können. Zudem erlaubt die Formulierung in SMT-LIB-Standard, dass verschiedene SMT-Solver genutzt werden können, was Flexibilität und Zukunftsfähigkeit sichert. Neben der theoretischen Sauberkeit hebt das Projekt auch die Wichtigkeit von Schleifeninvarianten hervor. Ohne korrekte Invarianten lassen sich Schleifen nicht zuverlässig beweisen, was das Hauptproblem der mechanisierten Verifikation darstellt.
