[13 February 2009]

In the last couple of years I have become rather fond of a tool called Alloy. I’ve been talking to a couple of people about it lately, and this week I had an extremely enlightening experience with Alloy, so it occurred to me it might be useful to give a simple example of its use here. (This has gotten longer than expected, because some context is needed to understand the problem I had this week and how Alloy helped me solve it. Reader, persevere!)

First, some background.

Alloy is intended for use in what its developers call ‘light-weight formal methods’. It can be used as a sort of desk-checker for software designs. Alloy allows you to describe a design in a simple notation for symbolic logic, define predicates which hold either of particular objects in the universe, or of the universe as a whole, make assertions about the design, and so on. So far, it’s a lot like the specification language Z, only it doesn’t use Greek symbols and it’s much less intimidating to programmers who turn off when things look too formal or mathy. But one nice feature of Alloy not shared by Z is that Alloy can be used to find instances of predicates you define, or counter-examples to assertions you make. It doesn’t actually prove your assertions true, but it does an exhaustive check on all possible instances of the model you’ve defined, up to a user-specified size, and if it finds a counter-example, it will show it to you.

So if there is a problem in your design which can be illustrated by an example small enough to fit into the scope you specify, Alloy will find it.

Not all bugs have small test cases that exercise them. But a whole lot of them do. And Alloy’s clever exploitation of current SAT-solver technology means you can find those bugs really easily.

Now, my former W3C colleague Dan Connolly pointed out to me a long, long time ago that one can use specification languages like Alloy not just to check software designs, but to test our understanding of things we read. Dan told me once that when he really wanted to understand something, he tried to model it using a specification language and prove at least a few trivial theorems about it. As an example, he showed me a formalization he had done of part of paper by Murata Makoto, using Larch (and in particular the Larch Prover LP) for this purpose; nowadays I think he uses ACL2 for this kind of thing. (I like LP and ACL2, too, but I find them hard to use, which means I don’t use them very often. And I’m not sure how many theorems Dan proves in a year using these techniques.)

The other day, Claus Huitfeldt and I were discussing Nelson Goodman’s account of properties in his book The structure of appearance. Some properties, Goodman points out, have the property that if they are true of a thing, they are true of every part of that thing. (The property “is located in Indiana” is an example.) Other properties have other (second-order) properties; Goodman identifies several properties of properties that he finds useful. Claus and I worked through the definitions of dissective, expansive, collective, and nucleative properties, translating them into symbols and trying to think of examples, and we were just starting on the properties of two-place predicates when I thought it might be useful to check some of our conjectures by formalizing things a little more fully.

This involved backing up a bit, because in defining the terms dissective, expansive, etc., Goodman appeals to notions like “is part of”, “is the sum of”, and “is the product of”. These, in turn, are secondary concepts defined in terms of a single primitive, “overlaps”. (This alone would probably have sufficed to hook Claus and me.) So we set out to describe, in Alloy, the notion of overlap in Goodman’s calculus of individuals.

My first cut was simple. An individual is anything a particular system wants to treat as an individual; OO programmers would call it “object” not “individual”, but Goodman antedates OO programming. Overlap is a relation among individuals, and relations among things are specified in Alloy by naming them in the description of the first member of the ordered pairs. So I wrote

sig Individual {
overlaps : set Individual
}

This defines a signature or set of objects, named Individual. Each individual has a field (or property) named overlaps, the value of which is a set of individuals. Another equivalent way to describe it is to say that there is a relation overlaps the members of which are ordered pairs of individuals.

Looking at instances of this model (using the Alloy Analyzer, you add the instruction run {} and ask that it be executed) showed that this formulation had an intuitive drawback: For two individuals a and b, a could overlap b without b overlapping a. That didn’t seem right, so I added a constraint: if b is in the overlaps set of a, then a is in the overlap set of b. (The “@” sign is a syntactic artifact; don’t worry about it.)

sig Individual {
overlaps: set Individual
}{
all i : Individual | i in overlaps iff this in i.@overlaps
}

The second pair of braces contains a set of constraints (in this case, just one) that hold of every member of the signature. This constraint has the desired effect of guaranteeing that if a.overlaps contains b, then b.overlaps contains a.

To avoid having to say awkward things like b in a.overlaps, we can define a predicate that allows us to say simply overlap[a,b]. (For technical reasons, predicate arguments in Alloy 4 are enclosed in square brackets, not parentheses. You’ll get used to it.)

