Why3 ist eine Software-Verifikationsplattform, die am französischen Forschungsinstitut INRIA und der Université Paris-Sud entstanden ist (Jean-Christophe Filliâtre, Andrei Paskevich, Claude Marché, Guillaume Melquiond, François Bobot). Die Idee hinter Why3 fasst der Slogan „Shepherd your herd of provers" zusammen: Man schreibt ein Programm mit Spezifikation in der ML-artigen Sprache WhyML, und Why3 erzeugt daraus automatisch Proof Obligations (Beweisverpflichtungen), die an eine „Herde" verschiedener Beweiser verteilt werden.

Erste Schritte

why3 config                  # installierte Beweiser erkennen (Alt-Ergo, Z3, CVC4/CVC5, E)
why3 prove datei.mlw         # alle Proof Obligations auf der Kommandozeile beweisen
why3 ide datei.mlw           # grafische Oberfläche: Ziele, Beweisversuche, Strategien
why3 replay datei.mlw        # gespeicherte Beweise erneut ausführen (nach Änderungen)
why3 session html datei.mlw  # HTML-Bericht über den Beweisstand

Warum „Herde von Beweisern"?

• Automatische Beweiser wie Alt-Ergo, Z3 oder CVC5 lösen viele Ziele allein; der Aufruf erfolgt pro Ziel über why3 prove -P <beweiser> datei.mlw.
• Schwierige Ziele gehen an interaktive Assistenten wie Coq, Isabelle oder PVS — Why3 verwaltet die Beweisstrategien für alle.
• WhyML-Spezifikationen stehen in geschweiften Klammern, z. B. let f (x: int) : int ensures { result > 0 } = ....

Einordnung

Why3 ist das Verifikations-Backend hinter Frama-C: Das WP-Plugin übersetzt ACSL-Annotationen in WhyML und delegiert die Beweisverpflichtungen an dieselben Beweiser. Interaktive Assistenten wie HOL können in dieser Kette als Beweis-Backend für besonders anspruchsvolle Ziele dienen. Formale Methoden wie VDM verfolgen dieselbe Idee — Spezifikation vor Implementierung — mit anderer Werkzeugkette.

Verwandte Grundlagen: Frama-C-Befehle, ACSL, Coq-Befehle.

HOL steht für Higher-Order Logic (Logik höherer Stufe) und bezeichnet zugleich eine Familie interaktiver Beweisassistenten, die auf das LCF-System (Logic for Computable Functions, Robin Milner, Edinburgh 1970er) zurückgehen. Kernidee: Ein minimaler, vertrauenswürdiger Kernel akzeptiert nur Schlussfolgerungen, die durch elementare Regeln abgesichert sind — jedes Theorem ist damit maschinell geprüft.

Die HOL-Familie

• HOL4 ist der aktiv weiterentwickelte Hauptnachkomme, läuft auf Poly/ML, Lizenz BSD, mit dem Build-Werkzeug Holmake.
• HOL Light (John Harrison, Cambridge/Microsoft) ist ein minimalistischer OCaml-Fork mit sehr kleinem Kernel (~400 Zeilen) — extrem hohe Vertrauenswürdigkeit.
• Isabelle/HOL ist der bekannteste Abkömmling der HOL-Ideen: Isabelle nutzt eine generische Logik-Infrastruktur und darauf aufgesetzt die HOL-Logik.

Arbeiten im Goalstack

poly               # Poly/ML-REPL starten
Holmake            # HOL4-Theorien bauen (make-Ersatz)
g `1 + 1 = 2`;     # Goal setzen (Backticks um das Ziel)
e (REWRITE_TAC []);# Taktik anwenden
e (DECIDE_TAC);    # arithmetische Entscheidungsprozedur
top_thm();         # bewiesenes Theorem anzeigen

Typische Taktiken: REWRITE_TAC (mit Theoremen umschreiben), STRIP_TAC (Annahmen/Hüllen auflösen), GEN_TAC (Allquantor einführen), MESON_TAC/METIS_TAC (Prädikatenlogik-Suche), DECIDE_TAC/TAUT_TAC (Arithmetik/Aussagenlogik), Induct_on (strukturelle Induktion).

Einordnung

HOL beweist Korrektheitseigenschaften interaktiv — im Gegensatz zu Plattformen, die Beweise weitgehend automatisieren: Why3 verteilt Proof Obligations an Beweiser, und Coq, Lean und PVS verfolgen ähnliche Ansätze. In Verifikationsketten wie Frama-C mit ACSL-Spezifikationen übernimmt ein interaktiver Assistent die Ziele, die automatische Beweiser nicht schließen.

