SPARK examiner visibility problem

SPARK examiner visibility problem

[Laurie Dillon]

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

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

Note that Std_IO.Put_Line is visible, as it should be.

Any insights or explanation for what I'm doing wrong in this example
will be greatly appreciated!

Thanks,

Laurie

Re: SPARK examiner visibility problem

[Britt]

There are several things that can cause the visibility error message
you are seeing. Have you created an index file (using sparkmake) that
tells the Examiner where to find each of the source files? You will
need to pass the index file to the Examiner with the /index_file
switch.

- Britt

Re: SPARK examiner visibility problem

[Laurie Dillon]

On Sep 13, 8:32 pm, Britt <britt.snodgr...@gmail.com> wrote:
> There are several things that can cause the visibility error message
> you are seeing. Have you created an index file (using sparkmake) that
> tells the Examiner where to find each of the source files? You will
> need to pass the index file to the Examiner with the /index_file
> switch.
>
> - Britt

Yes, I have an index file and it is passed with the index_file
switch.  I don't think that is the problem since the examiner
apparently thinks Std_IO.Put_Line is visible, which is also declared
in the same file ...

But thanks for the reply.

Laurie

Re: SPARK examiner visibility problem

[Ludovic Brenta]

Laurie Dillon wrote on comp.lang.ada:
> 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.

From a past discussion here on comp.lang.ada, I vaguely remember that
#hide annotations must be in the spec, not in the body, to take
effect.

--
Ludovic Brenta.

Re: SPARK examiner visibility problem

[Phil Thornley]

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

Re: SPARK examiner visibility problem

[Phil Thornley]

On 14 Sep, 07:28, Ludovic Brenta <ludo...@ludovic-brenta.org> wrote:
> Laurie Dillon wrote on comp.lang.ada:
>
> > 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.
>
> From a past discussion here on comp.lang.ada, I vaguely remember that
> #hide annotations must be in the spec, not in the body, to take
> effect.
>
> --
> Ludovic Brenta.

You can hide any of:
1. the private part of a spec (not the visible part)
   the --# hide follows the 'private' keyword

2. a package body (all of it)
   the --# hide follows the 'is' keyword.

3. a subprogram body
   ditto

4. the initialisation part of a package body
   the --# hide follows the 'begin' keyword.

Cheers,

Phil

Re: SPARK examiner visibility problem

[Phil Thornley]

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

Re: SPARK examiner visibility problem

[Laurie Dillon]

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 :(