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

NaN Nonsense

Gary Leavens has a paper in the current issue of the Journal of Object Technology in which he describes the problems caused by NaN (Not-a-Number) values in the specification of software involving IEEE 754 floating point computations.  It never ceases to dismay me how ready some people are to use single (defined) values to represent undefined values.  They then get themselves tied up in knots over such questions as whether one NaN should be equal to another NaN, or whether NaN should be a number or not.  If you think I am just joking about the latter then read the following quotation from Leaven's paper:

The tricotomy law says that either x < y, x = y, or x > y; but if either x or y is NaN, then all three of these expressions may be false. Violation of tricotomy tells us that, with NaN, floating-point numbers are no longer totally ordered.  Of course, this makes sense if you consider NaN to be “not a number” as only the numbers are totally ordered.  The trouble is that type systems usually consider NaN to be a number.

Type systems consider 'Not-a-Number' to be a number!  And people don't even seem to wonder why they run into difficulties with this approach.  This is precisely the sort of silliness that I was complaining about in my Undefined Values should remain Undefined.

I agree with Leavens that the best solution to the NaN problems is to dispense with them altogether and to throw an exception on the failure of the precondition for a floating point operation.  This would be the 'Design by Contract' approach.

State the Problem Before Describing the Solution

Today I came across the following short note on Leslie Lamport's site:

State the Problem Before Describing the Solution, Leslie. Lamport, ACM SIGSOFT Software Engineering Notes 3, 1 (January 1978) 26

The idea is that, when writing a paper, you should precisely state the correctness requirements for any solution before you present your proposed solution.  Lamport points out that this idea can also be used when writing programs.  The separation of the requirements from the solution is similar to Michael Jackson's insistence that requirements be written in terms of domain concepts rather than solution concepts.