Enrique and the printer

[18 February 2009]

Enrique isn’t speaking to me just now.

He phoned this morning, fuming. “I installed some new OS update the other day, and now my printer won’t print.” “I’m sorry to hear that,” I said. I was, too: when Enrique’s printer doesn’t work, he always wants to use mine. “Did you try to fix the problem?” “Well, I went to the Web and found some advice to try deleting the printer and re-adding it. So I deleted it. And now the [expletive deleted] machine can’t see the printer at all!” “Ouch,” I said, wondering whether the toner we have on hand would get us through the week, if Enrique descended on us with hundreds of pages to print. “So I ran Software Update again, and it took forty-five minutes to download yet another security update for the OS. And it still couldn’t find the printer. So then I went to the Apple site and downloaded the packet of HP printer drivers … and it’s still not finding the driver.“

“Is the USB cable seated securely?” “What kind of amateur do you take me for? Of course. I checked, it’s secure both at the machine end and at the printer end.“

“Did you unplug and replug the power cord, too?”

There was a brief pause, before the call was cut off. Like I say, he’s not talking to me today. I’ll try to use the quiet time to get some other work done.

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

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

Such a little thing, to provoke so many thoughts

[3 February 2009]

I saw an interesting bit of stray XML this morning, which raises a number of questions worth mulling over.

The New York Times sends me email every morning with headlines from the day’s papers; this is one of the perqs, I think, of being a subscriber. Given the choice, I asked for the ASCII-only version (like many people I know, I don’t much like HTML email; I’m not sure this is a well-founded prejudice, but there it is).

In today’s headlines, I find the following fragment:


"Oh, you're one of <em style="i">them."
- IRIS CHAU, recounting an acquaintance's reaction when she said she
worked at a banking company.

My eye was caught (perhaps this is just a deformation professionelle) by the unmatched start-tag for an ’em’ element, appearing in what was intended to be a markup-free context. This seems to tell us several things about the internal system used by the Times, and to invite several questions:

  • They seem to be using markup (perhaps HTML, perhaps some other XML vocabulary), not just for delivery of the headlines but in the system for preparing features like the quotation of the day.
  • Their XML vocabulary seems to require an inline specification of rendering information. This seems odd; wouldn’t it be natural for a stylesheet to say that ’em’ elements should be italic? How many other renderings of emphasis are there likely to be in the main story block, in a broadsheet? (Oh, well; not my design, and I don’t know what constraints the vocabulary designer was working under.)
  • Assuming that this quotation was cut and pasted out of the story in which it appears (which does not appear to be ill-formed), could we infer that the journalist who did the cut and paste could was using an editing tool that had no markup awareness? Would a tool with better awareness of markup have helped here? (E.g. by picking up the end-tag of the ’em’ element, as soon as it picks up the start-tag, as SoftQuad’s Author/Editor used to do [and presumably still does in its current incarnation], or by dropping the start-tag.)
  • Could a better validator somewhere in the system that generates the ASCII headlines have caught this error? Could it have been fixed automatically, or with minimal-cost human intervention?
  • What properties would a validator for that process need to have, to induce people to view it as an asset instead of a nuisance?
  • What properties would a schema language need to have, in order to make it easier to write a validator with those properties? And how might the schema language go about encouraging implementors to write such validators?