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

[JP Thornley <jpt@diphi.demon.co.uk>]

In article <OPWdnbuqg7uyN1bUnZ2dnUVZ8qOWnZ2d@posted.plusnet>, Tim Rowe 
<spamtrap@tgrowe.plus.net> 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