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!c26g2000vbq.googlegroups.com!not-for-mail From: Ludovic Brenta Newsgroups: comp.lang.ada Subject: Re: Ada2012 Invariants and obaque types Date: Tue, 21 Jun 2011 03:43:24 -0700 (PDT) Organization: http://groups.google.com Message-ID: References: <239a78ad-0937-4a7a-8163-231430fd5ffe@k27g2000yqn.googlegroups.com> NNTP-Posting-Host: 153.98.68.197 Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Trace: posting.google.com 1308653005 7405 127.0.0.1 (21 Jun 2011 10:43:25 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Tue, 21 Jun 2011 10:43:25 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: c26g2000vbq.googlegroups.com; posting-host=153.98.68.197; posting-account=pcLQNgkAAAD9TrXkhkIgiY6-MDtJjIlC User-Agent: G2/1.0 X-Google-Web-Client: true X-Google-Header-Order: HUALESRCNK X-HTTP-UserAgent: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:1.9.0.6) Gecko/2009012111 Red Hat/3.0.6-1.el5 Firefox/3.0.6,gzip(gfe) Xref: g2news1.google.com comp.lang.ada:19971 Date: 2011-06-21T03:43:24-07:00 List-Id: 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)). But 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. So I vote for b) an unexpected (and undesirable) consequence (of existing rules). -- Ludovic Brenta.