From: anon@att.net
Subject: Re: Ada2012 Invariants and obaque types
Date: Thu, 23 Jun 2011 16:21:03 +0000 (UTC)
Date: 2011-06-23T16:21:03+00:00 [thread overview]
Message-ID: <itvp5e$apu$1@speranza.aioe.org> (raw)
In-Reply-To: 239a78ad-0937-4a7a-8163-231430fd5ffe@k27g2000yqn.googlegroups.com
package P1 is
type T1 is tagged private
with Invariant => Is_Valid ( T1 ) ;
function Create return T1 ;
function Is_Valid ( This : T1 ) return Boolean ;
private
type Imp ; -- ???? Where is the completed type definition of "Imp"
-- Another thing the syntax for Aspect Types may require
-- that "Imp" be defined before T1, so "Imp" may be
-- required in this example to be public.
type T1 is tagged record -- ???? You forgot the keyword "tagged"
I : Imp ;
end record ;
end P1 ;
An Example of one that might work is from sem_ch13.ads
package AspectVis is
R_Size : constant Integer := 32;
package Inner is
type R is new Integer with
Size => R_Size;
F : R; -- freezes
R_Size : constant Integer := 64;
S : constant Integer := R'Size; -- 32 not 64
end Inner;
end AspectVis;
Check file Aspects.ads for a list of Aspects like "Invariant"
In <239a78ad-0937-4a7a-8163-231430fd5ffe@k27g2000yqn.googlegroups.com>, Martin <martin.dowie@btopenworld.com> writes:
>A fairly common Ada idiom is to define the full view of a private type
>using an incomplete declaration. Thus leaving the actual
>implementation to the package spec. Trying this out with the public
>view defined with an invariant lead to a compiler error - is this:
>
>a) expected?
>b) an unexpected consequence? or
>c) a compiler bug?
>
>Example:
>package P1 is
> type T1 is tagged private
> with Invariant => Is_Valid (T1);
> function Create return T1;
> function Is_Valid (This : T1) return Boolean;
>private
> type Imp;
> type T1 is
> record
> I : Imp;
> end record;
>end P1;
>
>gnatmake -ws -c -u -PH:\Ada\test_invariants\test_invariants.gpr p1.ads
>gcc -c -g -g -gnatE -gnatVn -gnato -fstack-check -gnat12 -gnatf -I- -
>gnatA H:\Ada\test_invariants\src\p1.ads
>p1.ads:11:04: type "Imp" is frozen at line 3 before its full
>declaration
>p1.ads:13:09: full declaration of private type "T1" defined at line 3
>must be a tagged type
>p1.ads:15:14: invalid use of type before its full declaration
>gnatmake: "H:\Ada\test_invariants\src\p1.ads" compilation error
>
>[2011-06-21 09:46:55] process exited with status 4 (elapsed time:
>00.26s)
prev parent reply other threads:[~2011-06-23 16:21 UTC|newest]
Thread overview: 31+ messages / expand[flat|nested] mbox.gz Atom feed top
2011-06-21 8:53 Ada2012 Invariants and obaque types Martin
2011-06-21 10:27 ` Yannick Duchêne (Hibou57)
2011-06-21 10:36 ` Martin
2011-06-21 10:46 ` Martin
2011-06-21 18:42 ` Yannick Duchêne (Hibou57)
2011-06-21 10:43 ` Ludovic Brenta
2011-06-21 10:53 ` Martin
2011-06-21 11:14 ` Martin
2011-06-21 11:31 ` Robert A Duff
2011-06-21 11:48 ` Martin
2011-06-21 12:01 ` Martin
2011-06-21 12:13 ` Robert A Duff
2011-06-21 12:22 ` Martin
2011-06-21 12:54 ` Robert A Duff
2011-06-21 13:00 ` Martin
2011-06-21 12:08 ` Dmitry A. Kazakov
2011-06-21 12:17 ` Georg Bauhaus
2011-06-21 12:31 ` Dmitry A. Kazakov
2011-06-21 13:29 ` Georg Bauhaus
2011-06-21 14:42 ` Dmitry A. Kazakov
2011-06-21 18:37 ` Yannick Duchêne (Hibou57)
2011-06-21 18:53 ` Dmitry A. Kazakov
2011-06-21 19:34 ` Vinzent Hoefler
2011-06-21 20:52 ` Dmitry A. Kazakov
2011-06-21 21:50 ` Vinzent Hoefler
2011-06-22 7:55 ` Dmitry A. Kazakov
2011-06-21 21:18 ` Manuel Collado
2011-06-22 8:00 ` Dmitry A. Kazakov
2011-06-22 10:39 ` Egil Høvik
2011-06-22 13:57 ` Martin
2011-06-23 16:21 ` anon [this message]
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox