Log in



In my classes here we talk a lot about formal specifications of programs and using the specifications to prove the correctness of implementations. It is a very interesting idea, that has unfortunately not been able to be applied much in practice because of the shear complexity involved in trying to prove things about programs.

I have been for a long time now very interested in TDD and testing of software. One of the things about TDD (Test-Driven Development) is that you are not supposed to be thinking of the practice of TDD as testing. Even though that is in the name, and everything uses the nomenclature of testing it is not about testing.

It is about design.

Formal specifications are about design as well.

The more I've seen these things the more that I have noticed that they are trying to do almost the same thing. The TDD crowd took the very pragmatic approach of using what we can do (write snippets of specifications as code to check some other code) and applying it. The formal methods crowd took the route of purity by taking pure math and using that to describe the systems.

Both sides have downsides. In TDD you can't really prove your program correct. The best you are getting is that in the cases you chose you have shown that it works. Formal specifications can prove your program correct, so long as it is fairly small and simple. Anything larger and you will just get completely overwhelmed.

Recently the test focused nature of TDD has been called into question. From the beginning most masters (I don't think they would want to be called that) in it have said that you are driving your design, not testing your code. Most people encounter problems with this (I think) because the terminology does not match up with what you are trying to do. A Test Case is a Specification? Not in most people's minds.

Out of this has grown some movement to change the terminology to save TDD from itself. One project that I have found interesting is rSpec for Ruby. A wonderful article that explains this a lot better than I can is Dave Astels. I found it so interesting that I decided to see how well I could get something like this into perl. I've always loved perl's testing facilities, but they have never quite given me the right framework to really express that my .t files are really my specification.

So I just hacked together (no way this could be used for a project yet, but I'll probably start using it on my projects and growing it that way) something that looks like rSpec for perl. I'm calling it pSpec for now, but might change that. Since I haven't actually used rSpec or jBehave yet, I don't know if I have large gaps in what I'm doing, but it is an interesting experiment so far.

What does it look like?

use pSpec;

context "x variable", is {
    my $x;

    setup {
        $x = 2;

    specify "should be 2", as {
        should_be $x, 2;

I won't bother anyone with the implementation for now :)



December 2007

Powered by LiveJournal.com