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
	autolearn=unavailable autolearn_force=no version=3.4.4
Path: 
 border1.nntp.ams3.giganews.com!border2.nntp.ams3.giganews.com!border2.nntp.ams2.giganews.com!border4.nntp.ams.giganews.com!border2.nntp.ams.giganews.com!nntp.giganews.com!weretis.net!feeder4.news.weretis.net!news.teledata-fn.de!newsfeed.arcor.de!newsspool3.arcor-online.net!news.arcor.de.POSTED!not-for-mail
Date: Sun, 25 Aug 2013 15:06:16 +0200
From: Georg Bauhaus <rm.dash-bauhaus@futureapps.de>
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.7;
 rv:17.0) Gecko/20130801 Thunderbird/17.0.8
MIME-Version: 1.0
Newsgroups: comp.lang.ada
Subject: Q: SPARK: visibility of private child in parent's body
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Message-ID: <521a0149$0$9514$9b4e6d93@newsspool1.arcor-online.net>
Organization: Arcor
NNTP-Posting-Date: 25 Aug 2013 15:06:17 CEST
NNTP-Posting-Host: a47964f1.newsspool1.arcor-online.net
X-Trace: 
 DXC=D@5YBkiBW[D02Sh8E_NfIAic==]BZ:afN4Fo<]lROoRAnkgeX?EC@@@jD]=Ch2TYTBPCY\c7>ejVHWD\@ZD`V7cDD=mkLc^n4@D
X-Complaints-To: usenet-abuse@arcor.de
X-Original-Bytes: 3522
Xref: number.nntp.dca.giganews.com comp.lang.ada:183125
Date: 2013-08-25T15:06:17+02:00
List-Id: <comp.lang.ada>

Hi,

a small hierarchy of packages has the body of parent P refer
to entities of a private child package P.C.  According to
Barnes (1997), this is possible. (I have placed supporting
quotes before the body of P below.)

I'm hitting a wall.

Examiner does not accept the packages, warning that C of P.C
is "either undeclared or not visible at this point".
(There is no --# inherit for P.C, as none is required.)
The Examiner then continues diagnosing semantic errors.

When I rearrange the source by embedding package P.C into the
body of P instead of making it a private child package, then
everything seems fine.

What am I doing wrong?

Can I at all refer to private packages in the parent's body
when using somewhat recent editions of SPARK (2011 and 2012)?



package P
   --# own State;
   --# initializes State;
is

    One: constant := 1;

    procedure Proc (K : in out Natural);
    --# global in State;
    --# derives K from K, State;

end P;

--# inherit P;
private package P.C is

    type Int_1 is range 1 .. P.One;

    procedure Chldproc (X : in out Int_1);
    --# derives X from X;

end P.C;

package body P.C is

    procedure Chldproc (X : in out Int_1) is
    begin
       X := Int_1'Min (1, Int_1'Max (X, X - 1));
    end Chldproc;

end P.C;

-- "a parent can never have an inherit clause for its child. (...) and
-- in the case of a private child although a with clause is allowed on
-- the parent body, nevertheless an inherit clause is not required."
--
-- "An entity T within P.Child has to be referred to as P.Child.T from
-- within the body of P." (Barnes (1997), 7.2)

-- "In addition, a package P can inherit a private child of a package
-- Q only if P is also a private child of Q or a descendant of such a
-- child (or if Q is package Standard)" (SPARK LRM 7.1.1)

with P.C;  -- warning, C undeclared or not visible
package body P
   --# own State is Y;
is

    Y : P.C.Int_1;  -- semantic error 337
    --Y : C.Int_1;  -- semantic error 754

    procedure Proc (K : in out Natural)
       --# global in Y;
       --# derives K from K, Y;
    is
       V : P.C.Int_1;  -- semantic error 337
       --V : C.Int_1;  -- semantic error 754
    begin
       V := P.C.Int_1 (K);
       V := P.C.Int_1'Min (V, Y);
       P.C.Chldproc (V);
       K := Natural (V);
    end Proc;

begin
    Y := 1;
end P;