Re: Ada and Design By Contract

["Randy Brukardt" <randy@rrsoftware.com>]

Peter Amey wrote in message <3E817504.5040806@praxis-cs.co.uk>...
>> The check is made in the body of Q.SomeOperations. Why should
>> P.IsFull visible here?
>
>Because it is too late to wait until Q.SomeOperation is executed in
>breach of contract.  The real cause of the contract failure is
>AnotherOperation's attempt to call Q.SOmeOtherOperation in a way that
>will cause the stack to overflow.  If we want to try and deal with the
>problem we need to know where the dangerous condition started.   In our
>view this is better done by proof than by dynamic checks.


Which is why Janus/Ada was always included a call walkback with every
unhandled exception, and includes this information in
Exception_Information. It's often the case that the location of an
exception being raised (assertion failure) isn't enough information.
But, usually (probably more than 90% of the time), knowing the caller(s)
allow tracing/fixing the bug without having to add additional code (or
even run the program again).

Proof has its place, of course, but I don't think that most systems can
justify the extra work to develop that way. A few carefully placed
run-time assertions (combined with good compiler suppprt - it's not
surprising that Gnat added a walkback feature) are sufficient for
non-critical systems.

               Randy.