Dafny

Klassische "Design by Contract" Syntax. requires x != 0 (Vorbedingung). invariant i < n (Schleifen-Invariante). Wenn du die Invariante vergisst, meckert Dafny: "Loop might not terminate" oder "Index out of bounds". Wenn es kompiliert, hast du die Garantie, dass keine Runtime-Exceptions (außer OOM) passieren.

1. Z3 SMT Solver

Dafny ist "nur" ein Frontend. Die Schwerarbeit macht Z3 (auch Microsoft). Ein SMT (Satisfiability Modulo Theories) Solver. Er kann Gleichungssysteme mit Millionen Variablen lösen. Dafny übersetzt deinen Code in eine riesige logische Formel ("Verification Condition") und fragt Z3: "Ist das immer wahr?".

2. Auto-Active Verification

Ein Begriff, den Dafny geprägt hat. Es ist nicht voll-automatisch (wie Coverity), man muss Specs schreiben. Es ist nicht voll-interaktiv (wie Coq), man muss keine Beweisschritte tippen. Man interagiert mit dem Solver, indem man den Code/Specs ändert ("Leite den Solver").

1. VC Generation (Verification Condition)

Wie "sieht" Dafny deinen Code? Es wandelt ihn in eine Zwischensprache namens Boogie um. Boogie generiert daraus Verification Conditions (VCs). Das sind gigantische mathematische Formeln der Form: $\forall x, y \in \mathbb{Z} : (\text{Pre}(x,y) \land \text{Loop}(x,y,k)) \implies \text{Post}(x,y)$. Z3 versucht dann, ein Gegenbeispiel zu finden. Wenn Z3 beweist, dass kein Gegenbeispiel existiert, gilt die Methode als verifiziert. In der Produktion kann ein einzelner assert oder eine komplexe Invariante die VC-Größe explodieren lassen, was zu Timeouts im Solver führt ("Prover failed").

2. Ghost Variables & Functions

Ein mächtiges Feature sind Ghost Constructs. Das sind Variablen oder Funktionen, die nur für den Beweis existieren. ghost var sum := 0; Man kann darin komplexe mathematische Werte sammeln, um Invarianten zu beweisen. Beim Kompilieren (zu C# oder Go) wird der gesamte "Ghost-Code" restlos entfernt. Dadurch hat man zur Laufzeit null Performance-Verlust, obwohl man im Code extrem komplexe mathematische Prüfungen mitschleppt. Es ist wie eine "Safety-Wall", die beim Bauen des Hauses da ist, aber verschwindet, wenn man einzieht.

3. Frame Specifications (Reads & Modifies)

In der Objektorientierung (Heap) ist das größte Problem der Aliasing-Effekt. Wenn zwei Pointer auf das gleiche Objekt zeigen und ich eines ändere... was passiert mit dem anderen? Dafny erzwingt Frame Specifications: modifies this.data reads other.config Dafny beweist, dass eine Methode nur die Dinge ändert, die sie explizit nennt. Das erlaubt es dem Solver, sicher zu sein, dass andere Teile des Speichers stabil bleiben. Ohne dieses "Framing" wäre die Verifikation von komplexen Datenstrukturen wie verketteten Listen oder Bäumen mathematisch unmöglich.