Thursday, March 18, 2010

How to test post-conditions

A pretty good student, Joshua Muheim, just asked me what the simplest way was to check postconditions. And my answer was the following:

Joshua, this is a research question! To the best of my knowledge, currently and in practice, developers use steamroller tactics to check postconditions. The standard way to verify that the LHC works as intended, in a method exterminate on a class EarthPopulation:
exterminate
| oldSize |
oldSize := self size.
LHC switchOn.
self size should < oldSize.

That is, you copy whatever you intend to change and then compare new with old value. It isn’t difficult to imagine that this can lead to trouble if whatever you want to change isn’t cloneable. And of course it isn't possible to switch off the overhead of these assertions.* And that’s where Histoory (by Pluquet et al) comes to the rescue. Not only does it work independent of the cloneability, it also provides a much cleaner syntax:
exterminate
[LHC swithOn]
postCond: [:old | old size should < self size]

Alas, it isn’t in the latest flavor of any programming language, so I truly hope that Histoory will make it into Pharo :).

* I added this sentence after Joshua's correct observation of this problem.

6 comments:

  1. But what about the overhead of creating these oldSize etc. variables? They should only be created when assertions are turned on, right? So in your version, they are always created.

    I guess in Ruby (or any other "cool" programming language) you could do such things using blocks or something...

    assert_postcondition(:old => size, :expected => size + 1) do
    size += 1
    end

    Oh, right, I forgot how really bothersome java is... What a pitty it's still the programming language #1 that's taught at the universities...

    Sincerely yours, the pretty good student ;-)

    ReplyDelete
  2. Hi, that's a correct observation. Of course, the Histoory code is in one of these cool languages, and there it's perfectly possible to switch off postconditions.

    And about Java: I won't comment on my preferences in the scope of the class, but this being my own blog … Java is really missing some advances in programming languages that can be missed only too easily.

    ReplyDelete
  3. There is a programming language, which implements pre- and postconditions very well: Eiffel.

    In Eiffel it's very easy to check pre- and postconditions. But even in this case, a certain additional overhead remains.

    Cheers Pat

    ReplyDelete
  4. Hi Pat,

    I receive a lot of pointers to Eiffel. I think the day where I just won't be able to avoid studying it has finally arrived …

    ReplyDelete
  5. I'm always complaining about still using Java as the first language that students learn. In my opinion, it just doesn't fit for this purpose - it's too tedious, too unintuitive, too heavy... It's just no fun to work with it - or to learn programming with it.

    ReplyDelete

Note: Only a member of this blog may post a comment.