KomuraSoft LLC
Kontakt
Menü

Einführung in die formale Verifikation mit SPARK ── Von Ada-Verträgen zum mathematischen Beweis

· · Ada, SPARK, Formale Verifikation, GNATprove, Design by Contract, Hohe Integrität, Programmiersprache, Hohe Zuverlässigkeit

1. Einleitung ── Jenseits von „Ausführen und Nachsehen”

Der gängigste Weg, die Qualität von Software sicherzustellen, sind Tests.

Test: prüft, ob das Programm für ausgewählte Eingaben korrekt arbeitet

Doch Tests haben inhärente Grenzen. Die Anzahl möglicher Eingaben ist unendlich, und Tests allein können die Korrektheit nicht für alle Eingaben nachweisen.

Hier kommt die formale Verifikation (Formal Verification) ins Spiel.

Formale Verifikation: beweist mathematisch, dass eine Eigenschaft für alle möglichen Eingaben gilt

Der vorherige Artikel „Die Faszination der Sprache Ada” gab einen Überblick über Ada und streifte SPARK bereits kurz.

Dieser Artikel konzentriert sich speziell auf die praktische formale Verifikation mit SPARK und behandelt Folgendes:

Was SPARK ist und wie es sich zu Ada verhält
Wie man Verträge (Pre/Post) schreibt
Wie man sie mit GNATprove beweist
Wie man Schleifeninvarianten entwirft
Wie man mit Datenfluss-Verträgen (Global/Depends) Nebenwirkungen verwaltet
Eine schrittweise Einführungsstrategie über Beweisstufen (Stone bis Platinum)
Wie man SPARK in reale Projekte integriert

Das Ziel ist, den Übergang von Test zu Beweis anhand funktionierender Codebeispiele erfahrbar zu machen.

Die Codeausschnitte dieses Artikels sind kapitelweise geordnet als Referenzsammlung auf GitHub verfügbar.

ada-spark-formal-verification - komurasoft-blog-samples (GitHub)

2. Was ist SPARK ── Adas Teilsprache als Zugang zur Welt des Beweises

SPARK ist eine Teilmenge der Programmiersprache Ada.

Dass es sich um eine Teilmenge handelt, ist eine bewusste Designentscheidung.

Vollständiges Ada → hoch ausdrucksstark, aber die vollständige Verifikation ist unpraktikabel
SPARK             → beschränkt auf verifizierbare Merkmale, macht Beweise realistisch

Die wichtigsten Einschränkungen von SPARK sind:

Dynamische Speicherverwaltung über Zeiger (Access-Typen) → über ein Ownership-Modell kontrolliert
Freie Verwendung von Ausnahmebehandlungen               → in eingeschränkter Form erlaubt
Rekursive Datenstrukturen                                → eingeschränkt, da schwer beweisbar
Freie Verwendung von Tasking                             → über das Ravenscar-Profil eingeschränkt

„Einschränkungen” mögen einengend klingen, doch sie sind der Preis für Beweisbarkeit.

Der Kern des SPARK-Werkzeugkastens ist GNATprove von AdaCore.

So arbeitet GNATprove:
1. Analysiert SPARK-annotierten Ada-Code
2. Übersetzt Verträge (Pre/Post) und Assertionen in die Zwischensprache Why3
3. Versucht Beweise mit automatischen Beweisern wie Z3, CVC4 und Alt-Ergo
4. Meldet Ergebnisse als Meldungen direkt am Quellcode

Entscheidend ist: SPARK ist auf Ada aufgebaut.

SPARK-Code = Ada-Code + Vertragsannotationen

Mit anderen Worten: SPARK ist eine natürliche Erweiterung der gewohnten Ada-Entwicklung. Es ist keine völlig neue Syntax zu erlernen.

3. GNATprove installieren und der erste Beweis

Zunächst richten wir eine Umgebung zum Ausführen von GNATprove ein.

Mit Alire lässt sich mit folgendem Befehl ein SPARK-fähiges Projekt anlegen:

alr init --bin spark_demo
cd spark_demo

Da GNATprove Teil des GNAT-Compilers ist, steht der Befehl gnatprove automatisch zur Verfügung, sobald sich das Projekt mit alr build bauen lässt.

Als erstes Beweisziel schreiben wir eine Funktion, die den Absolutwert zurückgibt.

