From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00
	autolearn=unavailable autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: 103376,67afd31696e08d55
X-Google-Attributes: gid103376,public
X-Google-ArrivalTime: 2003-03-26 01:00:43 PST
Path: archiver1.google.com!postnews1.google.com!not-for-mail
From: volkert@nivoba.de (Volkert)
Newsgroups: comp.lang.ada
Subject: Re: Ada and Design By Contract
Date: 26 Mar 2003 01:00:42 -0800
Organization: http://groups.google.com/
Message-ID: <d37844cb.0303260100.58180d8d@posting.google.com>
References: <d37844cb.0303231055.610fead@posting.google.com>
 <3E7EE470.5030807@praxis-cs.co.uk>
 <d37844cb.0303240940.13be700e@posting.google.com>
 <3E801279.80905@praxis-cs.co.uk>
NNTP-Posting-Host: 138.189.120.38
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 8bit
X-Trace: posting.google.com 1048669243 31944 127.0.0.1 (26 Mar 2003 09:00:43
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: 26 Mar 2003 09:00:43 GMT
Xref: archiver1.google.com comp.lang.ada:35714
Date: 2003-03-26T09:00:43+00:00
List-Id: <comp.lang.ada>

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