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=ham
	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-25 00:23:45 PST
Path: 
 archiver1.google.com!news1.google.com!newsfeed.stanford.edu!headwall.stanford.edu!fu-berlin.de!uni-berlin.de!213.155.153.242!not-for-mail
From: Peter Amey <peter.amey@praxis-cs.co.uk>
Newsgroups: comp.lang.ada
Subject: Re: Ada and Design By Contract
Date: Tue, 25 Mar 2003 08:25:29 +0000
Message-ID: <3E801279.80905@praxis-cs.co.uk>
References: <d37844cb.0303231055.610fead@posting.google.com>
 <3E7EE470.5030807@praxis-cs.co.uk>
 <d37844cb.0303240940.13be700e@posting.google.com>
NNTP-Posting-Host: 213.155.153.242
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii; format=flowed
Content-Transfer-Encoding: 7bit
X-Trace: fu-berlin.de 1048580623 78913601 213.155.153.242 (16 [69815])
User-Agent: Mozilla/5.0 (Windows; U; Windows NT 5.0; en-US;
 rv:1.0.2) Gecko/20030208 Netscape/7.02
X-Accept-Language: en-us, en
Xref: archiver1.google.com comp.lang.ada:35669
Date: 2003-03-25T08:25:29+00:00
List-Id: <comp.lang.ada>



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