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=ham autolearn_force=no version=3.4.4 X-Google-Thread: a07f3367d7,146d9a693430fff2 X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,ASCII Path: g2news1.google.com!postnews.google.com!o4g2000vbv.googlegroups.com!not-for-mail From: Martin Newsgroups: comp.lang.ada Subject: Re: Ada2012 Invariants and obaque types Date: Tue, 21 Jun 2011 03:53:35 -0700 (PDT) Organization: http://groups.google.com Message-ID: <381cb069-104e-4684-9817-a307e2b96ff3@o4g2000vbv.googlegroups.com> References: <239a78ad-0937-4a7a-8163-231430fd5ffe@k27g2000yqn.googlegroups.com> NNTP-Posting-Host: 20.133.0.8 Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Trace: posting.google.com 1308654055 17327 127.0.0.1 (21 Jun 2011 11:00:55 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Tue, 21 Jun 2011 11:00:55 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: o4g2000vbv.googlegroups.com; posting-host=20.133.0.8; posting-account=g4n69woAAACHKbpceNrvOhHWViIbdQ9G User-Agent: G2/1.0 X-Google-Web-Client: true X-Google-Header-Order: HUALESRCNK X-HTTP-UserAgent: Mozilla/5.0 (Windows NT 5.1; rv:5.0) Gecko/20100101 Firefox/5.0,gzip(gfe) Xref: g2news1.google.com comp.lang.ada:19973 Date: 2011-06-21T03:53:35-07:00 List-Id: On Jun 21, 11:43=A0am, Ludovic Brenta wrote: > Martin Dowie wrote on comp.lang.ada: > > > > > > > > > > > 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 > > =A0 =A0type T1 is tagged private > > =A0 =A0 =A0 with Invariant =3D> Is_Valid (T1); > > =A0 =A0function Create =A0 =A0 =A0 =A0 =A0 =A0 =A0 return T1; > > =A0 =A0function Is_Valid (This : T1) return Boolean; > > private > > =A0 =A0type Imp; > > =A0 =A0type T1 is > > =A0 =A0 =A0 record > > =A0 =A0 =A0 =A0 =A0I : Imp; > > =A0 =A0 =A0 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) > > This looks like a consequence of 13.14(8.2/1): "If an expression is > implicitly converted to a type or subtype T, then at the place where > the expression causes freezing, T is frozen." (where in this case the > expression is T1, which stands for the current instance of the type, > and the type T is also T1). > > This subclause however seems to contradict 13.14(7.2/3): "At the > freezing point of the entity associated with an aspect_specification, > any expressions or names within the aspect_specification cause > freezing."; this subclause would defer the freezing point of T1 until > the end of the enclosing package spec or the declaration of a constant > of the type, whichever comes first (as is normal for tagged types). > > Another possible interpretation is that Is_Valid must be called as > part of the elaboration of type T1, in which case the > aspect_specification is a function call, which freezes the types of > its parameters (per 13.14(10.1/3)). =A0But I doubt this is true. > > So, this looks like an area of the language definition that needs > clarifying (but then again, freezing rules have always been difficult > to understand). The behavior of the compiler definitely looks > undesirable to me. =A0So I vote for b) an unexpected (and undesirable) > consequence (of existing rules). > > -- > Ludovic Brenta. Ok, thanks for that Ludovic...maybe need to post this one to ada- auth... -- Martin