Alloy Specification Language
Table of Contents
Introduction
Alloy is a lightweight formal specification language for software modeling, based on first-order relational logic with transitive closure.
Key Characteristics
- Declarative relational modeling
- Bounded model checking (SAT-based)
- Automatic counterexample generation
- Small scope hypothesis
Alloy vs TLA+ vs Lean4
Core Concepts
Signatures and Relations
sig Node {
edges: set Node
}
sig Graph {
nodes: set Node
}
fact acyclic {
no n: Node | n in n.^edges
}
State Machine Pattern
Bounded Model Checking
Integration with Scheme
Example: Redirect Termination
Proving that a web redirect chain always terminates.
Model
sig URL {}
sig RedirectMap {
redirect: URL -> lone URL
}
pred terminates[m: RedirectMap] {
no u: URL | u in u.^(m.redirect)
}
assert AllRedirectsTerminate {
all m: RedirectMap | terminates[m]
}
check AllRedirectsTerminate for 10
Resources
- Alloy Analyzer
- Alloy Tutorial
- Software Abstractions (Jackson, 2012)