package Simple_Proof with SPARK_Mode is

   function Abs_Value (X : Integer) return Integer
     with Post => Abs_Value'Result >= 0;

end Simple_Proof;

package body Simple_Proof with SPARK_Mode is

   function Abs_Value (X : Integer) return Integer is
   begin
      if X < 0 then
         return -X;
      else
         return X;
      end if;
   end Abs_Value;

end Simple_Proof;

Wichtige Punkte im Überblick:

with SPARK_Mode wird sowohl an die Paketspezifikation als auch an den Rumpf angehängt
Die Post-Bedingung deklariert die Eigenschaft „das Ergebnis ist nicht negativ"
Das Attribut 'Result verweist auf den Rückgabewert der Funktion

Nun führen wir GNATprove auf diesem Code aus:

gnatprove -P spark_demo.gpr

Die Ausgabe sieht so aus:

SUMMARY
-------
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
simple_proof.adb:5:15: info: range check proved
simple_proof.adb:6:16: info: range check proved
simple_proof.ads:3:19: info: postcondition proved

Die Meldung postcondition proved bedeutet: Für alle möglichen Integer-Eingaben wurde mathematisch bewiesen, dass der Rückgabewert nicht negativ ist.

Das ist der Einstiegserlebnis in SPARK.

4. Grundlagen des vertragsbasierten Designs ── Pre und Post schreiben

SPARK-Beweise beginnen mit dem Schreiben von Verträgen.

Verträge sind ein Sprachmerkmal von Ada 2012, doch in SPARK werden sie zur Eingabe für den Beweis.

procedure Transfer (From, To : in out Account; Amount : Positive)
  with Pre  => From.Balance >= Amount,
       Post => From.Balance = From.Balance'Old - Amount
                and then
                To.Balance = To.Balance'Old + Amount;

Leitlinien für den Entwurf von Pre- und Post-Bedingungen:

Pre (Vorbedingung):
  Verantwortung des Aufrufers
  „Wenn du mich mit dieser erfüllten Bedingung aufrufst, garantiere ich die Post-Bedingung"
  Schwach genug, um erfüllbar zu sein, stark genug, um nützlich zu sein

Post (Nachbedingung):
  Verantwortung der Implementierung
  „Nach dem Aufruf sieht die Welt so aus"
  Das Attribut 'Old verweist auf Werte vor dem Aufruf
  Zu stark macht die Implementierung zu eng; zu schwach beweist nichts Nützliches

Häufige Fehler und wie man sie vermeidet:

Fehler 1: Pre zu stark
  Pre => X > 0 and X < 100 and X /= 50 and ...
  → Prüfen: Kann der Aufrufer das immer erfüllen?
  → Pre nicht nur deshalb verengen, weil Tests bestehen

Fehler 2: Post zu schwach
  Post => True
  → Garantiert nichts. Der Beweis ist bedeutungslos.

Fehler 3: Nebenwirkungen in Post vergessen
  Post => Result = X * 2  (Aktualisierung einer globalen Variablen übersehen)
  → Nebenwirkungen mit Global/Depends-Verträgen explizit machen (Abschnitt 9)

5. Beweis der Overflow-Freiheit ── Numerische Sicherheit garantieren

Zu den praktisch wertvollsten Dingen, die SPARK beweist, gehört die Freiheit von Overflow.

Betrachten Sie diesen Code:

procedure Increment (X : in out Integer)
  with SPARK_Mode,
       Pre  => X < Integer'Last,
       Post => X = X'Old + 1;

Pre => X < Integer'Last ist der Schlüssel. Mit diesem Vertrag kann GNATprove beweisen, dass die Addition nicht überläuft.

Ohne Vertrag warnt GNATprove vor einem möglichen Overflow:

medium: overflow check might fail

Dasselbe gilt für komplexere Berechnungen:

