Home

Alloy: A Simple Structural Modeling Language Based on First-Order Logic

The Alloy Analyzer is a tool developed by the Software Design Group for analyzing models written in Alloy, a simple structural modeling language based on first-order logic. The tool can generate instances of invariants, simulate the execution of operations (even those defined implicitly), and check user-specified properties of a model. Alloy and its analyzer have been used primarily to explore abstract software designs. Its use in analyzing code for conformance to a specification and as an automatic test case generator are being investigated in ongoing research projects.

Alloy has been mentioned before, but with the recent discussions revolving around IDEs and questions about whether some kinds of checking belong in the language or in the tools surrounding the language, I thought it might be worth revisiting. In fact, it's tempting to suggest that we at LtU adopt a new category for stories: "Lightweight Formal Methods," and that we editors attempt to establish a continuum with respect to stories that fit the category. For example, Pierce makes the observation in TAPL that type systems are a particular kind of lightweight formal method, and that one of their benefits is that they're the only kind that are guaranteed to be used. Alloy falls in the "outside the language proper, but still incremental" category, and somewhere else on the spectrum you have full-blown theorem provers like Twelf, Coq, MetaPRL, et al. Does it make sense to try to unify some of the discussions about the boundary between languages and external tools under this umbrella?

By Paul Snively at 2005-10-30 23:58 | DSL | Software Engineering | other blogs | 16483 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Outstanding

I'm a little surprised that this tool hasn't generated a bit more buzz. In the course of building a model-checker that's proven surprisingly versatile in debugging industrial technologies and protocols (e.g. COM), they also built a very expressive language that manages to unify some aspects of relations, sets, and object classes. I'd love to see programming languages built around a syntax like Alloy's...

By erk at Wed, 2005-11-02 11:53 | login or register to post comments

Agreed

I should have mentioned that Alloy's language does a very interesting job of relating FOL, basic set theory, and objects. Also that several extremely useful Alloy models are in the 100-200 line range. That's one reason it's a Lightweight Formal Method: as compared to my rants about type systems :-) you can do as much or as little Alloy as you like, and even a complete model is likely to be very compact.

Minor nit: as the site points out, Alloy isn't a model checker, bur rather a model refuter: given a model, it generates gazillions of instances very quickly and looks for counterexamples. As a consequence, it's conservative, but appropriate modularization can make the phase-space of the portion of the model being checked more than tractable, e.g. you can reduce the probability of the failure to find a counterexample that does exist to below that of your system failing due to being struck by random cosmic radiation, at which point all you can do is declare victory and retreat.

By Paul Snively at Thu, 2005-11-03 04:38 | login or register to post comments

Lightweight Formal Methods

In fact many of these tools and techniques were discussed here in the past. I quite agree with Paul that this topic is closely related to PLT and especially type theory.

Types are not just "guaranteed to be used", they are alos guaranteed to be in sync with what the actual code does.

By Ehud Lamm at Wed, 2005-11-02 20:32 | login or register to post comments

And Rice...

The discussion of the Rice theorem in another thread reminded my of a related discussion relevant to the distinction between types and tools .

By Ehud Lamm at Thu, 2005-11-03 22:50 | login or register to post comments