pred overlap[x, y : Individual] {
x in y.overlaps or y in x.overlaps
}

[Enrique piped up here, to say “The constraint in the declaration of Individual guarantees that if y in x.overlaps then x in y.overlaps; you can delete either half of the or without losing anything except unnecessary complexity.” I was doubtful, but to shut him up, I wrote

pred overlap2[x, y : Individual] {
x in y.overlaps
}
assert defs_equivalent {
all x, y : Individual | overlap[x,y] iff overlap2[x,y]
}
check defs_equivalent for 5

The Analyzer found no counter-examples to the assertion. This isn’t exactly a proof, but it persuaded me that Enrique was right.]

Now, Goodman takes overlap as a primitive notion, but he provides a sort of formal definition by saying that individuals x and y overlap if and only if there is some individual z, such that anything that overlaps z also overlaps x and y. Intuitively, z can be any individual which is part of both x and y. (You can think of x and y as sets, and of z as any individual in their intersection, but only if you don’t mind hearing howls of outrage from the general direction of Goodman’s grave: in defining the calculus of individuals, he was trying to provide an alternative to set theory for those who like himself preferred to avoid having to assume that sets exist.)

We translated this into Alloy thus:

fact overlap_axiom {
all x, y : Individual |
overlap[x,y] iff
(some z : Individual |
(all w : Individual |
overlap[w,z] => (overlap[w,x] and overlap[w,y])))
}

Now, it seems clear from our intuitive understanding of the nature of overlap that in a plausible formalization the overlap predicate has to be both symmetric (overlap[a,b] iff overlap[b,a]) and reflexive (everything overlaps itself).

We added appropriate assertions to the model and checked them. It seemed clear that the symmetry must follow from what we had said so far, and I was not surprised to see that it did: in every universe with ten Individuals or fewer, the symmetry of the overlap relation holds. It seemed equally clear that based on our model so far, overlap would not (yet) be reflexive, and we would need to make it so by adding another fact asserting the reflexivity of overlap as an axiom.

So I admit I was surprised when Alloy found no examples of the model which violated the assertion that overlap is reflexive.

I have spent several odd hours, over the last couple of days, trying to understand this result. I assumed it was a typo on my part, some error in my definition of overlap_axiom. Perhaps the scoping of the operators was wrong? But no, I can never remember operator priorities reliably, so the version I was testing was already fully parenthesized. Perhaps some weirdness of the syntax rules was tripping me up?

Finally, I sat down and wrote out a description of a universe in which all the axioms of the Alloy model held, in which overlap was not reflexive. After two failed attempts, I realized that reflexivity follows necessarily from Goodman’s characterization of overlap (i.e. from overlap_axiom). (Hint: in a universe with only one individual a, bind x, y, and z to a and try to make overlap[a,a] false. You won’t. Q.E.D.)

Goodman’s axiom guarantees the symmetry of overlap, too. So we can lose the constraint in the definition of the Individual signature.

What I like about this experience is not so much having spent two hours or so looking fruitlessly for a syntax error in my formulation of overlap_axiom; that I could have done without. What I really like is that formalizing Goodman’s concept of overlap in Alloy surprised me by exposing a bug in my understanding. I was convinced that the reflexivity of overlap, as Goodman described it, was a hidden premise smuggled in from our extra-logical understanding of the English word “overlap”. At the cost of about ten minutes’s work with Alloy, I discovered that my conviction was misplaced. It did take me several more hours of thought, over a couple of days, to understand why reflexivity follows from Goodman’s characterization, but that really illustrates a shortcoming in my central nervous system, not one in Alloy.

Any tool that can so effortlessly expose misconceptions about fundamental concepts and thus help clarify our thinking about a design or a theory is a tremendous aid. Why isn’t every Working Group in the W3C and every other standards-development organization working in information technology writing Alloy models to check their understanding of their designs?

Finally, some links: If I have succeeded in making Alloy sound worth looking at, you’ll want to know that Alloy was developed by the Software Design Group at MIT’s Computer Science and Artificial Intelligence Laborary (CSAIL) under the leadership of Daniel Jackson. The Alloy site has tutorials and other ancillary information, as well as the current downloadable version of the Alloy Analyzer.