Re: SPARK Examiner -- visibility of Ada.Strings.Unbounded (and probably lots of other packages)

[roderick.chapman@googlemail.com]

On Mar 26, 4:15 pm, 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