Contract checking in Ada

Contract checking in Ada

[Tapio Kelloniemi]

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

Re: Contract checking in Ada

[Vinzent 'Gadget' Hoefler]

Tapio Kelloniemi wrote:

> 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.

Sounds a little bit like SPARK (<URI:http://www.sparkada.com>),
especially if you want to get rid of the checks at run time.

AFAIK even in Eiffel the contract is checked at run time, not compile
time.


Vinzent.

-- 
worst case: The wrong assumption there actually is one.

Re: Contract checking in Ada

[Georg Bauhaus]

Tapio Kelloniemi wrote:
 
> I'm interested in design by contract and would like to have an
> implemenation for Ada (like Eiffel's as much as possible).

http://www.ada-auth.org/cgi-bin/cvsweb.cgi/AIs/AI-00375.TXT


Georg 

Re: Contract checking in Ada

[Martin Dowie]

Georg Bauhaus wrote:
> Tapio Kelloniemi wrote:
>
>> I'm interested in design by contract and would like to have an
>> implemenation for Ada (like Eiffel's as much as possible).
>
> http://www.ada-auth.org/cgi-bin/cvsweb.cgi/AIs/AI-00375.TXT


!status No Action

Re: Contract checking in Ada

[Tapio Kelloniemi]

Georg Bauhaus <bauhaus@futureapps.de> wrote:
>Tapio Kelloniemi wrote:
>
>> I'm interested in design by contract and would like to have an
>> implemenation for Ada (like Eiffel's as much as possible).
>
>http://www.ada-auth.org/cgi-bin/cvsweb.cgi/AIs/AI-00375.TXT

Oh, wow! Good stuff! Few things annoy me:
1. Why this AI does not mention access parameters to procedures and
functions (only [IN] OUT).
2. Which AI describes pre- and postconditions which are mentioned here.

-- 
Tapio

Re: Contract checking in Ada

[Georg Bauhaus]

Tapio Kelloniemi wrote:

>>http://www.ada-auth.org/cgi-bin/cvsweb.cgi/AIs/AI-00375.TXT
> 
> 2. Which AI describes pre- and postconditions which are mentioned here.

Have you tried the search engine available at the above
site?


Georg 

 

Re: Contract checking in Ada

[Randy Brukardt]

"Tapio Kelloniemi" <spam17@thack.org> wrote in message
news:0ux2e.4977$nP.4533@reader1.news.jippii.net...
> Georg Bauhaus <bauhaus@futureapps.de> wrote:
> >Tapio Kelloniemi wrote:
> >
> >> I'm interested in design by contract and would like to have an
> >> implemenation for Ada (like Eiffel's as much as possible).
> >
> >http://www.ada-auth.org/cgi-bin/cvsweb.cgi/AIs/AI-00375.TXT
>
> Oh, wow! Good stuff! Few things annoy me:
> 1. Why this AI does not mention access parameters to procedures and
> functions (only [IN] OUT).

It was never finished; it was abandoned as taking too much work with too
little interest from end-users.

> 2. Which AI describes pre- and postconditions which are mentioned here.

http://www.ada-auth.org/cgi-bin/cvsweb.cgi/AIs/AI-00288.TXT

But really, you should look in the index of Airs or use the search engine.
Look in the home page: http://www.ada-auth.org

                  Randy.

Re: Contract checking in Ada

[Ed Falis]

On Wed, 30 Mar 2005 20:57:06 -0500, Randy Brukardt <randy@rrsoftware.com>  
wrote:

> It was never finished; it was abandoned as taking too much work with too
> little interest from end-users.


Guess I should have stepped up to the plate.  I'm interested, even though  
I work for a compiler vendor.

= Ed

Re: Contract checking in Ada

[Martin Dowie]

Ed Falis wrote:
> On Wed, 30 Mar 2005 20:57:06 -0500, Randy Brukardt 
> <randy@rrsoftware.com>  wrote:
> 
>> It was never finished; it was abandoned as taking too much work with too
>> little interest from end-users.
> 
> 
> 
> Guess I should have stepped up to the plate.  I'm interested, even 
> though  I work for a compiler vendor.

I don't know if Randy is refering to the AdaUK conference that Tucker
spoke at but - as far as I can recall - the vote went against them
there.

Cheers

-- Martin

Re: Contract checking in Ada

[Martin Dowie]

Martin Dowie wrote:
> I don't know if Randy is refering to the AdaUK conference that Tucker
> spoke at but - as far as I can recall - the vote went against them
> there.

Ok, found a like http://www.ada-auth.org/ai-files/grab_bag/adauk200y.zip

Check slide 39. Compared to other proposed features pre/post & invariant
were voted a lower priority by those attending (vast majority being users).

These were the only votes where no one considered them high priority.

I voted for both as 'medium' priority - I didn't buy into the idea that this
would confuse people about SPARK.

Cheers

-- Martin

Re: Contract checking in Ada

[Tapio Kelloniemi]

"Randy Brukardt" <randy@rrsoftware.com> wrote:
>"Tapio Kelloniemi" <spam17@thack.org> wrote in message
>news:0ux2e.4977$nP.4533@reader1.news.jippii.net...
>> Georg Bauhaus <bauhaus@futureapps.de> wrote:
>> >Tapio Kelloniemi wrote:
>> >
>> >> I'm interested in design by contract and would like to have an
>> >> implemenation for Ada (like Eiffel's as much as possible).
>> >
>> >http://www.ada-auth.org/cgi-bin/cvsweb.cgi/AIs/AI-00375.TXT
[--]
>It was never finished; it was abandoned as taking too much work with too
>little interest from end-users.

Ada.Containers (AI-302) has also status of No action, does it mean that
they were also abandoned?

But back to my original question, how could I implement programming by
contract now when the designers have abandoned it in their great wisdom?
SPARKADA seems not to be free software, so it is not an option for me.

>> 2. Which AI describes pre- and postconditions which are mentioned here.
>
>http://www.ada-auth.org/cgi-bin/cvsweb.cgi/AIs/AI-00288.TXT
>
>But really, you should look in the index of Airs or use the search engine.
>Look in the home page: http://www.ada-auth.org

Sorry, I did not remember they had a search engine and it didn't come to my
mind to check.

-- 
Tapio

Re: Contract checking in Ada

[Martin Dowie]

Tapio Kelloniemi wrote:
> Ada.Containers (AI-302) has also status of No action, does it mean that
> they were also abandoned?

Look again:
http://www.ada-auth.org/cgi-bin/cvsweb.cgi/AIs/AI-20302.TXT

It's status is "Amendment 200Y".

There are actually a number of entries in the AI database for the 
Containers - some are just to hold the huge volume of traffic the 
proposal has generated.


> But back to my original question, how could I implement programming by
> contract now when the designers have abandoned it in their great wisdom?
> SPARKADA seems not to be free software, so it is not an option for me.

In short, you can't but at least "pragma Assert" is being standardized.

Cheers

-- Martin

p.s. Just "SPARK" never "SPARKADA" :-)

Re: Contract checking in Ada

[Martin Dowie]

Tapio Kelloniemi wrote:
> But back to my original question, how could I implement programming by
> contract now when the designers have abandoned it in their great wisdom?

And I don't think you're being very fair to the Ada0Y team. The effort 
that has gone into/is going into it is still huge!

It would be great if there were dozens of volunteers to promote new 
proposals but the sad truth is very few people are capable of writing an 
amendment to the RM (and I certainly include myself is the 'not able' 
camp). When people talk about "language lawyers" it isn't far from the 
truth! The knowledge of the language has to be absolutely inside-out if 
you want to be able to amend the actual language - not so much the 
standard library but even that's tricky.

Cheers

-- Martin

Re: Contract checking in Ada

[Randy Brukardt]

"Martin Dowie" <martin.dowie@btopenworld.com> wrote in message
news:d2hcqs$ct0$1@sparta.btinternet.com...
> Tapio Kelloniemi wrote:
> > But back to my original question, how could I implement programming by
> > contract now when the designers have abandoned it in their great wisdom?
>
> And I don't think you're being very fair to the Ada0Y team. The effort
> that has gone into/is going into it is still huge!
>
> It would be great if there were dozens of volunteers to promote new
> proposals but the sad truth is very few people are capable of writing an
> amendment to the RM (and I certainly include myself is the 'not able'
> camp). When people talk about "language lawyers" it isn't far from the
> truth! The knowledge of the language has to be absolutely inside-out if
> you want to be able to amend the actual language - not so much the
> standard library but even that's tricky.

Yes, and they have to be very carefully reviewed, both for language issues
and for implementation ones. (You don't want the new features to cause
programs to run much slower -- the dreaded "distributed overhead"). These
proposals kept getting messier and messier, and that played a part in their
eventually being abandoned.

For instance, Postconditions required a mechanism to get at the original
values of parameters. Which meant that those values had to be saved
somewhere. That would be a huge performance hit unless it is possible to
tell in advance whether or not the original value would be required. We
never had a proposal with that property (it really needs to be visible on a
purely syntax basis; otherwise it can be too complex to figure out, as it
would depend on name resolution and visibility).

We certainly had to prioritize our work, and input like the Ada UK vote that
Martin mentioned was very helpful in doing that. You don't please your
customers by doing the things that they are least interested in! (Note that
input like this was the reason that the containers library got added; it
just seemed too big to undertake, but the consistent message from the user
community was "this is important". So we buckled down and did it - but of
course other things, like the exception hierarchies and the pre/post
condition stuff got dropped to make room.)

                        Randy.

Re: Contract checking in Ada

[Tapio Kelloniemi]

Randy Brukardt <randy@rrsoftware.com> wrote:
>"Martin Dowie" <martin.dowie@btopenworld.com> wrote in message
>news:d2hcqs$ct0$1@sparta.btinternet.com...
>> Tapio Kelloniemi wrote:
>> > But back to my original question, how could I implement programming by
>> > contract now when the designers have abandoned it in their great wisdom?
>>
>> And I don't think you're being very fair to the Ada0Y team. The effort
>> that has gone into/is going into it is still huge!

I did not mean that quite seriously, though I'm sad programming by contract
got rejected. If I did not appreciate the work of AdaXY teams, I would
not be here asking questions and wasting your time.

>> It would be great if there were dozens of volunteers to promote new
>> proposals but the sad truth is very few people are capable of writing an
>> amendment to the RM (and I certainly include myself is the 'not able'
>> camp). When people talk about "language lawyers" it isn't far from the
>> truth! The knowledge of the language has to be absolutely inside-out if
>> you want to be able to amend the actual language - not so much the
>> standard library but even that's tricky.

I agree. Looking at references of other languages reveals that some are
quite different from ARM, and not in the positive sense. Some I have read
are almost tutorials to the language with very few syntax descriptions.
Such manuals certainly are ambiguous in many places and some concepts
ar eleft unclear altogether.

>Yes, and they have to be very carefully reviewed, both for language issues
>and for implementation ones. (You don't want the new features to cause
>programs to run much slower -- the dreaded "distributed overhead"). These
>proposals kept getting messier and messier, and that played a part in their
>eventually being abandoned.

You don't have to tell, I've programmed in C++ (hopefully there aren't
any C++ programmers reading this...)

>For instance, Postconditions required a mechanism to get at the original
>values of parameters. Which meant that those values had to be saved
>somewhere. That would be a huge performance hit unless it is possible to
>tell in advance whether or not the original value would be required. We
>never had a proposal with that property (it really needs to be visible on a
>purely syntax basis; otherwise it can be too complex to figure out, as it
>would depend on name resolution and visibility).

Programming by contract features are IMHO disabled (speaking in free
software terminology) when a stable version is released, or in other
words, when a final product goes out. Xconditions are certainly a huge
performance hit, but not as much as inserting a break point at the
beginning and end of every subprogram in a debugger and then manually
examining parameter and result values, if program behaves oddly. All other
run-time checks are also expensive and that is why Ada provides a way to
disable them. Xconditions could actually speed up code that is considered
to be stable. This is because subprograms' parameters' validity checking
can be written as a precondition and does not need to be executed, when
the caller knows that a bad value cannot be passed in any situation.
For example subprograms of Ada.Strings's child packages have many checks for
their parameters' validity and as some of the subprograms are implemented
(in GNAT) in terms of others, the checks are doubled.

-- 
Tapio

Re: Contract checking in Ada

[Dmitry A. Kazakov]

On Fri, 01 Apr 2005 08:02:54 GMT, Tapio Kelloniemi wrote:

> Randy Brukardt <randy@rrsoftware.com> wrote:

>>For instance, Postconditions required a mechanism to get at the original
>>values of parameters. Which meant that those values had to be saved
>>somewhere. That would be a huge performance hit unless it is possible to
>>tell in advance whether or not the original value would be required. We
>>never had a proposal with that property (it really needs to be visible on a
>>purely syntax basis; otherwise it can be too complex to figure out, as it
>>would depend on name resolution and visibility).
> 
> Programming by contract features are IMHO disabled (speaking in free
> software terminology) when a stable version is released, or in other
> words, when a final product goes out. Xconditions are certainly a huge
> performance hit, but not as much as inserting a break point at the
> beginning and end of every subprogram in a debugger and then manually
> examining parameter and result values, if program behaves oddly. All other
> run-time checks are also expensive and that is why Ada provides a way to
> disable them. Xconditions could actually speed up code that is considered
> to be stable. This is because subprograms' parameters' validity checking
> can be written as a precondition and does not need to be executed, when
> the caller knows that a bad value cannot be passed in any situation.
> For example subprograms of Ada.Strings's child packages have many checks for
> their parameters' validity and as some of the subprograms are implemented
> (in GNAT) in terms of others, the checks are doubled.

That is the problem. Basically the question is: can a contract violation be
handled at run-time? I would say no. Theoretically, a contract violation
should kill the program, reboot the computer (and all other computers of
world (:-)).

If so, then the validity checks cannot be turned into contract checks.
Compare:

begin
   Do_One_Thing (X);
exception
   when Constraint_Error =>
      Do_Other_Thing (X); -- This is OK
end;

Compare with:

begin
   Do_One_Thing (X);
exception
   when Contract_Error =>
      Do_Other_Thing (X); -- Nonsense
end;

Validity, constraint checks /= contract checks.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Contract checking in Ada

[Randy Brukardt]

"Tapio Kelloniemi" <spam17@thack.org> wrote in message
news:Oe73e.6358$qc.2422@reader1.news.jippii.net...
...
> Programming by contract features are IMHO disabled (speaking in free
> software terminology) when a stable version is released, or in other
> words, when a final product goes out.

That's a horrible idea. That's like wearing a life-preserver when training
on land, and then discarding it when you go to sea!

The problem is that assertions of all stripes (like runtime checks) detect
unanticipated conditions before much damage is done. And no one antipicates
(and thus tests) every possible issue.

Yes, sometimes you have to suppress checks (and conditions), but you want to
do that only in the most performance critical parts of your application. A
feature that makes your whole application like that is a feature that will
be rarely used.

> Xconditions are certainly a huge
> performance hit, but not as much as inserting a break point at the
> beginning and end of every subprogram in a debugger and then manually
> examining parameter and result values, if program behaves oddly. All other
> run-time checks are also expensive and that is why Ada provides a way to
> disable them. Xconditions could actually speed up code that is considered
> to be stable. This is because subprograms' parameters' validity checking
> can be written as a precondition and does not need to be executed, when
> the caller knows that a bad value cannot be passed in any situation.
> For example subprograms of Ada.Strings's child packages have many checks
for
> their parameters' validity and as some of the subprograms are implemented
> (in GNAT) in terms of others, the checks are doubled.

That's also a bad idea. Indeed, we had something like that in pragma Assert
and eventually dropped it because of the objections. Again, the issue is
that you need to be checking for the unanticipated. You shouldn't be
assuming that the asserts will pass without checking.

OTOH, the compiler may be able to optimize out checks and preconditions on
calls given the preconditions on the arguments. That's fine (its the reason
for the null exclusion, for instance); but doing so by assumption, rather
than by checking, is bad news.

                     Randy.

Re: Contract checking in Ada

[Hyman Rosen]

Randy Brukardt wrote:
> The problem is that assertions of all stripes (like runtime checks) detect
> unanticipated conditions before much damage is done. And no one antipicates
> (and thus tests) every possible issue.

But in detecting those unanticipated conditions, they do maximum damage.
We've had this discussion before. If some operation raises Constraint
Error or Program Error, or fails some other assertion, the action usually
taken is to abort the program. That can mean losing unsaved work, or just
rendering a program unusable where it might otherwise muddle through and
continue working even thiugh it has done something illegal.

Re: Contract checking in Ada

[Randy Brukardt]

"Hyman Rosen" <hyrosen@mail.com> wrote in message
news:XcY3e.953$7b.886@trndny02...
> Randy Brukardt wrote:
> > The problem is that assertions of all stripes (like runtime checks)
detect
> > unanticipated conditions before much damage is done. And no one
antipicates
> > (and thus tests) every possible issue.
>
> But in detecting those unanticipated conditions, they do maximum damage.
> We've had this discussion before. If some operation raises Constraint
> Error or Program Error, or fails some other assertion, the action usually
> taken is to abort the program. That can mean losing unsaved work, or just
> rendering a program unusable where it might otherwise muddle through and
> continue working even thiugh it has done something illegal.

Only if the program designer hasn't taken steps to do something useful on
unanticipated conditions. And if they haven't done so, that usually suggests
shoddy design.

Our web and mail programs trap unexpected exceptions, log them, and reset
the program to continue running. Our spam filter traps the message for
hand-analysis. None of them "abort the program".

OTOH, our Ada compiler does let unhandled exceptions abort the program. That
seems like a better choice than generating garbage code. There have been a
couple instances of failures happening because of broken assertions, but the
vast majority have been real problems. Had the compiler gone ahead and
generated something, it might has worked -- for a while. Or it might have
done something weird that would have cost everyone lots of debugging time.
I'd rather get my errors up front.

There might be some programs that "muddle through" OK, but I haven't seen or
used many of them. The muddling through in the bookeeping software I used
probably caused the data file to get corrupted, which made me spend most of
a day reentering stuff. I would rather have had a clean crash...

It is necessary to decide what to do with unantipated conditions, but that's
an important part of application design. When it is not done, you get
security holes and corrupted data files that could easily have been
prevented.

                                Randy.

Re: Contract checking in Ada

[Peter Amey]

Tapio Kelloniemi wrote:
[snip]
> 
> But back to my original question, how could I implement programming by
> contract now when the designers have abandoned it in their great wisdom?
> SPARKADA seems not to be free software, so it is not an option for me.
> 

SPARK is available free for academic use if that is of any help to you.

[snip]

Peter

Re: Contract checking in Ada

[adaworks]

"Peter Amey" <peter.amey@praxis-cs.co.uk> wrote in message
news:3b4bloF6h1fppU1@individual.net...
>
>
> Tapio Kelloniemi wrote:
> [snip]
> >
> > But back to my original question, how could I implement programming by
> > contract now when the designers have abandoned it in their great wisdom?
> > SPARKADA seems not to be free software, so it is not an option for me.
> >
>
> SPARK is available free for academic use if that is of any help to you.
>
One the graduate students at our school is, in fact, pursuing a thesis that
involves
SPARK and we are quite enthusiastic to see what kind of results whe will get.
We have been pleased with the generous support so far provided by Praxis in
making this effort go smoothly.

Richard Riehle

Re: Contract checking in Ada

[Duncan Sands]

Hi Tapio,

> 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.

the GNAT run-time library is built without run-time checks (-gnatp).

Ciao,

D.

Re: Contract checking in Ada

[Martin Dowie]

Duncan Sands wrote:
> Hi Tapio,
> 
> 
>>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.
> 
> 
> the GNAT run-time library is built without run-time checks (-gnatp).

I think that the OP is complaining that there are explicit checks
in the subprograms that /can't/ be turned off - even though you
know that you're code isn't "broken".

Cheers

-- Martin