Re: SPARK examiner visibility problem

[Phil Thornley <phil.jpthornley@googlemail.com>]

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