Re: Ada and Design By Contract

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

Volkert wrote:
[snip]
> 
>>The big problem here is that the really interesting 
>>contractual claims may involve items not visible at the point where the 
>>contract is being checked (unless the code is rewritten with reduced 
>>abstraction to make them visible).
> 
> I see not the problem. Can you give a short example.
> 
> 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;

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;

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 really difficult cases are those that involve indirect manipulation 
of global data in remote packages.  These problems are worst when trying 
to express a postcondition that depends on the initial values of that 
global data.

SPARK avoids these problems by having two different sets of scopes: 
program (i.e. Ada) context and proof context.  In the above example, we 
would make IsFull a proof function (i.e. not part of the executable 
code) and make use of "inherit" to make it visible without having to 
increase the number of with clauses.

regards


Peter