Verwandte Grundlagen: Isabelle-Befehle, Coq-Befehle, Lean-Befehle.

ACSL (ANSI/ISO C Specification Language) ist eine formale Spezifikationssprache für C-Programme, entwickelt im Frama-C-Projekt. Ihr Design ist von JML (Java Modeling Language) inspiriert und erbt viel von Caduceus, einem früheren Analysewerkzeug. Mit ACSL beschreibt man das Verhalten von C-Funktionen präzise — als Verträge mit Vorbedingung, Nachbedingung und Frame-Regel — und lässt diese Eigenschaften anschließend maschinell beweisen.

Syntax: Annotationen als Kommentare

/*@ requires n >= 0;
  @ ensures 
esult == n * (n + 1) / 2;
  @ assigns 
othing;
  @*/
int summe(int n) {
  int s = 0;
  /*@ loop invariant 0 <= i <= n && s == i * (i - 1) / 2;
    @ loop assigns s, i;
    @ loop variant n - i;
    @*/
  for (int i = 1; i <= n; i++) s += i;
  return s;
}

Wichtige Konstrukte

• requires — Vorbedingung (Precondition), die der Aufrufer garantieren muss.
• ensures — Nachbedingung (Postcondition), die die Funktion garantiert.
• assigns — Frame-Regel: welche Speicherbereiche die Funktion verändern darf.
• loop invariant / loop variant — Schleifeninvariante und Terminierungsargument.

Logische Terme

ACSL stellt spezielle Terme bereit: esult (Rückgabewert), old(ausdruck) (Wert vor dem Funktionsaufruf), valid(zeiger) (gültiger Speicherbereich), valid_range, length, othing (leere Frame-Regel), ull, rue/false.

Einordnung

ACSL wird von den Frama-C-Plugins verarbeitet: WP (Weakest Precondition) erzeugt Beweisverpflichtungen, die Why3 an Beweiser wie Alt-Ergo oder Z3 delegiert; EVA analysiert mit abstrakter Interpretation; E-ACSL übersetzt Annotationen in Laufzeitprüfungen. Damit steht ACSL in einer Reihe mit anderen formalen Spezifikationssprachen: VDM und Z-Notation spezifizieren auf höherer Ebene, HOL-Assistenten können die erzeugten Verpflichtungen interaktiv beweisen.

Verwandte Grundlagen: Frama-C-Befehle, Why3-Befehle, C/C++-Befehle.

Frama-C ist eine Open-Source-Plattform zur Analyse von C-Quellcode; sie bündelt mehrere Analysetechniken in einem gemeinsamen Rahmenwerk. Die formale Spezifikationssprache heißt ACSL (ANSI/ISO C Specification Language), ausgewählte Plug-ins führen statische Analyse und Verifikation durch.

Aufruf von der Kommandozeile

frama-c -eva datei.c              # abstrakte Interpretation (Werte)
frama-c -wp datei.c               # Schwaechste-Vorbedingung, Beweis
frama-c -wp -wp-prover alt-ergo datei.c
frama-c -metrics datei.c          # Metriken
frama-c -gui datei.c              # graphische Oberflaeche (frama-c-gui)

Das EVA-Plug-in (ab 18.0; vorher VALUE) überapproximiert die möglichen Werte von Variablen an jedem Programmpunkt und findet so Laufzeitfehler wie Überläufe oder Zugriffe außerhalb von Feldgrenzen. Das WP-Plug-in implementiert einen Weakest-Precondition-Kalkül und erzeugt Verifikationsbedingungen (VCs), die an externe Beweiser wie Alt-Ergo, Z3 oder CVC4 gehen.

ACSL-Annotationen

/*@ requires 0 <= n && n < 100;
  @ ensures  
esult == n * n;
  @*/
int quadrat(int n) { return n * n; }

• requires: Vorbedingung, ensures: Nachbedingung, assigns: erlaubte Seiteneffekte.
• //@ assert p;: lokale Behauptung, //@ loop invariant: Schleifeninvariante.
• esult, old(expr), valid(p), separated(...): Terme für Rückgabe, Alt-Werte, Zeiger-Gültigkeit.

Frama-C ergänzt die Beweisassistenten-Familie um eine C-spezifische, praktische Verifikation: verwandt sind VDM, PVS und SPIN/Promela; als C-Anker dient C/C++-Befehle.