What Came Before: Theorem
only need to express the property you
want to check rather than a large col-
lection of test cases. And the analysis is
much more complete than testing, be-
cause it effectively covers all (or almost
all) test cases that you could have writ-
ten by hand.
Provers and Model Checkers
To understand Alloy, it helps to know
a bit about the context in which it was
developed and the tools that existed at
Theorem provers are mechanical aids
for constructing mathematical proofs.
To apply a theorem prover to a software
design problem, you formulate some
intended property of the design, and
then attempt to prove the theorem that
the property follows from the design.
Theorem provers tend to provide very
rich logics, so they can usually express
any property the designer might want,
at least about states and state transitions—more dynamic properties can
require a temporal logic that theorem
provers don’t typically support directly.
Also, because they generate mathemat-
ical proofs, which can be checked by
tools that are smaller and simpler than
the tool that finds the proof, you can be
confident the analysis is sound.
On the down side, the combination
of an expressive logic and sound proof
means that finding proofs cannot generally be automated. Theorem provers
usually require considerable effort and
expertise from the user, often orders
of magnitude greater than the effort
of constructing a formal design in the
first place. Moreover, failure to find a
proof does not mean that a proof does
not exist, and theorem provers don’t
provide counterexamples that explain
concretely why a theorem is not valid.
So theorem provers are not so useful
when the intended property does not
hold—which unfortunately is the common case in design work.
Model checkers revolutionized de-
sign analysis by providing exactly the
features theorem provers lacked. They
offer push-button automation, requir-
ing the user to give only the design and
property to be checked. They allow
dynamic properties to be expressed
(through temporal logics), and gener-
ate counterexamples when properties
do not hold. Model checkers work by
exploring the space of possible states
of a system, and if that space is large,
they may require considerable compu-
tational resources (or may fail to termi-
nate). The so-called “state explosion”
problem arises because model check-
ers are often used to analyze designs
involving components that run in par-
allel, resulting in an overall state space
that grows exponentially with the num-
ber of components.
Alloy was inspired by the successes
and limitations of model checkers.
For designs involving parallelism and
simple state (comprising Boolean
variables, bounded integers, enumerations and fixed-size arrays), model
checkers were ideal. They could easily find subtle synchronization bugs
that appeared only in rare scenarios
that involved long traces with multiple context switches, and therefore
For hardware designs, model checkers were often a good match. But for
software designs they were less ideal.
Although some software design
problems involve this kind of synchronization, often the complexity arises
from the structure of the state itself. Early