function Average (A, B : Integer) return Integer
  with SPARK_Mode,
       Pre  => (if A >= 0 and B >= 0 then A <= Integer'Last - B
                elsif A < 0 and B < 0 then A >= Integer'First - B),
       Post => (if A <= B then A <= Average'Result and Average'Result <= B
                else B <= Average'Result and Average'Result <= A);

Die Pre-Bedingung wirkt komplex, drückt aber lediglich aus, dass „die Summe A+B nicht überläuft” – mit vorzeichenabhängiger Fallunterscheidung.

Kernaussage:
  Das Wesen des Overflow-Beweises besteht darin, in Pre zu deklarieren,
  dass das Ergebnis von Addition oder Multiplikation im Bereich des Typs bleibt
  Das wirkt mühsam, aber einmal geschrieben, plagt einen nie wieder ein Overflow-Fehler

6. Schleifeninvarianten ── Eigenschaften von Schleifen beweisen

Einer der schwierigsten Teile der formalen Verifikation ist der Beweis von Schleifeneigenschaften.

Schleifen laufen eine beliebige Anzahl von Malen, sodass Tests nicht alle Fälle abdecken können. SPARK verwendet dafür Schleifeninvarianten (Loop Invariants).

function Sum_Of_Naturals (N : Natural) return Natural
  with SPARK_Mode,
       Post => Sum_Of_Naturals'Result = (N * (N + 1)) / 2;

function Sum_Of_Naturals (N : Natural) return Natural is
   Result : Natural := 0;
begin
   for I in 1 .. N loop
      Result := Result + I;
      pragma Loop_Invariant (Result = (I * (I + 1)) / 2);
   end loop;
   return Result;
end Sum_Of_Naturals;

Der Entwurf von Schleifeninvarianten erfordert folgende Denkweise:

1. Eine Eigenschaft schreiben, die zu Beginn jeder Iteration gilt
2. Eine wählen, die nach der letzten Iteration die gewünschte Post-Bedingung impliziert
3. Die Invariante drückt die bisherige Teilberechnung als Formel aus

Hier ein weiteres Beispiel: die Suche in einem Array.

function Find (Arr : Array_Of_Integer; Target : Integer) return Natural
  with SPARK_Mode,
       Post => (if Find'Result = 0 then
                  (for all K in Arr'Range => Arr (K) /= Target)
                else
                  Arr (Find'Result) = Target);

function Find (Arr : Array_Of_Integer; Target : Integer) return Natural is
begin
   for I in Arr'Range loop
      if Arr (I) = Target then
         return I;
      end if;
      pragma Loop_Invariant
        (for all K in Arr'First .. I => Arr (K) /= Target);
   end loop;
   return 0;
end Find;

Die Invariante hier lautet: „Im bisher untersuchten Bereich existiert Target nicht.”

Prinzipien für den Entwurf von Schleifeninvarianten:
  Als Formel ausdrücken: „Was lässt sich nach n Iterationen sagen?"
  Bei Array-Schleifen lautet das Muster oft „für den bereits verarbeiteten Bereich gilt P"
  Eine zu starke Invariante lässt sich nicht beweisen; eine zu schwache impliziert die Post-Bedingung nicht
  Die richtige Balance zu finden, ist die eigentliche Kunst des Schleifenbeweises

7. Assertion-Pragmas ── Partielle Eigenschaften im Code

Zusätzlich zu Verträgen (Pre/Post) erlaubt SPARK, Assertionen (Assert) direkt im Codekörper zu schreiben.

procedure Divide (A, B : Integer; Q, R : out Integer)
  with SPARK_Mode,
       Pre  => B /= 0,
       Post => A = Q * B + R and R >= 0 and R < abs (B);

procedure Divide (A, B : Integer; Q, R : out Integer) is
begin
   Q := A / B;
   R := A rem B;

   pragma Assert (A = Q * B + R);
   pragma Assert (R >= 0);
   pragma Assert (R < abs (B));
end Divide;

Die Verwendung der verschiedenen Pragmas im Überblick:

Pre/Post:       Zusagen beim Eintritt in und Austritt aus dem Unterprogramm
Assert:         Eine Eigenschaft, die an einer bestimmten Stelle im Code gelten soll
Loop_Invariant: Eine Eigenschaft, die über jede Schleifeniteration hinweg erhalten bleibt
Loop_Variant:   Eine abnehmende Größe, um die Terminierung der Schleife zu beweisen

Gute Einsatzorte für Assert:

Überprüfung von Zwischenergebnissen komplexer Berechnungen
Zustandsprüfung nach if/else-Verzweigungen
Bestätigung von Eigenschaften der Rückgabewerte nach Prozeduraufrufen
Bereitstellung von Hilfssätzen (Lemmata) für nachfolgende Beweise

8. Datenfluss-Verträge ── Global und Depends

Eines der leistungsfähigsten Merkmale von SPARK sind Datenfluss-Verträge.

Sie deklarieren explizit, welche globalen Variablen ein Unterprogramm liest und schreibt.

package Counter_Unit with SPARK_Mode is

   Count : Natural := 0;

   procedure Increment
     with Global => (In_Out => Count);

   procedure Reset
     with Global => (Output => Count);

   function Get_Value return Natural
     with Global => (Input => Count);

end Counter_Unit;

Die Modi des Global-Vertrags:

Input:  nur lesen (für Funktionen)
Output: nur schreiben (für Initialisierung)
In_Out: lesen und schreiben (für Aktualisierungen)

Darüber hinaus lassen sich Abhängigkeiten zwischen Variablen mit Depends ausdrücken:

procedure Transfer
  (From, To : in out Account_Type)
  with Global => (Input => Exchange_Rate),
       Depends => (From =>+ (From, Exchange_Rate),
                   To   =>+ (To, Exchange_Rate));

=>+ bedeutet „hängt vom vorherigen Wert plus diesen zusätzlichen Eingaben ab”.

Vorteile von Datenfluss-Verträgen:
  1. „Was berührt diese Funktion?" ist auf einen Blick ersichtlich
  2. Unbeabsichtigte Nebenwirkungen werden zur Kompilierzeit erkannt
  3. Sie fließen in die Informationsflussanalyse von Variablen ein
  4. Sie helfen, den Datenfluss in großen Systemen zu visualisieren

9. Beweisstufen ── Schrittweise Einführung von Stone bis Platinum

SPARK definiert das Konzept der Beweisstufen (Proof Levels).

Der Versuch, allen Code auf einmal vollständig zu beweisen, führt oft zur Frustration. SPARK bietet daher eine Strategie, die Strenge des Beweises schrittweise zu erhöhen.

Stone (Stufe 0):
  Nur Prüfung der Vertragssyntax und Typkonsistenz
  Die erste zu erreichende Stufe

Bronze (Stufe 1):
  Stone + Beweis, dass keine uninitialisierten Variablen gelesen werden
  Grundlegende Korrektheitssicherung

Silver (Stufe 2):
  Bronze + Beweis der Freiheit von Laufzeitfehlern (Bereichsüberschreitung,
  Overflow, Division durch Null)
  Das praktischste Ziel

Gold (Stufe 3):
  Silver + Beweis der Pre/Post-Bedingungen
  Garantie vollständiger funktionaler Korrektheit

Platinum (Stufe 4):
  Gold + Beweis der Datenunabhängigkeit und des Informationsflusses
  Für sicherheitskritische Systeme

Eine praktische Einführungsstrategie:

Phase 1: Das gesamte Projekt auf Stone-Stufe bringen
  → Fehler beim Schreiben von Verträgen aufdecken

Phase 2: Wichtige Module auf Silver-Stufe bringen
  → Overflow und Zugriffe außerhalb des Bereichs beseitigen
  → Die meisten praktischen Fehler werden hier erfasst

Phase 3: Kernlogik auf Gold-Stufe beweisen
  → Funktionale Korrektheit mathematisch garantieren
  → Die Korrektheit von Algorithmen beweisen

Phase 4: Bei Sicherheitsanforderungen zu Platinum übergehen
  → Pfade für Informationslecks aufdecken

10. Ein praktischer Beweis-Workflow ── Nacharbeit reduzieren

Hier ein Workflow für die tägliche Nutzung von GNATprove:

1. Typen und Spezifikationen entwerfen
   Bereichseinschränkungen und Typinvarianten festlegen

2. Verträge (Pre/Post) schreiben
   Die Spezifikation vor der Implementierung als Vertrag ausdrücken

3. Kompilieren
   Kompilierfehler mit GNAT beheben

4. GNATprove auf Stone-Stufe ausführen
   gnatprove -P proj.gpr --level=0

5. Warnungen prüfen und Verträge bei Bedarf verfeinern
   Besonders auf Initialisierungsprobleme achten

6. Silver-Stufe anstreben
   gnatprove -P proj.gpr --level=2
   Alle Laufzeitfehler beseitigen

7. Wo nötig, Schleifeninvarianten hinzufügen
   Schlägt ein Beweis fehl, prüfen, ob Invarianten fehlen

8. Funktionale Korrektheit auf Gold-Stufe beweisen
   gnatprove -P proj.gpr --level=3

Häufige „nicht beweisbar”-Situationen und ihr Umgang:

Fall 1: „medium: postcondition might fail"
  → Post-Bedingung zu stark oder Pre-Bedingung zu schwach
  → Oder Schleifeninvarianten unzureichend

Fall 2: „medium: overflow check might fail"
  → Wertebereiche in Pre einschränken
  → Oder den Bereich des Typs selbst verengen

Fall 3: „medium: array index check might fail"
  → Mit einer Schleifeninvariante zeigen, dass der Schleifenbereich
    innerhalb der Array-Grenzen liegt
  → for I in Arr'Range verwenden, um SPARKs automatische
    Bereichserkennung zu unterstützen

Fall 4: „prover timeout"
  → Der Beweiser hat ein Zeitlimit überschritten; mit gestuften
    Invarianten aufteilen
  → Große Funktionen in kleinere aufspalten

11. SPARK und Tests gemeinsam nutzen ── Die komplementäre Beziehung verstehen

Formale Verifikation und Tests sind keine Gegner, sondern ergänzen sich.

SPARK-Beweise:
  Beweisen Eigenschaften für alle möglichen Eingaben
  Decken nur die in Verträgen niedergeschriebenen Eigenschaften ab
  Nicht beweisbare Fälle werden manueller Prüfung oder Tests überlassen

Tests:
  Prüfen das tatsächliche Verhalten für ausgewählte Eingaben
  Können implizite, nicht in Verträgen niedergeschriebene Annahmen aufdecken
  Können das Zusammenspiel mit der Laufzeitumgebung prüfen

Muster für die kombinierte Nutzung:

1. Mit SPARK die Freiheit von Laufzeitfehlern (Silver-Stufe) garantieren
2. Mit Unit-Tests konkrete Ein-/Ausgabe-Korrektheit prüfen
3. Kernlogik auf Gold-Stufe beweisen
4. Tests gezielt auf nicht beweisbare Teile konzentrieren

Ada verfügt mit AUnit über ein Unit-Test-Framework. Eine praxistaugliche Kombination besteht darin, Typen und Verträge mit SPARK zu festigen und das Verhalten mit AUnit zu testen.

12. GNATprove-Ergebnisse lesen ── Meldungen interpretieren

Die Ausgabe von GNATprove kennt drei Schweregrade:

info:    Beweis erfolgreich
medium:  Beweis fehlgeschlagen (Warnung). Manuelle Prüfung nötig
high:    Beweis fehlgeschlagen (Fehler). Vertragsverletzung wahrscheinlich

Häufige Meldungen und ihre Bedeutung:

„postcondition proved"          Die Post-Bedingung wurde bewiesen
„range check proved"            Die Bereichsprüfung wurde bewiesen
„overflow check proved"         Die Freiheit von Overflow wurde bewiesen
„index check proved"            Die Array-Indexgrenzen wurden bewiesen
„divide by zero check proved"   Die Freiheit von Division durch Null wurde bewiesen

„might fail"                    Konnte nicht bewiesen werden
„cannot prove"                  Der Beweiser konnte den Beweis nicht abschließen
„prover timeout"                Der Beweis wurde nicht innerhalb des Zeitlimits abgeschlossen

Vorgehen bei might fail:

1. Den Code lesen und beurteilen, ob er tatsächlich fehlschlagen kann
2. Falls ja, den Code korrigieren
3. Falls es eigentlich nicht fehlschlagen sollte, den Vertrag
   (Pre / Invariante) verstärken
4. Lässt sich immer noch nichts beweisen, mit pragma Assume als
   Annahme deklarieren (Achtung: Assume ist eine unbewiesene Annahme)

13. Integration in reale Projekte

Ein realistischer Ansatz zur Einführung von SPARK in ein bestehendes Projekt:

1. Mit neuem Code beginnen
   Nicht versuchen, den gesamten Bestandscode auf einmal SPARK-fähig zu machen
   SPARK_Mode für neu geschriebene Module aktivieren

2. Silver anstreben
   Gold (vollständiger funktionaler Beweis) ist ideal, aber man beginnt
   mit Silver (keine Laufzeitfehler)
   Schon die reine Vermeidung von Overflow hat enormen praktischen Wert

3. Verträge ausgehend von Schnittstellen schreiben
   Verträge vor der Implementierung in die Paketspezifikation (.ads) schreiben
   Bei einer soliden Spezifikation kann jeder Implementierer Code schreiben,
   der die Verträge erfüllt

4. In CI/CD integrieren
   gnatprove in die CI-Pipeline aufnehmen
   Den Build bei Beweisfehlern stoppen (oder zumindest warnen)

5. Beweisberichte sammeln
   Berichte mit gnatprove --report=all erzeugen
   Die Entwicklung unbewiesener Punkte über die Zeit verfolgen

Für Projekte mit gemischtem C/C++- und Ada-Code eignet sich ein gestufter Ansatz:

1. Neue Module in Ada/SPARK schreiben
2. Mit C/C++ über Interfaces.C kommunizieren
3. Kritische Datenstrukturen und Verifikationslogik nach SPARK migrieren
4. Den SPARK-Umfang schrittweise erweitern

14. Grenzen und Vorbehalte von SPARK

Auch SPARK ist kein Allheilmittel. Die eigenen Grenzen ehrlich zu verstehen führt zur richtigen Anwendung.

Was SPARK beweisen kann:
  SPARK beweist ausschließlich die in Verträgen niedergeschriebenen
  Eigenschaften
  Vergessene Eigenschaften (die man nicht aufgeschrieben hat) werden
  nicht bewiesen
  Beispiel: Der Beweis, dass das Ergebnis in Post sortiert ist,
  garantiert nicht, dass die ursprünglichen Elemente erhalten bleiben,
  sofern man das nicht ebenfalls aufschreibt

Grenzen der Beweiser:
  Manche komplexen Eigenschaften übersteigen die Fähigkeiten
  automatischer Beweiser
  In solchen Fällen ist interaktiver Beweis (z. B. mit Coq) nötig
  Dennoch genügt automatisches Beweisen für die meisten praktischen Fälle

Sprachliche Einschränkungen:
  Code mit intensiver Zeigernutzung lässt sich nicht SPARK-fähig machen
  Der Beweis dynamischer Speicherallokation ist begrenzt
  Der Beweis rekursiver Datenstrukturen ist schwierig

Erfahrung der Entwickler:
  Das Schreiben von Verträgen erfordert Übung
  Der Entwurf von Schleifeninvarianten ist besonders zeitaufwendig zu erlernen
  Ein teamweiter Weiterbildungsplan ist unerlässlich

15. Fazit ── Beweis als Teil der täglichen Entwicklung

Wir haben die Praxis der formalen Verifikation mit SPARK durchlaufen.

SPARK ist eine Teilmenge von Ada, eingeschränkt auf verifizierbare Merkmale
Verträge (Pre/Post) sind die Eingabe für Beweise. Ada-2012-Verträge
funktionieren direkt
GNATprove führt automatische Beweise aus und meldet Ergebnisse auf
Quellcodeebene
Schleifeninvarianten beweisen Eigenschaften von Schleifen
Global/Depends machen den Datenfluss explizit und verwalten
Nebenwirkungen
Beweisstufen (Stone bis Platinum) erlauben eine schrittweise Erhöhung
der Strenge
Zunächst die Silver-Stufe (keine Laufzeitfehler) anzustreben ist die
praktische Empfehlung
Tests und Beweise sind keine Gegensätze – sie ergänzen sich

Möglicherweise besteht die Vorstellung, „formale Verifikation sei zu schwierig und nur für besondere Projekte geeignet”.

Doch die heutige Kombination aus SPARK und GNATprove hat folgendes Niveau erreicht:

1. Einen Vertrag schreiben. Das ist im Grunde dieselbe Entwurfstätigkeit
   wie das Schreiben von Typen oder Tests
2. gnatprove ausführen. Es fühlt sich an wie eine Kompilierung
3. Die Ergebnisse betrachten und entweder Code oder Vertrag korrigieren

Dieser Zyklus unterscheidet sich nicht vom alltäglichen Entwicklungsablauf, bei dem man Code anhand von Compiler-Fehlermeldungen korrigiert.

Der Unterschied ist: Während ein Compiler garantiert, dass „die Syntax korrekt ist”, garantiert GNATprove „korrekt für alle Eingaben”.

Das im vorherigen Artikel vorgestellte Motto von Ada – „Fehler werden nicht gefunden; Typen und Verträge machen es unmöglich, sie überhaupt zu schreiben” – geht mit SPARK auf die nächste Stufe:

Die Abwesenheit von Fehlern wird durch Beweis garantiert.

Beginnen Sie damit, SPARK_Mode und ein Post an eine kleine Funktion anzuhängen und gnatprove auszuführen.

Wenn Sie die grüne Meldung postcondition proved sehen, wird sich Ihre Sicht auf die Qualitätssicherung von Software verändern.

Referenzen

Verwandte Artikel

Aktuelle Artikel mit denselben Schlagwörtern führen zu verwandten Themen weiter.

Verwandte Themen

Diese Seiten ordnen den Artikel in einen größeren Leistungs- und Entscheidungskontext ein.

Häufige Fragen

Fragen, die in Beratungen zu diesem Artikelthema häufig gestellt werden.

Was ist SPARK, und wie verhält es sich zu Ada?
SPARK ist eine bewusst eingeschränkte Teilmenge von Ada, die so gestaltet ist, dass sich Programmeigenschaften mathematisch beweisen lassen. Sie schränkt schwer verifizierbare Merkmale ein – freie Zeigernutzung, uneingeschränkte Ausnahmebehandlung, rekursive Datenstrukturen und freie Nebenläufigkeit – und erhält dafür Beweisbarkeit. SPARK-Code ist Ada-Code plus Vertragsannotationen, also eine natürliche Erweiterung der gewohnten Ada-Entwicklung und keine eigene Sprache. Das zentrale Werkzeug ist GNATprove von AdaCore: Es übersetzt Verträge in die Zwischensprache Why3 und versucht Beweise mit automatischen Beweisern wie Z3, CVC4 und Alt-Ergo.
Worin unterscheidet sich formale Verifikation mit SPARK von Tests?
Tests prüfen, ob das Programm für ausgewählte Eingaben korrekt arbeitet; formale Verifikation beweist mathematisch, dass eine Eigenschaft für alle möglichen Eingaben gilt. Beide ergänzen sich, statt zu konkurrieren: SPARK beweist ausschließlich die im Vertrag festgehaltenen Eigenschaften, während Tests auch implizite, nirgends niedergeschriebene Annahmen aufdecken und das Zusammenspiel mit der Laufzeitumgebung prüfen können. In der Praxis bewährt sich die Kombination, mit SPARK die Freiheit von Laufzeitfehlern zu garantieren, mit Unit-Tests konkretes Ein-/Ausgabeverhalten zu prüfen und Tests gezielt dort einzusetzen, wo kein Beweis gelingt.
Was sind die SPARK-Beweisstufen, und welche sollte man zuerst anstreben?
SPARK definiert fünf Stufen zunehmender Strenge: Stone (Syntax der Verträge und Typkonsistenz), Bronze (zusätzlich Beweis, dass keine uninitialisierten Werte gelesen werden), Silver (zusätzlich Beweis der Freiheit von Laufzeitfehlern wie Overflow, Bereichsverletzungen und Division durch Null), Gold (zusätzlich Beweis der funktionalen Korrektheit über Pre/Post) und Platinum (zusätzlich Beweis der Datenunabhängigkeit und des Informationsflusses). Silver ist das praktischste erste Ziel – die meisten realen Fehler werden bereits durch die Beseitigung von Laufzeitfehlern erfasst –, und Gold lohnt sich für Kernlogik, deren Korrektheit garantiert werden muss.
Was ist eine Schleifeninvariante, und warum braucht ein SPARK-Beweis eine?
Eine Schleifeninvariante ist eine Eigenschaft, die zu Beginn jeder Schleifeniteration gilt und mit pragma Loop_Invariant geschrieben wird. Schleifen laufen eine beliebige Anzahl von Malen, sodass der Beweiser die Invariante braucht, um über alle Iterationen hinweg zu argumentieren – sie drückt die bisherige Teilberechnung als Formel aus, und nach der letzten Iteration muss sie die gewünschte Nachbedingung implizieren. Das Entwerfen von Invarianten ist die anspruchsvollste Fertigkeit bei Schleifenbeweisen: Eine zu starke Invariante lässt sich nicht beweisen, eine zu schwache impliziert die Nachbedingung nicht.

Autorenprofil

Profilseite des Artikelautors.

Go Komura

Geschäftsführer von KomuraSoft LLC

Spezialisiert auf Windows-Softwareentwicklung, technische Beratung und Fehleranalyse, insbesondere bei bestehenden Systemen und schwer reproduzierbaren Störungen.

Kontakt

Öffentliche Links

GitHub LinkedIn X COM_BLAS COM_BigDecimal
Zurück zum Blog