Re: Ada and Design By Contract

[Colin_Paul_Gloster@ACM.org (Colin Paul Gloster)]

Peter Amey wrote:
"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)."

Yesterday I received in the post an application form for another Adaxia
event which is to have a presentation by a very pro-OO, pro-C++, probably
pro-abstraction expert so I would have a doubt that he practises all the
pro-correctness policies of SPARK users'. I quoted an email of this
speaker's in which he/she disapproved of one way of emulating a very small
part of Ada with C in "some people who have seen the light still do not
learn (single = in C conditions)" on Team Ada which is currently archived
at HTTP://WWW.ACM.org/archives/wa.cgi?A2=ind0211&L=team-ada&F=&S=&P=300
with timestamp Tue, 19 Nov 2002 14:57:41 +0000. Examining his email
closely he could be interpreted to be pro-Ada. On the plus side, he
provided me with moral support to learn Ada and in coping with gross
inefficiency from an ACM office when I was joining the Association for
Computing Machinery.

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