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

[roderick.chapman@googlemail.com]

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;