Tag Archives: Alloy

Alloy as logical desk calculator

Posted on by

[26 March 2010]

Long ago I used a wonderful file-oriented database system called Watfile, which was designed as a sort of desk-calculator for data. It was designed for personal use, not industrial-strength data management, and its designers successfully resisted the temptation to add more features and more power at the cost of a more complex user interface. Watfile was to a full enterprise-class database as a desk calculator of the 1960s was to … oh, perhaps to Fortran. For suitable problems, the ease of setup far outweighed any considerations of power or completeness.

The experience of using Watfile for data manipulation tasks established in my mind the class of ‘desk-calculator-like’ packages for various kinds of problem.

Today I experimented with Alloy as a sort of logical desk calculator, and I’m happy to report that it passed the test with flying colors.

For reasons I won’t go into here, I’ve wondered a bit recently what it might look like to apply the technique of distinctive-feature analysis (originally developed for phonological descriptions of sound systems of language) to writing systems. When I sat down a few months ago with pencil and paper to see if I could devise a smallish set of typographic features which could (say) distinguish the twenty-six letters of the alphabet as I was taught it in first grade, I rapidly found that working solely with pen and paper made me impatient: it was too tedious to look at the set of features already identified and see which letters could not yet be distinguished (because they had the same value for all the features in question).

When I came back to this problem this afternoon, I thought for a few minutes about what questions I’d like to be able to ask the machine. Given a specified set of graphemes (as a first exercise, I chose the lower-case alphabet) and a specified set of binary features (does the letter have an ascender? a descender? a vertical stroke? a full or partial circle or bowl? Is the stroke to the left of the bowl? …), with information about which graphemes have the feature in question, I want to be able to ask, first, whether a particular set of features suffices to distinguish each individual grapheme? Or are there two or more graphemes which have the same value for all features in the set? And of course, if there are such sets of indistinct graphemes, what are they?

It occurred to me to solve the problem in Prolog; it would take just a relatively simple set of Prolog predicates to do what I wanted. But as I was preparing to launch X Windows, so that I could launch Prolog, I realized that I already had the Alloy Analyzer running. And so I wrote the predicates I wanted in Alloy instead of Prolog, to see whether it would work.

The upshot is: yes, it worked, and it was probably a bit easier to do than it would have been in Prolog. When I was thinking about how to set up the problem in Prolog, I found myself wondering about the best data representation to choose, and so on, almost as much as about the structure of the problem. I won’t say that Alloy posed no analogous problems — I did have to think for a moment or two about the best way to describe graphemes and distinctive features. But the high level of abstraction afforded by Alloy made the decision feel less binding, and made me feel a bit more comfortable experimenting. (It sounds strange to put it this way: after all, Prolog’s high level of abstraction is one of its great design strengths. But Prolog is also designed to be an efficient and effective programming language, which means that some details are exposed which have only procedural significance, and sometimes you find yourself thinking about them, even in situations where questions of execution efficiency don’t arise.

In very short order, I found it possible to define a suitably abstract representation of graphemes and features, specify some useful functions and predicates for asking the questions described above, and specify a small set of features (ten) which have a certain degree of typographic plausibility and which suffice to distinguish the graphemes in question. (Ten binary features for twenty-six graphemes may seem high, given that the theoretical minimum is only five, and that ten bits suffice to distinguish a thousand objects, not just twenty-six. But writing, like natural language, has some redundancy. Feature sets used to analyse natural language sound systems are also often very inefficient.) The visualization tools did not prove very helpful, but the Evaluator feature of the Alloy Analyzer was a great help.

If I pursue this work any further, I probably will put it into Prolog, where the interactive interface for expression evaluation is perhaps a bit more convenient than in Alloy. But it’s nice to know that Alloy can be used for this kind of problem, too.

Interested readers can find both the generic definitions and the specific graphemes and features for lower-case Latin letters (as used in Anglophone countries) on the Black Mesa Technologies web site.

How formal can you get?

Posted on by

[26 January 2010; updated a URI 28 Jan 2010]

In a recent comment on an earlier post here, David Carlisle wrote of proofs concerning properties of the XPath 1.0 data model

It’s not clear how formal any such proof could be, given that the XPath model and even more so, XML itself are defined so informally.

It’s true that the XPath spec defines the data model in prose and not in formulas. But on the whole it’s relatively formal and explicit prose, and I would expect it to be relatively easy to translate the prose into a formal notation.

As a test of that proposition, I recently improved a shining hour or four by translating section 5 of the XPath 1.0 spec into Alloy, the modeling tool developed by Daniel Jackson and others in the MIT Software Design Group. (I would describe Alloy briefly here, but I’ve written about Alloy often enough in this blog that I won’t describe it again now; regular readers of this blog will already know about it, and those who don’t can search the Web for information, or search this blog for what I’ve said about it before.)

The full Alloy model of XPath 1.0 is available from the Black Mesa Technologies web site. It will be of most interest, of course, for those familiar with Alloy, or wanting to learn more about it. But Alloy’s formalism is simple enough that anyone with a taste for formal methods will find it easy going, and the document paraphrases all the important things in English prose.

The net result, I think, is that there are (unsurprisingly) some places where the definition of the XPath 1.0 data model could or should be more explicit, and a few places where it seems a rule or two given explicitly is strictly speaking redundant, but by and large the definition is pretty clean and seems to mean what its creators meant it to mean. By and large, the definition of the data model is formulated without reliance on the XML spec (there are a few places where this separation could be cleaner), so that the informality of the XML spec (or what I prefer to think of as its programmatic promiscuity regarding models) does not in fact make it hard to formalize the XPath 1.0 data model.

In the current version, there are a couple of rough bits that I hope to sand down before I use this model in any other contexts. The ones I’m currently aware of are these:

  • The definition of the parent relation does not require that whenever parent(c,p) is true, either child(p,c) or attribute(p,c) is true. The XPath 1.0 spec doesn’t say this explicitly, but I think its authors probably felt that it would be pedantic to say something like that for a relation with a name like parent.
  • Similarly, the relations parent and ch are not guaranteed acyclic, though I think the original spec assumes that the names parent and child make clear that the relations should be acyclic. (But see the song “I’m my own Grandpa” and the Alloy models illustrating it, developed in Daniel Jackson’s Software Abstractions and shipped with Alloy in the samples directory.)
  • The predicate precedes intended to model document order is defined recursively; this is not legal in Alloy. So a conventional relation on nodes will need to be defined instead, with appropriate constraints. It is still not clear whether the rules given in the spec suffice to make the order total (at least in the absence of multiply occurring children); if they don’t, I’d like to propose an additional predicate which has that effect.

One reason I love Alloy (Goodman, calculus of individuals)

Posted on by

[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.