Ada's contract stuff is a bit more sophisticated than a simple assertion. You can, for example, do this: procedure increment(v: in out integer) with

Ada's contract stuff is a bit more sophisticated than a simple assertion. You can, for example, do this: procedure increment(v: in out integer) with post => v /= v'old ... (/= is Ada's not-equal-to operator.) This enforces as a postcondition that the value of v must have changed. You can even refer to the old versions of arrays. Plus, the run-time type checking required by more complex type expressions are augmented by compile-time checking. If the compiler can deduce that a conversion will always be correct, it won't emit a check. If it can deduce that it will always be wrong, it'll error out at compile time. It all works really rather well. The only trouble I have with preconditions and postconditions is that you have to declare them in your module's interface, which is public, rather than in the module's implementation, which isn't. So you can only test your module's public interface. If your module doesn't expose a state variable to the outside world, you can't use it in a precondition or postcondition. I find that a very odd design decision.