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!
Apparently the UK publication date has been put back to May 28th.