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

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

[Tim Rowe]

Now that a GPL version of SPARK Examiner has been announced, I suppose 
this group will be getting a flood of queries on how to use it. Well, I 
hope so, because that would indicate a large take-up -- good for 
software as a whole, and presumably what Praxis HIS and AdaCore are 
hoping for.

So let me try to get in ahead of the flood. I'm trying to put my Ada 
learning exercise into SPARK, and I'm using the evaluation version of 
Examiner (and the gnat compiler). I have
    with Ada.Strings.Unbounded;
at the start of a package file, and SPARK Examiner complains:
    1  with Ada.Strings.Unbounded;
            ^1
--- (  1)  Warning           :  1: The identifier Ada is either 
undeclared or not
            visible at this point.

I can't work out how to make Ada.Strings.Unbounded visible to examiner. 
Could somebody point me to what I'm missing, please?

Thanks!

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

[Ludovic Brenta]

On Mar 26, 3:50 pm, Tim Rowe <spamt...@tgrowe.plus.net> wrote:
> Now that a GPL version of SPARK Examiner has been announced, I suppose
> this group will be getting a flood of queries on how to use it. Well, I
> hope so, because that would indicate a large take-up -- good for
> software as a whole, and presumably what Praxis HIS and AdaCore are
> hoping for.
>
> So let me try to get in ahead of the flood. I'm trying to put my Ada
> learning exercise into SPARK, and I'm using the evaluation version of
> Examiner (and the gnat compiler). I have
>     with Ada.Strings.Unbounded;
> at the start of a package file, and SPARK Examiner complains:
>     1  with Ada.Strings.Unbounded;
>             ^1
> --- (  1)  Warning           :  1: The identifier Ada is either
> undeclared or not
>             visible at this point.
>
> I can't work out how to make Ada.Strings.Unbounded visible to examiner.
> Could somebody point me to what I'm missing, please?
>
> Thanks!

I don't think Ada.Strings.Unbounded is part of SPARK. SPARK is a
*subset* of Ada that removes everything not statically provable. By
definition, anything unbounded is not statically provable. I would
even assume that SPARK forbids the entire Ada run-time library (i.e.
package Ada and its children) but presumably provides a replacement
library (perhaps a package SPARK?)

--
Ludovic Brenta.

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

[Georg Bauhaus]

Ludovic Brenta schrieb:

> I don't think Ada.Strings.Unbounded is part of SPARK. SPARK is a
> *subset* of Ada that removes everything not statically provable.

And some other things ...

> By
> definition, anything unbounded is not statically provable. I would
> even assume that SPARK forbids the entire Ada run-time library (i.e.
> package Ada and its children) but presumably provides a replacement
> library (perhaps a package SPARK?)


My outdated copy of the SPARK book describe a Spark I/O package.
Also, package Interfaces does not pass, so if that is an important
base for run-time support ...

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

[roderick.chapman]

On Mar 26, 3:18 pm, Georg Bauhaus <rm.dash-bauh...@futureapps.de>
wrote:

> My outdated copy of the SPARK book describe a Spark I/O package.
> Also, package Interfaces does not pass, so if that is an important
> base for run-time support ...

You'll need what we call a "shadow" package specification that
offers a SPARK-friendly (i.e. legal SPARK) version of an
otherwise non-SPARK package.

You then use the Examiner's "index file" mechamisn to
make the Examiner read in the shadow specification, while
your compiler, of course, uses the "real" Ada version.

More info in the book in section 13.1.

Ada.Strings.Unbounded is likely to be very hard
to shadow, though, since it is full on non-SPARK
things like String_Access and returning String
from a function, which is beyond the run-time
library profile support by SPARK.


Same goes for Interfaces - most of it is legal SPARK,
but (in GNAT anyway) the overloading of the various
Shift_ and Rotate_ functions is not legal in SPARK.

If you really need access to those things, then
create a "thick binding" that "un-overloads" those
functions in a distinct package.   SPARK_IO
is an example of this - it offers a thick-binding
to the underlying Ada.Text_IO package.

 - Rod Chapman, SPARK Team

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

