Alloy Specification Language
Table of Contents
1. Introduction
Alloy is a lightweight formal specification language for software modeling, based on first-order relational logic with transitive closure.
1.1. Key Characteristics
- Declarative relational modeling
- Bounded model checking (SAT-based)
- Automatic counterexample generation
- Small scope hypothesis
3. Core Concepts
3.1. Signatures and Relations
sig Node {
edges: set Node
}
sig Graph {
nodes: set Node
}
fact acyclic {
no n: Node | n in n.^edges
}
6. Example: Redirect Termination
Proving that a web redirect chain always terminates.
6.1. 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
7. Resources
- Alloy Analyzer
- Alloy Tutorial
- Software Abstractions (Jackson, 2012)