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-Language: ENGLISH,ASCII Path: g2news2.google.com!postnews.google.com!v2g2000vbb.googlegroups.com!not-for-mail From: Phil Thornley Newsgroups: comp.lang.ada Subject: Re: SPARK examiner visibility problem Date: Mon, 14 Sep 2009 09:12:36 -0700 (PDT) Organization: http://groups.google.com Message-ID: 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 1252944757 28283 127.0.0.1 (14 Sep 2009 16:12:37 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Mon, 14 Sep 2009 16:12:37 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: v2g2000vbb.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:8322 Date: 2009-09-14T09:12:36-07:00 List-Id: On 13 Sep, 23:47, Laurie Dillon 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. I feel that this needs a more complete response than I gave this morning (which was wrong anyway). > > I have the following package spec: > > -------------------------------------------------------------------------= --=AD---------- > > with Ada.Text_IO; > package Std_IO > -- =A0encapsulates IO to and from standard input and standard output > --# own stdin: Istream_Type; > --# =A0 =A0 =A0 =A0stdout: Ostream_Type; > --# initializes stdin, > --# =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 stdout; > is > =A0 =A0--# type Istream_Type is abstract; > =A0 =A0--# type Ostream_Type is abstract; > > =A0 =A0procedure New_Line; > =A0 =A0-- =A0output a new line to stdout > =A0 =A0--# global in out stdout; > =A0 =A0--# derives stdout from *; > > =A0 =A0procedure Put_Line (Item =A0: in String); > =A0 =A0-- =A0output a string followed by a carriage return to stdout > =A0 =A0--# global in out stdout; > =A0 =A0--# derives stdout from *, Item; > > =A0 =A0procedure Put_Integer (Item : in Integer); > =A0 =A0-- =A0output an integer to stdout > =A0 =A0--# global in out stdout; > =A0 =A0--# derives stdout from *, Item; > > =A0 =A0procedure Get_Integer (Item : out Integer; > =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 OK =A0 : out Boolean)= ; > =A0 =A0-- =A0input an integer from stdin > =A0 =A0--# global in stdin; > =A0 =A0--# derives Item, OK from stdin; > > end Std_IO; > -------------------------------------------------------------------------= --=AD------------------------------- > > The examiner has no problem with this package (the body carries a > #hide Std_IO annotation). =A0But when I try to examine a package spec > (or body) that inherits Std_IO, I get semantic errors at every > reference to Std_IO.stdin and Std_IO.stdout. > > 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; Every import and export of a procedure must be either a parameter or named in a global annotation. Here you have said that the exported parameter theLoc is derived from Std_IO.stdin but that item is not visible. For this annotation to be acceptable Std_IO.stdin must be imported in a global annotation: --# global in 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. > -------------------------------------------------------------------------= --=AD---------- > > I thought the own declaration for stdin in the spec of Spark_IO should > qualify as "a preceding legal global annotation". =A0 What am I missing > here? > > Analysis of the body of myGps gives similar errors. =A0For example: > > =A0 =A0Unit name: =A0MyGps > =A0 =A0Unit type: =A0package body > =A0 =A0Unit has been analysed, any errors are listed below. > > 14 error(s) or warning(s) > > Line > =A0 35 =A0 =A0 =A0 =A0Std_IO.Put_Line (Item =3D> "Enter x-coordinate of l= ocation : > "); > =A0 =A0 =A0 =A0 =A0 =A0 ^1,2 > *** ( =A01) =A0Semantic Error =A0 =A0: 25: The identifier Std_IO.stdout > (imported by called > =A0 =A0 =A0 =A0 =A0 =A0subprogram) is not visible at this point. > *** ( =A02) =A0Semantic Error =A0 =A0: 24: The identifier Std_IO.stdout > (exported by called > =A0 =A0 =A0 =A0 =A0 =A0subprogram) is not visible at this point. This must be the code of GetLocation. The Examiner has identified that the procedure Put_Line both imports and exports Std_IO.stdout, but at the moment it isn't visible to the procedure GetLocation (see above). Since these errors state that Std_IO.stdout is both imported and exported by Put_Line then GetLocation must also both import and export it, so I guess its annotations should be (at least): --# global in out Std_IO.stdout; --# derives theLoc from --# Std_IO.Stdout --# & Std_IO.Stdout from --# *; Hope this is clearer than previously. Phil