Software
Verifikationssprache SPARK wird freie Software
Die Firma AdaCore hat SPARK, eine Sprache zur formalen Verifikation der Korrektheit von Software, in einer GPL-Edition freigegeben.
AdaCore ist ein Unternehmen, das Tools rund um die Programmiersprache Ada entwickelt. So steht sie hinter der Entwicklungsumgebung GNAT, die einen auf GCC beruhenden Compiler, Bibliotheken, Entwicklungsumgebung und einiges mehr enthält. Ferner hat sie sie Sprache SPARK entwickelt, die es ermöglicht, Anmerkungen in die Kommentare eines Ada-Programmes aufzunehmen, die Vor- und Nachbedingungen einer Prozedur spezifizieren. Der Compiler versucht beim Compilieren schon den Nachweis zu erbringen, dass der Code das tut, was spezifiziert wurde, und falls das gelingt, wird die Korrektheit des Prozedur als bewiesen angesehen.
Ein weiteres Produkt des Unternehmens ist Tokeneer, ein Tutorial und Tools zur Verwendung von SPARK.
Während GNAT und Tokeneer schon länger als freie Varianten unter der GPL verfügbar waren, ist dies bei SPARK erst jetzt der Fall. Neben der freien wird für GNAT und SPARK eine kommerziell unterstützte Version angeboten, die im Gegensatz zur GPL-Version Support und Garantien enthält. Die GPL-Version von SPARK kann nach einer Anmeldung heruntergeladen werden.
Das formale Beweisen der Korrektheit von Software, wie SPARK es in gewissen Grenzen ermöglicht, ist ein Jahrzehnte altes Forschungsgebiet der Informatik. Es erzielte zwar stetige Fortschritte in den letzten Jahren, doch bleiben formale Korrektheitsbeweise weiterhin die Ausnahme, da sie eine entsprechende Ausbildung erfordern und immer noch schwierig zu führen sind. Am häufigsten werden sie dort durchgeführt, wo es besonders hohe Anforderungen an Sicherheit und Zuverlässigkeit gibt.
SPARK kann nach Ansicht des Software-Experten David A. Wheeler dazu beitragen, formale Beweise etwas zu erleichtern. Mit der freien Version von SPARK wird Tokeneer zu einem »Open Proof«. Ein Open Proof ist eine Kombination einer Implementation, automatisch verifizierbarer Beweise von mindestens einer wichtigen Eigenschaft der Implementation und der dafür benötigten Tools. Zusätzlich müssen all diese Komponenten freie Software sein, so dass im Prinzip jeder den Beweis nachvollziehen kann.
Laut Wheeler litt das Forschungsgebiet der automatischen Beweise stark darunter, dass viele Forschungsergebnisse geheim gehalten wurden und wieder verloren gingen. Anders als in vielen anderen Gebieten der Informatik war der Fortschritt trotz der hohen Investitionen in die Forschung eher gering. Wichtige Details fehlten in den Publikationen, wenn überhaupt etwas publiziert wurde. Daher wurde viel Zeit verschwendet, Ergebnisse mehrfach zu entdecken, und den Forschern fehlte es an Feedback und Beispielen, um die Ergebnisse zu verbessern. Nun, da SPARK für Open Proofs zur Verfügung steht, könnte die Gemeinschaft für eine größere Sammlung von Open Proofs und eine schnelle Verbesserung der Beweistechniken sorgen.
