Monthly Archives: January 2010

Binary adder in ACL2 and Alloy

Posted on by

[11 January 2010]

Not too long ago, I wrote about cross training in programming languages, and the pleasure of rewriting things from one language into another.

Recently I had another occasion to think about that. I’ve been doing some work lately with two systems which I think of as similar, though they have different goals and emphases. ACL2 (‘a computational logic for applicative Common Lisp’) is an industrial-strength theorem prover, with a history of use for proofs of correctness for chip designs, programming languages, and mathematical propositions like the fundamental theorem of calculus. It’s a lot like a high-performance car, both in its power and in the fact that it spends a lot of time in the shop. Er, uh, I mean, it requires close, intelligent attention from the user. And its learning curve looks a lot like the approach to Mesa Verde. Alloy, by contrast, is an instance of what its designer calls “light-weight formal methods”; the language is kept simple for analysability’s sake, and no theorem prover is provided: instead, exhaustive searches through all the models of a system up to a given size are made, to find counter-examples to an assertion. It’s got a learning curve, too, but in my experience it’s pretty manageable.

I’m interested in both ACL2 and Alloy because both seem to me to offer help in making designs and specifications correct, and keeping them that way when changes are made. It would be nice to have a better sense of when one tool is more appropriate to a problem, and when the other. One conjecture I’ve entertained: Alloy for initial playing around with a design, ACL2 for fuller proofs of correctness (when real proofs are desired) after the design has settled down a bit. Solving the same problem using both tools seems like an obvious way to test that conjecture and get a sense of how the two compare.

So in a spirit of exploration, I recently took an example from the ACL2 textbook* and experimented with making an Alloy model of the same thing, which I finished the other day and have now published on the Alloy community site. The example covers a binary adder constructed from simple sub-units which add single-bit numbers. (I found it enlightening to read the Wikipedia article on adders; if you’re not an electrical engineer, you may, too.)

* Matt Kaufmann, Panagiotis Manolios, and J Strother Moore, Computer-Aided Reasoning: An Approach ([Austin]: [n.p.], 2002), section 10.5.1.

The experience poses a bit of a challenge to the conjecture just mentioned: although ACL2 does require some help proving that the relevant function terminates and that it’s correct, in some ways the ACL2 description seems simpler than the Alloy description. Certainly it’s more compact. To ensure that models are analysable, Alloy forbids recursive functions; finding an Alloy equivalent to the recursive ACL2 specification of the adder took me some head-scratching, and the result uses a lot of machinery that feels kind of ad hoc to me. But in a way, the fact that a non-recursive formulation can be found also feels like a demonstration of Alloy’s expressive power. (Short version: recursion can be changed to iteration, right? So think about using sequences.)

A really good comparative sense of the two systems will require a lot more than one exercise of this kind; ideally, I’d like a whole series of ACL2-to-Alloy and Alloy-to-ACL2 translations. Currently, my Alloy seems to be up to translating at least some ACL2 exercises into Alloy; I am not certain my ACL2 skills are up to finding ACL2 equivalents for standard Alloy exercises. If you are interested in formal methods (and who else will still be reading at this point?), all I can say is: stay tuned. And if you do any cross-translation exercises of this kind, think about sharing them!

Bare-bones TEI

Posted on by

[6 January 2010]

The markup vocabulary defined by the Text Encoding Initiative is, for good and sound reasons, rather large and in some ways rather complicated. From time to time, however, it’s useful to have a radically cut-down version of the TEI vocabulary. For people just learning TEI markup (to name just one instance), a cut-down version can simplify initial training and make the TEI feel a little less intimidating.

Many people use TEI Lite, which is much smaller than full TEI. But for some work I’m doing with Yves Marcoux and Claus Huitfeldt, we felt it would be handy to have an even smaller subset of TEI to work with. Years ago (1994), I defined a profile of TEI called ‘Bare Bones TEI’, intended not so much for serious use as for training and for thought experiments.

I had long regarded the full details of bare-bones TEI as lost to history: the documentation has been preserved by Robin Cover at the XML Cover Pages, but it didn’t include the DTD modification file showing the precise changes from the then-current TEI DTD. I had tried a few times, searching both the Web and my hard disk, to find the original data, but had had no luck. But the other day, for reasons I don’t think I can explain, an attempt at one more search eventually found an old copy of the documentation, the modification files, and the full DTD for bare-bones TEI.

I’ve now translated the original documentation to XML, added updated links to the various DTD files, and added parameter entities to the DTD to make it work both for SGML contexts and for XML. The documentation for Bare bones TEI is now available on this site, as is the modified DTD.

The current version of the bare-bones DTD is based on TEI P3, and the translation to XML loses a small amount of information involving the pb (page break) element. Eventually, perhaps, I’ll apply the bare-bones customization to TEI P5 and produce an updated version of the schema and documentation.

Note: in searching for Bare-bones TEI on the TEI Consortium site just now, I discovered that someone has produced a similar profile, called ‘Bare TEI’. [Further research shows that although the page on customizations does not identify the authors, the work was done originally by Laurent Romary and later edited by Syd Bauman, Lou Burnard, and possibly also Sebastian Rahtz.] This may be worth exploring, for those seeking a minimal profile of TEI. Unfortunately, I haven’t found any usable documentation for Bare TEI, so I don’t know the design principles that govern it, and the DTD is full of undefined ghost elements (or ‘zombies’), which renders it unfortunately cumbersome in a syntax-directed editor. So for now I’m sticking with bare-bones TEI.