Re: Ada and Design By Contract

[volkert@nivoba.de (Volkert)]

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? 

> 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.
Part of a client/supplier contract can only the Entites visible
in the Ada Spec. For the post condition i can think that the
assertion statement can have also access to the private part of 
the spec. But i see no problems to make the contract relevant 
informations visible in the public part of a spec.

Volkert