TLA+

Viele Programmierer denken in "Code". Leslie Lamport (Erfinder von Paxos, LaTeX) denkt in Mathe. Er sagt: "Ein System ist eine mathematische Formel." TLA+ ist eine Sprache, um Systeme (wie Cloud-Datenbanken) mathematisch präzise zu spezifizieren. Kein "vielleicht", kein "ungefähr". Man schreibt auf: $Next == x' = x + 1$. Dann lässt man den TLC Model Checker laufen. Er prüft JEDEN möglichen Ablauf. Amazon (AWS) nutzt es massiv (für DynamoDB, S3), um Bugs zu finden, die man durch Testen nie finden würde ("Design Flaws").

Merksatz: Eine von Leslie Lamport entwickelte formale Spezifikationssprache, die auf Mengenlehre und temporaler Logik basiert, um komplexe verteilte Algorithmen zu modellieren und zu verifizieren.

Du schreibst kein Programm. Du schreibst eine Spezifikation. Variables: status Init: status = "ready" Next: status = "ready" /\ status' = "busy" \/ status = "busy" /\ status' = "done" Spec: Init /\ [][Next]_status Dann definierst du Invarianten ("Es darf nie Status 'error' geben"). Der TLC-Checker prüft das.

1. PlusCal

Mathematik ist schwer. Viele Ingenieure hassten die TLA+ Syntax ($\land, \lor, \in$). Lamport erfand PlusCal. Sieht aus wie Pseudo-Code (C-Style). Ein Transpiler übersetzt es in reines TLA+. Damit wurde es in der Industrie (Microsoft, Amazon) populär.

2. Refinement Mapping

Das mächtigste Feature. Du schreibst eine abstrakte Spec (High-Level). Du schreibst eine konkrete Spec (Low-Level, mit Optimierungen). TLA+ kann beweisen: "Die konkrete Spec implementiert die abstrakte Spec korrekt." Das ist der Heilige Gral der Verifikation.

1. Safety vs. Liveness

TLA+ unterscheidet strikt zwei Arten von Fehlern:

Safety ("Nichts Schlechtes passiert"): "Zwei Prozesse halten nie gleichzeitig den Mutex." Das prüft der TLC, indem er alle Zustände absucht. (Einfacher).
Liveness ("Etwas Gutes passiert irgendwann"): "Jede Anfrage wird irgendwann beantwortet." Das ist viel schwerer. Es erfordert die Prüfung von unendlichen Pfaden. TLA+ nutzt dafür Fairness-Annahmen (Weak/Strong Fairness), um zu garantieren, dass das System nicht ewig "untätig" bleibt oder einen Prozess verhungern lässt.

2. State Space Explosion & Symmetry

In einem System mit 10 Prozessen gibt es Trillionen Zustände. Der TLC-Checker würde sterben. In der Produktion nutzt man Symmetry Sets. Man sagt TLA+: "Alle Server sind identisch." Anstatt Server A und Server B separat zu prüfen, betrachtet der Checker sie als eine Klasse. Wenn es für Server 1 und 2 funktioniert, funktioniert es auch für 2 und 1. Das reduziert den Suchaufwand oft um den Faktor $N!$ (Fakultät), was den Unterschied zwischen 10 Jahren und 10 Minuten Rechenzeit ausmacht.

3. Model Checking vs. Theorem Proving

TLA+ ist nicht nur ein Model Checker (der alles ausprobiert). Es gibt auch den TLAPS (TLA+ Proof System). Damit kann man mathematische Beweise schreiben, die für unendlich große Systeme gelten (wo kein Model Checker der Welt hinkommt). Microsoft nutzt das für die Verifikation von Cloud-Komponenten. Es ist die "Champions League" der Informatik: Man schreibt Formeln, die beweisen, dass der Code unter allen physikalischen Bedingungen korrekt sein muss.