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 BeweisstandWarum „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.