ALLOY IS A language and a toolkit for exploring the kinds
of structures that arise in many software designs. This
article aims to give readers a flavor of Alloy in action, and
some examples of its applications to date, thus giving a
sense of how it can be used in software design work.
Software involves structures of many sorts:
architectures, database schemas, network topologies,
ontologies, and so on. When designing a software
system, you need to be able to express the structures
essential to the design and to check that they have the
properties you expect.
You can express a structure by sketching it on a
napkin. That’s a good start, but it’s limited. Informal
representations give inconsistent interpretations, and
they cannot be analyzed mechanically. So people have
turned to formal notations that define structure and
behavior precisely and objectively, and that can exploit
the power of computation.
By using formality early in development, you can minimize the costs of
ambiguity and get feedback on your
work by running analyses. The most
popular approach to advocate this is
agile development, in which the formal
representation is code in a traditional
programming language and the analysis is conventional unit testing.
As a language for exploring designs,
however, code is imperfect. It’s verbose
and often indirect, and it does not allow partial descriptions in which some
details are left to be resolved later. And
testing, as a way to analyze designs,
leaves much to be desired. It’s notori-
A Language and
ously incomplete and burdensome,
since you need to write test cases ex-
plicitly. And it’s very difficult to use
code to articulate design without get-
ting mired in low-level details (such as
the choice of data representations).
An alternative, which has been ex-
plored since the 1970s, is to use a de-
sign language built not on convention-
al machine instructions but on logic.
Partiality is free because rather than
listing each step of a computation, you
write a logical constraint saying what’s
true after, and that constraint can say
as little or as much as you please. To
analyze such a language, you use spe-
cialized algorithms such as model
checkers or satisfiability solvers (more
on these later). This usually requires
much less effort than testing, since you
Tool for Exploring
Exploiting a simple, expressive logic based
on relations to describe designs and automate
BY DANIEL JACKSON
˽ Using a simple logic of relations, Alloy
lets you model software designs that
involve complex, evolving structures.
˽ Alloy’s tool uses SAT technology to
simulate designs and find subtle flaws,
and has been used in a wide variety
of applications from networking and
security to critical systems.
˽ A key advantage of logical modeling is that
you can construct a design incrementally,
in an agile way, representing and
analyzing only an essential subset of
the behavioral contraints.
˽ Alloy is complementary to a class
of tools called model checkers, and
is a valuable addition to the software