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-Thread: 103376,7b0188e023be40b6 X-Google-Attributes: gid103376,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news2.google.com!news3.google.com!news.germany.com!newsfeed20.multikabel.net!multikabel.net!newsfeed10.multikabel.net!feeder1.cambriumusenet.nl!feed.tweaknews.nl!81.171.88.15.MISMATCH!lightspeed.eweka.nl!81.171.88.16.MISMATCH!eweka.nl!hq-usenetpeers.eweka.nl!cyclone01.ams2.highwinds-media.com!news.highwinds-media.com!npeersf01.ams.highwinds-media.com!newsfe12.ams2.POSTED!7564ea0f!not-for-mail Message-ID: From: JP Thornley Newsgroups: comp.lang.ada Subject: Re: SPARK Examiner -- visibility of Ada.Strings.Unbounded (and probably lots of other packages) References: <8c753bd7-3df6-418a-8cd7-342af6eadeff@g38g2000yqd.googlegroups.com> MIME-Version: 1.0 Content-Type: text/plain;charset=us-ascii;format=flowed User-Agent: Turnpike/6.07-S (<9U$lieR1assNeRFOx7VcA7nRfr>) NNTP-Posting-Host: 80.177.171.182 X-Complaints-To: abuse@demon.net X-Trace: newsfe12.ams2 1238085042 80.177.171.182 (Thu, 26 Mar 2009 16:30:42 UTC) NNTP-Posting-Date: Thu, 26 Mar 2009 16:30:42 UTC Date: Thu, 26 Mar 2009 16:30:17 +0000 Xref: g2news2.google.com comp.lang.ada:5315 Date: 2009-03-26T16:30:17+00:00 List-Id: In article , Tim Rowe writes >Ludovic Brenta wrote: > >> I don't think Ada.Strings.Unbounded is part of SPARK. SPARK is a >> *subset* of Ada that removes everything not statically provable. > >It isn't. But John Barnes, in High Integrity Software: The SPARK >Approach to Safety and Security, says "where absolutely essential [...] >any feature of full Ada [...] can be used in parts of a program covered >by the special hide directive which tells the examiner that part of a >program is not to be examined". I just can't work out how to hide the >relevant bit -- I'm only allowed the hide after immediately after >private, after is and after the begin of a body -- that means that I >can't get the with inside the hidden part. Tim, Don't worry about the 'with' - the Examiner will flag an error but it (probably) won't stop the Examiner happily examining the visible part of the spec. Again, have a look at SPARK_IO specification - there is a with (but no inherit) for Text_IO. This generates a message from the Examiner but since it is only needed in the private part (which is hidden) the specification itself is examined OK and can be referenced in other proper SPARK text. Cheers, Phil -- JP Thornley