|
Philosophy
Software development is difficult;
choosing correct abstractions to base your
design around is a tricky process! Quite often
apparently simple and robust designs can turn
out to be incoherent and even inconsistent
when you come to implement them.
One way to avoid this problem of
"wishful thinking" as well as making
software development more straightforward
is through formal specification. This method
approaches software abstraction head-on using
precise and unambiguous notation, one such
example is the declarative language Z.
Naturally this is not fool proof either though;
proving your specification is correct/sound requires
a substantial amount of effort. Whilst conventional
theorem based analysis tools have improved, their
level of automation is still relatively poor
compared to model checkers.
Hence, Alloy was developed in the hope of adapting a
declarative language like Z to bring in fully automatic
analysis. To do this Alloy sacrifices the ability to
totally prove a system's correctness. Rather, it attempts
to find counterexamples within a limited scope that violate
the constraints of the system. Thus by combining the
best of both worlds Alloy produces a rigorous model
that gives the user immediate feedback
|
Main Developer
Professor Daniel Jackson
|
History
The design was done by the Software Design Group at MIT
lead by Professor Daniel Jackson. In 1997 they produced
the first Alloy prototype, which was then a rather limited
object modelling language. Over the years Alloy has developed
into a full structural modelling language capable of expressing
complex structural constraints and behaviour.
By employing first order logic, Alloy is able to translate
specifications into large Boolean expression that can be
automatically analyzed by SAT solvers. Thus when given a logical
formula (in Alloy), the Alloy Analyzer can attempt to find a
model which satisfies it.
One of the great benefits this lends to Alloy is the ability of
incremental analysis. A programmer may explore design ideas starting
from a tiny model which is then scaled up, with Alloy able to
analyse it at every step.
Alloy has gradually improved in performance and scalability and been
applied to many fields including scheduling, cryptography and
instant messaging.
|
Links
For more information on Alloy, we recommend the following:
Downloads
You can download the Alloy Analyzer from the following sources: