In my last post (which was, alas, a stupidly long time ago!), I talked a bit about software specification, and promised to talk about my favorite dedicated specification tool, Alloy. Alloy is a very cool system, designed at MIT by Daniel Jackson and his students.
Alloy is a language for specification, along with an environment which allows you to test your specifications. In a lot of ways, it looks like a programming language – but it’s not. You can’t write programs in Alloy. What you can do is write concise, clear, and specific descriptions of how something else works.
I’m not going to try to really teach you Alloy. All that I’m going to do is give you a quick walk-though, to try to show you why it’s worth the trouble of learning. If you want to learn it, the Alloy group’s website has a really good the official Alloy tutorial. which you should walk through.
Since I have some free time, I’ve been catching up on some of the stuff
I’ve been meaning to read. I’ve got a reading list of stuff that I’ve wanted
to look at that were written by other authors with my publisher. Yesterday, I started looking at Cucumber, which is an interesting behavior-driven development tool. This post isn’t really about Cucumber, but about something that Cucumber reminded me of.
When a competent programmer builds software, they write tests. That’s just
a given. But why do we do it? It seems like the answer is obvious: to make sure that our software works. But I’d argue that there’s another reason, which in the long run is as important as the functional one. It’s to describe what the software does. A well-written test doesn’t just make sure that the software does the right thing – it tells other programmers what the code is supposed to do.
A test is an executable specification. Specifications are a really good thing; executable specifications are even better.