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-7-bit
Path: 
 g2news2.google.com!postnews.google.com!c11g2000yqj.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:51:48 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: 
 <304930c9-d79d-4de7-89fb-706a35986f93@c11g2000yqj.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: 7bit
X-Trace: posting.google.com 1238086309 19489 127.0.0.1 (26 Mar 2009 16:51:49
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Thu, 26 Mar 2009 16:51:49 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: c11g2000yqj.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:5317
Date: 2009-03-26T09:51:48-07:00
List-Id: <comp.lang.ada>

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;