[roderick.chapman]

PS...if you want an example of some really well-written
SPARK, then feel free to download the Tokeneer
project archive from www.adacore.com/tokeneer
 - Rod

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

[Tim Rowe]

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.

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

[roderick.chapman]

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

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

[JP Thornley]

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

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

[roderick.chapman]

Here's a short example of shadowing and using Ada.Strings
and Ada.Strings.Unbounded.  You'll also need the
spec and body of SPARK_IO supplied with the SPARK tools
distribution.
 - Rod

----------------------

spark.sw
--------

-index=spark -flow=data -warn=all

spark.idx
---------

ada.strings spec is in ada-strings.shs
ada.strings.unbounded spec is in ada-strings-unbounded.shs
spark_io spec is in spark_io.ads

all.wrn
-------

pragma all
hidden
notes

ada-strings.shs
---------------

package Ada.Strings
is
   Space : constant Character := ' ';

   -- Wide_Space is not SPARK

   -- Exceptions Length_Error etc are not SPARK

   type Alignment  is (Left, Right, Center);

   -- Cannot overload Left and Right in SPARK
   -- type Truncation is (Left, Right, Error);

   type Membership is (Inside, Outside);

   type Direction  is (Forward, Backward);

   -- Cannot overload Left and Right in SPARK
   -- type Trim_End   is (Left, Right, Both);

end Ada.Strings;


ada-strings-unbounded.shs
-------------------------

--# inherit Ada.Strings;
package Ada.Strings.Unbounded
is
   -- Just a few things here for example

   type Unbounded_String is private;

   Null_Unbounded_String : constant Unbounded_String;

   function Length (Source : in Unbounded_String) return Natural;

   function To_Unbounded_String (Source : in String)
      return Unbounded_String;

   -- Add more stuff here if it's legal SPARK

private
   --# hide Ada.Strings.Unbounded;
end Ada.Strings.Unbounded;


main.adb
--------

with Ada.Strings.Unbounded,
     SPARK_IO;
--# inherit Ada.Strings.Unbounded,
--#         SPARK_IO;

--# main_program;
procedure Main
--# global in out SPARK_IO.File_Sys;
is
   X : Ada.Strings.Unbounded.Unbounded_String;
   L : Natural;
begin
   X := Ada.Strings.Unbounded.To_Unbounded_String ("Wibble");
   L := Ada.Strings.Unbounded.Length (X);
   if L = 6 then
      SPARK_IO.Put_Line (SPARK_IO.Standard_Output, "Success", 0);
   else
      SPARK_IO.Put_Line (SPARK_IO.Standard_Output, "Failure", 0);
   end if;
end Main;

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

[Tim Rowe]

roderick.chapman@googlemail.com wrote:

> You'll need what we call a "shadow" package specification that
> offers a SPARK-friendly (i.e. legal SPARK) version of an
> otherwise non-SPARK package.

Many thanks -- as is so often the case, it comes down to knowing the 
right terminology for what one is trying to look up!

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

[Tim Rowe]

Ok, I'm still not getting importing to work.

I have a package specification Foo.ads, which pure SPARK -- Examiner is 
happy with it.

I have a package specification Bar.ads, in the same directory, which begins:

with Foo;
--# inherit Foo;

(Which looks to me very like the example on p59 of the Spark95 manual 
that comes with the evaluation version of the examiner), but Examiner 
complains:
Line
    1  with Foo;
            ^1
--- (  1)  Warning           :  1: The identifier Foo is either 
undeclared or not
            visible at this point.

    2  --# inherit Foo;
                   ^2
*** (  2)  Semantic Error    :  1: The identifier Foo is either 
undeclared or not
            visible at this point.

I'm still missing something obvious, aren't I?

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

[JP Thornley]

