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.
>
[...]

> 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;
>
> 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.

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