Re: Ada and Design By Contract

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

[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