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,FREEMAIL_FROM
	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
Path: 
 g2news2.google.com!postnews.google.com!d19g2000yqb.googlegroups.com!not-for-mail
From: roderick.chapman@googlemail.com
Newsgroups: comp.lang.ada
Subject: Re: SPARK Examiner -- visibility of Ada.Strings.Unbounded (and
	probably lots of other packages)
Date: Thu, 26 Mar 2009 09:26:17 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: 
 <3261f160-94a1-42c6-bd83-4d3173aea341@d19g2000yqb.googlegroups.com>
References: <MrqdnWzwueTeC1bUnZ2dnUVZ8r-WnZ2d@posted.plusnet>
	<8c753bd7-3df6-418a-8cd7-342af6eadeff@g38g2000yqd.googlegroups.com>
	<OPWdnbuqg7uyN1bUnZ2dnUVZ8qOWnZ2d@posted.plusnet>
NNTP-Posting-Host: 217.205.167.137
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: quoted-printable
X-Trace: posting.google.com 1238084777 14412 127.0.0.1 (26 Mar 2009 16:26:17
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Thu, 26 Mar 2009 16:26:17 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: d19g2000yqb.googlegroups.com; posting-host=217.205.167.137;
	posting-account=HCzrEgkAAABSfGsTnv-u5wET6EzuneVi
User-Agent: G2/1.0
X-HTTP-UserAgent: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-GB; rv:1.9.0.7)
	Gecko/2009021910 Firefox/3.0.7,gzip(gfe),gzip(gfe)
Xref: g2news2.google.com comp.lang.ada:5314
Date: 2009-03-26T09:26:17-07:00
List-Id: <comp.lang.ada>

On Mar 26, 4:15=A0pm, Tim Rowe <spamt...@tgrowe.plus.net> wrote:
> 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.

The hide annotation is only used with entire subprogram bodies,
package
private parts, package bodies, package initialization parts, and
exception handler parts.

It makes no sense at all to try to hide the visible part
of a package specification.

You need a shadow or a thick binding.
 - Rod