Contract checking in Ada

From: Tapio Kelloniemi (spam17_at_thack.org)
Date: 03/30/05 

Date: Wed, 30 Mar 2005 10:46:46 GMT

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

Relevant Pages

  • Re: Contract checking in Ada
    ... > implemenation for Ada. ... > pragma Assert and pragma Debug do not suffice. ...
    (comp.lang.ada)
  • Re: C Interface example
    ... In your later post you note that Ada can work out the length without ... needing it as a parameter here. ... I would probably raise Constraint_Error here (can't use pragma Assert ...
    (comp.lang.ada)
  • Ada pragma assert in Java
    ... Can anyone tell me in brief whether Java has a function like a pragma Assert ... in Ada? ... TIA ...
    (comp.lang.java.help)
  • Re: Printing out an Array
    ... > this code to convert bytes to bits but I dont know what to put in the ... in the package Ada.Text_IO (ARM A.10.1) ... you will find the generic packages Integer_IO and Modular_IO (described ... in Ada it is not necessary to convert the value to an array of bits ...
    (comp.lang.ada)
  • Re: ADA Popularity Discussion Request
    ... ARM 3.9reads: ... identifies the specific tagged type used to create the object originally. ... The tag of an operand of a class-wide tagged type TąClass controls which ... Dynamic type creation in Ada: ...
    (comp.lang.ada)