Contract checking in Ada

[Tapio Kelloniemi <spam17@thack.org>]

Hi all

Ada has very powerful run-time checking system which allows for safe
programming and efficient execution, depending on the user's needs. As
I look at the ARM and GNAT Runtime Library sources, I have noticed
that this does not unfortunately apply to Ada's standard library. Many
subprograms check that its parameters are valid. I'm not saying that
parameter validity checking is bad, becuase it is very useful, but the
user should be able to disable it, when (s)he is certain, that the
conditions will not fail. I'm quite surprised that Ada2005 does not
replace library functions' parameter checks with pragma Assert, in
which
case user could disable checking. In GNAT library, for example, many
checks
are done twice (or even more times), because the library has its own
checks
and the language has its own.

I'm interested in design by contract and would like to have an
implemenation for Ada (like Eiffel's as much as possible). However,
pragma Assert and pragma Debug do not suffice. I would like to have
pre- and postconditions and type invariants. However I have no idea of
how to implement them, except by writing an external tool which would
preprocess Ada sources. I don't want to do that. If anyone has any
advice (except waiting for Ada2015), please tell me.

-- 
Tapio