In the book Surely You’re Joking, My Feynmn!, Richard Feynman tells an amusing story of engineers showing him complicated blueprints and him pointing to them and asking “what happens if this valve sticks?”

The engineers were astonished. They pored over their blueprints and realized that they had a design flaw. What’s amusing about the story is that Mr. Feynman was bluffing. He didn’t know if he was pointing to a valve or not and assumed the engineers would gently correct his misunderstanding. By mere chance, a serious problem was averted.

In yet another anecdote I read, a contractor finished building a hospital but its opening was delayed because somehow nobody realized that they had forgotten to have phones in the building. Oops.

Today, these sorts of problems are less likely to occur because engineers, architects and others have sophisticated software tools which can alert them to potential problems. But what about “software engineers”?

An article in the latest issue of Scientific American entitled Dependable Software By Design explores this issue in some detail, but rather than just lament on the poor state of software development, this article details relatively recent software innovations that can allow software designers to truly earn the title “engineer”.

The article mentions several software packages which can help detect design flaws, but it focuses specifically on a free software package named Alloy. Alloy provides a declarative programming language (think “Prolog”) which allows the software designer to describe their software model, what it does, what it shouldn’t do, and Alloy attempts to find “counter-examples” which illustrate flaws in the software design (not in the software itself — that’s what tests are for).

The basic steps are fairly simple:

  • Define your objects
  • Model the operations
  • Specify requirements
  • Find and fix flaws

As an example of Alloy code, here are the basic object definitions they listed for testing directory moving code:

module filesystem

abstract sig Object []
sig File, Dir extends Object []

sig FS {
    dirs: set Dir,
    files: set File,
    contains: dirs -> (dirs + files)
    }

(Note that in the above, “set” refers to a set of objects, not setting a value)

The above notation is fairly simple and easy to read. In the examples provided in the article, they test moving a directory from one directory to another. The model states that after a move, the directory must not be in the old directory, it must be in the new directory, and nothing else must change. Further, there is a constraint that after the move, all directories must be reachable from the root directory.

Seems pretty simple, right? How could someone screw up code like that? Well, when Alloy is run, it finds a counter-example: a directory which is moved to itself. When that happens, the directory winds up being unreachable from root, therefore there’s a software flaw. Variants of this flaw are very common. A friend told me just yesterday that if she creates a folder named “Desktop” on her Windows Desktop, her version of Windows gets confused.

Software modeling is an important tool and many attempts at solving this problem in the past have produced cumbersome software products which are difficult to use. Some attempt to turn specifications directly into the software (which doesn’t do much good when the specification is flawed) and others attempt to analyze all possible paths through the software (which scales terribly). Alloy is content to merely look for counter-examples which demonstrate design flaws.

The Alloy Web site looks interesting. You can download the software for free for Mac OS X, Windows (requires Cygwin), Linux and NetBSD. The site has a quickstart, an online tutorial, a reference guide, numerous links to papers and a FAQ. Can Alloy and similar tools be the turning point in software design? I think it’s a great step in the right direction.