* Q: SPARK: visibility of private child in parent's body
@ 2013-08-25 13:06 Georg Bauhaus
2013-08-25 19:35 ` Phil Thornley
0 siblings, 1 reply; 3+ messages in thread
From: Georg Bauhaus @ 2013-08-25 13:06 UTC (permalink / raw)
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;
^ permalink raw reply [flat|nested] 3+ messages in thread
* Re: Q: SPARK: visibility of private child in parent's body
2013-08-25 13:06 Q: SPARK: visibility of private child in parent's body Georg Bauhaus
@ 2013-08-25 19:35 ` Phil Thornley
2013-08-25 22:00 ` Georg Bauhaus
0 siblings, 1 reply; 3+ messages in thread
From: Phil Thornley @ 2013-08-25 19:35 UTC (permalink / raw)
In article <521a0149$0$9514$9b4e6d93@newsspool1.arcor-online.net>,
rm.dash-bauhaus@futureapps.de says...
>
> 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)?
>
>
This code works OK for me (with the "P." prefixes removed from within
the body of P) with both the last standalone SPARK (2012) and the HiLite
version (downloaded 2013-06-07).
Assuming you are using separate files for each unit, the next place I
would look would be the index file. Does this identify the files that
you think it does, and does it contain the private child announcement
for P.C:
P components are P.C
Cheers,
Phil
^ permalink raw reply [flat|nested] 3+ messages in thread
* Re: Q: SPARK: visibility of private child in parent's body
2013-08-25 19:35 ` Phil Thornley
@ 2013-08-25 22:00 ` Georg Bauhaus
0 siblings, 0 replies; 3+ messages in thread
From: Georg Bauhaus @ 2013-08-25 22:00 UTC (permalink / raw)
On 25.08.13 21:35, Phil Thornley wrote:
> Assuming you are using separate files for each unit, the next place I
> would look would be the index file. Does this identify the files that
> you think it does, and does it contain the private child announcement
> for P.C:
> P components are P.C
Adding the component entry to the index file fixed it (after
removing the P prefixes in the body). Thanks!
^ permalink raw reply [flat|nested] 3+ messages in thread
end of thread, other threads:[~2013-08-25 22:00 UTC | newest]
Thread overview: 3+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2013-08-25 13:06 Q: SPARK: visibility of private child in parent's body Georg Bauhaus
2013-08-25 19:35 ` Phil Thornley
2013-08-25 22:00 ` Georg Bauhaus
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox