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=-0.3 required=5.0 tests=BAYES_00, REPLYTO_WITHOUT_TO_CC autolearn=no 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 01:55:09 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!diablo.theplanet.net!news.indigo.ie!feeder.news.heanet.ie!not-for-mail Newsgroups: comp.lang.ada From: Colin_Paul_Gloster@ACM.org (Colin Paul Gloster) Subject: Re: Ada and Design By Contract References: <3E7EE470.5030807@praxis-cs.co.uk> <3E801279.80905@praxis-cs.co.uk> Reply-To: Colin_Paul_Gloster@ACM.org Message-ID: User-Agent: slrn/0.9.7.0 (SunOS) Organization: Dublin City University (DCU) Cache-Post-Path: ns2-ext.dcu.ie!unknown@camac.dcu.ie X-Cache: nntpcache 2.3.3 (see http://www.nntpcache.org/) Date: 25 Mar 2003 09:55:08 GMT NNTP-Posting-Date: 25 Mar 2003 09:55:08 GMT NNTP-Posting-Host: 136.206.1.1 X-Trace: 1048586108 reader.news.heanet.ie 176 [::ffff:136.206.1.1]:48572 Xref: archiver1.google.com comp.lang.ada:35672 Date: 2003-03-25T09:55:08+00:00 List-Id: 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