Daniel Jackson's new book has arrived!

This afternoon I got home from work to find a letter from Waterstone's saying that my copy of Software Abstractions had arrived.  I put my shopping bags down on the kitchen table and went straight back out again and caught the bus back into town to pick it up.  Zoe had to to spend an extra 45 minutes at after-school club as a consequence. 

I have high hopes for this book, and will talk about it more when I have had a chance to go through it.  Of all the specification methods that I have come across, Daniel Jackson's Alloy is the most similar to my own ideas.  I like its simplicity and cleaness.  I now want to find out how practical and scalable it is.

The OS Titanic?

According to Paul Thurrot, Microsoft seem to be having some difficulties with Windows Vista, their intended successor to the Windows XP operating system.   My feeling is that it is, as C.A.R.Hoare said of the programming language Ada, "doomed to succeed".

Daniel Jackson's New Book

Daniel Jackson, creator of the Alloy specification language has a new book out.  It is called Software Abstractions - Logic, Language, and Analysis.  It apparently is already available in the USA and is to be published in the UK at the end of this month.  I popped into Waterstone's this evening and ordered my copy.   More details, including sample chapters are available from the book's web-page at MIT Press.

From the sample preface, I like Jackson's description of his experiences using an automatic specification analyzer:

The experience of exploring a software model with an automatic analyzer is at once thrilling and humiliating. Most modelers have had the benefit of review by colleagues; it’s a sure way to find flaws and catch omissions. Few modelers, however, have had the experience of subjecting their models to continual, automatic review. Building a model incrementally with an analyzer, simulating and checking as you go along, is a very different experience from using pencil and paper alone. The first reaction tends to be amazement: modeling is much more fun when you get instant, visual feedback. When you simulate a partial model, you see examples immediately that suggest new constraints to be added.

Then the sense of humiliation sets in, as you discover that there’s almost nothing you can do right. What you write down doesn’t mean exactly what you think it means. And when it does, it doesn’t have the consequences you expected. Automatic analysis tools are far more ruthless than human reviewers. I now cringe at the thought of all the models I wrote (and even published) that were never analyzed, as I know how error-ridden they must be. Slowly but surely the tool teaches you to make fewer and fewer errors. Your sense of confidence in your modeling ability (and in your models!) grows.

And from the sample introduction there is:

When good abstractions are missing from the design, or erode as the system evolves, the resulting program grows barnacles of complexity. The user is then forced to master a mass of spurious details, to develop workarounds, and to accept frequent, inexplicable failures.

From now on I won't be able to start up Microsoft Word without the vision of a foundering barnacle-encrusted ship coming into my mind!

Update on Sat 2006-05-13 by Tristram Brelstaff

Apparently the UK publication date has been put back to May 28th.

The +CAL Algorithm Language

Leslie Lamport has extended his TLA+ Tools with +CAL, a language to specify algorithms in.  As he explains:

+CAL (pronounced "plus-CAL") is an algorithm language based on TLA+.  A +CAL algorithm is translated to a TLA+ specification, which can be checked with the TLC model checker.

An algorithm language is for writing algorithms, just as a programming language is for writing programs.  The introduction to the +CAL manual (see below) explains how algorithms differ from programs, and how +CAL differs from programming languages. 

+CAL comes with two syntaxes, one Pascal-like and the other Java-like.  This looks like a cynical attempt to attract the curly-brace rabble (but I reckon most of them would probably fail to appreciate Lamport's distinction  between an algorithm and a program).

Michael Jackson's Papers

I have a lot of time for the software development guru Michael Jackson: he has thought deeply about important problems, and has come up with original, interesting and practical ways of solving them.  Recently, he has revamped his publications page to include on-line copies of many more of his papers.  This now provides lots of good reading on the subjects of Problem Frames, Requirements and Specification, as well as his earlier work which lead to JSP and JSD.

(If there was a competition for the coolest title for a computing science paper then Zave and Jackson's Four Dark Corners of Requirements Engineering would be my nomination.)