Re: SPARK examiner visibility problem

[Laurie Dillon <lauradillo@gmail.com>]

On Sep 14, 12:12 pm, Phil Thornley <phil.jpthorn...@googlemail.com>
wrote:
> 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.  My 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:
>
> > ---------------------------------------------------------------------------­----------
>
> > with Ada.Text_IO;
> > package Std_IO
> > --  encapsulates IO to and from standard input and standard output
> > --# own stdin: Istream_Type;
> > --#        stdout: Ostream_Type;
> > --# initializes stdin,
> > --#                 stdout;
> > is
> >    --# type Istream_Type is abstract;
> >    --# type Ostream_Type is abstract;
>
> >    procedure New_Line;
> >    --  output a new line to stdout
> >    --# global in out stdout;
> >    --# derives stdout from *;
>
> >    procedure Put_Line (Item  : in String);
> >    --  output a string followed by a carriage return to stdout
> >    --# global in out stdout;
> >    --# derives stdout from *, Item;
>
> >    procedure Put_Integer (Item : in Integer);
> >    --  output an integer to stdout
> >    --# global in out stdout;
> >    --# derives stdout from *, Item;
>
> >    procedure Get_Integer (Item : out Integer;
> >                           OK   : out Boolean);
> >    --  input an integer from stdin
> >    --# global in stdin;
> >    --# derives Item, OK from stdin;
>
> > end Std_IO;
> > ---------------------------------------------------------------------------­-------------------------------
>
> > The examiner has no problem with this package (the body carries a
> > #hide Std_IO annotation).  But 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:
> > ---------------------------------------------------------------------------­--------
> > --# inherit Std_IO;
> > package MyGps
> > --# own home;
> > is
>
> >    type Location is
> >    record
> >       x : Integer;
> >       y : Integer;
> >    end record;
>
> >    procedure MoveTo (theLoc : in Location);
> >    --  moves home to the given location
> >    --# global out home;
> >    --# derives home from theLoc;
>
> >    function Distance (theLoc : Location) return Integer;
> >    --  returns the (taxi) distance from home to the given location
> >    --# global home;
>
> >    procedure GetLocation (theLoc : out Location);
> >    --  prompts user for theLoc
> >    --# 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;
> > ---------------------------------------------------------------------------­------------------
> > Examiner report says:
>
> >    Unit name:  MyGps
> >    Unit type:  package specification
> >    Unit has been analysed, any errors are listed below.
>
> > 1 error(s) or warning(s)
>
> > Line
> >   23     --# derives theLoc from Std_IO.stdin;
> >                                  ^1
> > *** (  1)  Semantic Error    :752: The identifier Std_IO.stdin is
> > either undeclared
> >            or not visible at this point. This identifier must appear
> > in a
> >            preceding legal global annotation or formal parameter list.
> > ---------------------------------------------------------------------------­----------
>
> > I thought the own declaration for stdin in the spec of Spark_IO should
> > qualify as "a preceding legal global annotation".   What am I missing
> > here?
>
> > Analysis of the body of myGps gives similar errors.  For example:
>
> >    Unit name:  MyGps
> >    Unit type:  package body
> >    Unit has been analysed, any errors are listed below.
>
> > 14 error(s) or warning(s)
>
> > Line
> >   35        Std_IO.Put_Line (Item => "Enter x-coordinate of location :
> > ");
> >             ^1,2
> > *** (  1)  Semantic Error    : 25: The identifier Std_IO.stdout
> > (imported by called
> >            subprogram) is not visible at this point.
> > *** (  2)  Semantic Error    : 24: The identifier Std_IO.stdout
> > (exported by called
> >            subprogram) 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

Yes, thanks everyone for the good information.  In fact, the missing
global annotation was the problem.  And it makes sense that its needed
--- I knew that, but was being blind :(