Invariants and Design by Contract

I've just been doing a little reviewing of languages that support DBC programming, such as Eiffel. DBC programming allows you to structure your debugging code without littering it with assert()s. With a few macros I think it would be possible to achieve this in Dylan, while not mutilating the syntax as you would have to in C++. Also, the contracts could be moved out of the methods and act more like aspects in Aspect Oriented Programming.

// Define counter instance methods

define invariant-method increment (counter :: <counter>)
  counter.value := counter.value + 1;
end;

define invariant-method decrement (counter :: <counter>)
  counter.value := counter.value - 1;
end;

// Define method and class invariants

define invariant increment (counter :: <counter>, old)
  counter.value == old.value + 1;
end;

define invariant increment (counter :: <counter>, old)
  counter.value == old.value - 1;
end;

define class invariant (counter :: <counter>)
  counter.value >= 0;
end;

The implementation would look something like this:

define method increment (counter :: <counter>)
  let old = counter.shallow-copy;
  counter.value := counter.value + 1;
  increment-invariant (counter, old);
  class-invariant (counter, old);
end;