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 02:07:30 PST
Path: 
 archiver1.google.com!news1.google.com!newsfeed.stanford.edu!news-spur1.maxwell.syr.edu!news.maxwell.syr.edu!newsfeed.icl.net!newsfeed.fjserv.net!colt.net!peernews3.colt.net!newsfeed.stueberl.de!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 10:09:15 +0000
Message-ID: <3E802ACB.40108@praxis-cs.co.uk>
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>
 <slrnb809rs.d8a.Colin_Paul_Gloster@camac.dcu.ie>
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 1048586849 78735240 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:35673
Date: 2003-03-25T10:09:15+00:00
List-Id: <comp.lang.ada>

[snip]

> In a later post, Peter Amey said:
> 
> "[..]  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."
> 
> Could you please describe the SPARK concept of "inherit"?
> 
> Regards,
> Colin Paul Gloster

Inherit, in this context, is a package-level annotation which behaves 
rather like "with" (actually rather like the transitive closure of the 
with clauses) but in proof context.  In my example, package R would 
inherit packages P and Q even though it only withs Q.  This would make 
the proof function P.IsFull visible at the place needed to check the 
contract.

Inheritance does of course have other connotations nowadays!

Peter