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: a07f3367d7,a094903f87897fa4
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII
Path: 
 g2news2.google.com!postnews.google.com!t2g2000yqn.googlegroups.com!not-for-mail
From: Phil Thornley <phil.jpthornley@googlemail.com>
Newsgroups: comp.lang.ada
Subject: Re: SPARK examiner visibility problem
Date: Mon, 14 Sep 2009 00:40:39 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: <2e0ddf8d-4a67-48f1-931e-e14b6c5a95ef@t2g2000yqn.googlegroups.com>
References: <8d72d20b-489b-4494-9b13-1b00ee902850@j4g2000yqa.googlegroups.com>
NNTP-Posting-Host: 80.177.171.182
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: quoted-printable
X-Trace: posting.google.com 1252914040 22667 127.0.0.1 (14 Sep 2009 07:40:40
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Mon, 14 Sep 2009 07:40:40 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: t2g2000yqn.googlegroups.com; posting-host=80.177.171.182;
	posting-account=Fz1-yAoAAACc1SDCr-Py2qBj8xQ-qC2q
User-Agent: G2/1.0
X-HTTP-UserAgent: Mozilla/4.0 (compatible; MSIE 7.0; Windows NT 5.1;
	Trident/4.0; .NET CLR 1.1.4322; .NET CLR 2.0.50727; .NET CLR 3.0.4506.2152;
	.NET CLR 3.5.30729),gzip(gfe),gzip(gfe)
Xref: g2news2.google.com comp.lang.ada:8319
Date: 2009-09-14T00:40:39-07:00
List-Id: <comp.lang.ada>

On 13 Sep, 23:47, Laurie Dillon <lauradi...@gmail.com> wrote:
> I am having trouble with a toy example of encapsulating IO for a SPARK
> program. =A0My example seems to be consistent with the Spark_IO example
> in the Barnes book.
>
[...]

> For example, consider the following spec:
> -------------------------------------------------------------------------=
--=AD--------
> --# inherit Std_IO;
> package MyGps
> --# own home;
> is
>
> =A0 =A0type Location is
> =A0 =A0record
> =A0 =A0 =A0 x : Integer;
> =A0 =A0 =A0 y : Integer;
> =A0 =A0end record;
>
> =A0 =A0procedure MoveTo (theLoc : in Location);
> =A0 =A0-- =A0moves home to the given location
> =A0 =A0--# global out home;
> =A0 =A0--# derives home from theLoc;
>
> =A0 =A0function Distance (theLoc : Location) return Integer;
> =A0 =A0-- =A0returns the (taxi) distance from home to the given location
> =A0 =A0--# global home;
>
> =A0 =A0procedure GetLocation (theLoc : out Location);
> =A0 =A0-- =A0prompts user for theLoc
> =A0 =A0--# derives theLoc from Std_IO.stdin;
>
> end MyGps;
> -------------------------------------------------------------------------=
--=AD------------------
> Examiner report says:
>
> =A0 =A0Unit name: =A0MyGps
> =A0 =A0Unit type: =A0package specification
> =A0 =A0Unit has been analysed, any errors are listed below.
>
> 1 error(s) or warning(s)
>
> Line
> =A0 23 =A0 =A0 --# derives theLoc from Std_IO.stdin;
> =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0^1
> *** ( =A01) =A0Semantic Error =A0 =A0:752: The identifier Std_IO.stdin is
> either undeclared
> =A0 =A0 =A0 =A0 =A0 =A0or not visible at this point. This identifier must=
 appear
> in a
> =A0 =A0 =A0 =A0 =A0 =A0preceding legal global annotation or formal parame=
ter list.

It needs to have the global annotation added :

   procedure GetLocation (theLoc : out Location);
   --  prompts user for theLoc
   --# global in Std_IO.stdin;
   --# derives theLoc from Std_IO.stdin;

Cheers,

Phil