Re: Ada and Design By Contract

[Jeffrey Carter <spam@spam.com>]

Peter Amey wrote:
> 
> Volkert wrote:
> 
>>> with Q;
>>> package R is
>>>   procedure AnotherOperation;
>>>   -- this calls Q.SomeOperation;
>>>   -- It's execution will involve the check not P.IsFull but P is not
>>>   -- visible here.
>>> end R;
>>
>> 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.

It seems to me that R.Anotheroperation is responsible for checking the 
precondition to Q.Someotheroperation, not the client of R.

-- 
Jeff Carter
"This school was here before you came,
and it'll be here before you go."
Horse Feathers