Re: Ada and Design By Contract

[Peter Amey <peter.amey@praxis-cs.co.uk>]

Volkert wrote:
> Dear Peter,
> 
> 
>>>Volkert
>>
>>A small (but probably not the best) example:
>>
>>package P is
>>   function IsFull return Boolean;
>>   -- we may only want this function for assertion checking, not as
>>   -- part of our normally executable code
>>
>>   procedure Push ...
>>   --! pre not IsFull; -- run time assertion
>>   ...
>>end P;
> 
> IsFull is part of the contact between client/supplier. 
> The client needs access to IsFull. As a consequence
> IsFull has to be part of the executible code.
> 
> 
>>with P;
>>package Q is
>>   procedure SomeOperation;
>>   -- Calls P.Push so we really need to propagate the precondition here
>>   --! pre not P.IsFull;
>>   ...
>>end Q;
> 
> The caller has to check that not(P.isFull) is true, else 
> he can possibly break the contract. It is clear, that the caller 
> must implement this check in its own body
> 
> 
>>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.

Peter