Alloy ist eine deklarative Spezifikationssprache von Daniel Jackson und seiner Gruppe am MIT (Software Design Group) — ein Vertreter der „Lightweight Formal Methods". Statt vollständiger Beweise liefert der Alloy Analyzer automatisch Instanzen und Gegenbeispiele zu einem Modell, typischerweise innerhalb von Sekunden. Die Sprache baut auf relationaler Logik erster Ordnung auf und wird in Java-ähnlicher Syntax geschrieben.
Bausteine
sig User { following: set User }
fact NoSelfFollowing { all u: User | u not in u.following }
pred HasFollower[u: User] { some u.~following }
run HasFollower for 5
assert NoTransitiveClose { all u: User | no (u.following & u.following.following) }
check NoTransitiveClose for 4sigdeklariert einen Typ (Menge von Atomen), Felder sind Relationen.factsind immer gültige Einschränkungen des Modells.pred/fundefinieren wiederverwendbare Bedingungen beziehungsweise Ausdrücke.assertformuliert eine Behauptung;checksucht ein Gegenbeispiel.runsucht eine Instanz, in der das Prädikat gilt.
Relationale Operatoren und Quantoren
Mengen und Relationen werden kombiniert mit -> (Produkt), . (Join), +/-/& (Vereinigung, Differenz, Schnitt), ~ (Transposition), ^/* (transitive Hülle), in, =, univ, iden. Quantoren: all, some, no, lone, one; Kardinalität schreibt man als #.
Analyse
Der Analyzer übersetzt das Modell über Kodkod (einen relationalen Modell-Finder von Emina Torlak) in eine SAT-Instanz und löst sie mit Standard-SAT-Solvern. Weil die Suche auf eine Scope begrenzt ist (z. B. for 5 Atome pro Signatur), sind die Analysen vollständig automatisch — anders als beim interaktiven Beweisen mit Isabelle. Alloy eignet sich für Architektur-Analysen, Zugriffskontrollmodelle, Datenbankschemata und Sicherheitsdesigns.
Wer neben den statischen Strukturen auch zeitliches Verhalten nebenläufiger Systeme prüfen will, nutzt TLA+ mit seinem Model Checker TLC; ausführbare Prozessmodelle prüfen Promela und SPIN, mathematische Spezifikationen schreibt man in der Z-Notation.