In article <KfadnR5dBtNhTlbUnZ2dnUVZ8gqWnZ2d@posted.plusnet>, Tim Rowe 
<spamtrap@tgrowe.plus.net> writes
>Ok, I'm still not getting importing to work.
>
>I have a package specification Foo.ads, which pure SPARK -- Examiner is 
>happy with it.
>
>I have a package specification Bar.ads, in the same directory, which begins:
>
>with Foo;
>--# inherit Foo;
>
>(Which looks to me very like the example on p59 of the Spark95 manual 
>that comes with the evaluation version of the examiner), but Examiner 
>complains:
>Line
>   1  with Foo;
>           ^1
>--- (  1)  Warning           :  1: The identifier Foo is either 
>undeclared or not
>           visible at this point.
>
>   2  --# inherit Foo;
>                  ^2
>*** (  2)  Semantic Error    :  1: The identifier Foo is either 
>undeclared or not
>           visible at this point.
>
>I'm still missing something obvious, aren't I?

It looks like you aren't telling the Examiner to look at Foo first.
Check the report file that is produced (spark.rep) which lists all the 
files relevant to the run of the Examiner.  This may say that it 
couldn't find the specification of Foo.

The Examiner does not assume any file naming convention and doesn't go 
and look for files based on any expected file name (in the same way that 
Your Favourite Compiler (TM) does).

If you are just trying out some ideas in SPARK and don't want to compile 
the code then simply put everything into one file and examine that.

If you want to keep separate files then you need to tell the Examiner to 
look at all the relevant files - in this case use the command:
spark foo.ads,bar.ads

If you have more than about four files this isn't workable, so you can 
use a 'metafile' which is simply a list of files to be examined. Define 
foobar.smf as:
foo.ads
bar.ads

then use the command:
spark @foobar

This is OK as long as you are happy to examine the complete set of files 
every time.  For larger systems you need an index file, which tells the 
Examiner where to find any of the files it may need.  In this case 
define foobar.idx as:
foo specification is in foo.ads
bar specification is in bar.ads

then give this as the index_file qualifier - eg to examine the body of 
bar:
spark /index=foobar bar.adb

and the Examiner uses the index file to find first the spec of bar and 
then, because of the inherit, the spec of foo.

(Then for bigger systems you can define superindex files as well .... )

Cheers,

Phil

-- 
JP Thornley

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

[roderick.chapman]

Yeah - to process Bar, the Examiner needs to have previously seen
(or at least know where to find) the specification of Foo.

There's no "default" way to do this, since the Examiner is
designed to deal with the program-library structure and naming
scheme of _any_ Ada compiler - we can't just assume that people
name their compilation units and files like GNAT prefers to, for
example.

So...you either need to specify both files on the command line - this
works for small example but rapidly becomes tedious!  e.g.

 spark bar.ads foo.ads

The better solution is to add Bar and Foo to the Examiner's
"Index file" - this establishes a mapping from compilation
unit to filenames that the Examiner can use to automatically
find the specifications of other units.

The index file is set by the -index option so if it
says -index=spark, then you need to add the following
two lines to the spark.idx file

 foo spec is in foo.ads
 bar spec is in bar.ads

OR...you can use the "sparkmake" tool to generate the index file
for you automatically from a group of files.

More details in the book chapter 9 and section 4 of
the Examiner User Manual (which you should have - Examiner_UM.pdf).

I strongly recommend that you read through at least the first
4 chapters of the Examiner User Manual - full of useful info
I promise! :-)

All the best,
 Rod

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

[Tim Rowe]

roderick.chapman@googlemail.com wrote:
> More details in the book chapter 9 and section 4 of
> the Examiner User Manual (which you should have - Examiner_UM.pdf).
> 
> I strongly recommend that you read through at least the first
> 4 chapters of the Examiner User Manual - full of useful info
> I promise! :-)

Thanks (and thanks to Phil, too).

I am working my way through the User Manual, and John Barnes' book, but 
I find that I learn better if I try things out, and I keep trying out 
things that need stuff I haven't covered yet! I'll try to keep myself in 
check.