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-7-bit
Path: 
 g2news1.google.com!news2.google.com!border1.nntp.dca.giganews.com!nntp.giganews.com!novia!news-out.readnews.com!transit3.readnews.com!panix!newsfeed-00.mathworks.com!nntp.TheWorld.com!not-for-mail
From: Robert A Duff <bobduff@shell01.TheWorld.com>
Newsgroups: comp.lang.ada
Subject: Re: Ada2012 Invariants and obaque types
Date: Tue, 21 Jun 2011 07:31:10 -0400
Organization: The World Public Access UNIX, Brookline, MA
Message-ID: <wccmxhbv2td.fsf@shell01.TheWorld.com>
References: 
 <239a78ad-0937-4a7a-8163-231430fd5ffe@k27g2000yqn.googlegroups.com>
NNTP-Posting-Host: shell01.theworld.com
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii
X-Trace: pcls6.std.com 1308655870 9772 192.74.137.71 (21 Jun 2011 11:31:10
 GMT)
X-Complaints-To: abuse@TheWorld.com
NNTP-Posting-Date: Tue, 21 Jun 2011 11:31:10 +0000 (UTC)
User-Agent: Gnus/5.1008 (Gnus v5.10.8) Emacs/21.3 (irix)
Cancel-Lock: sha1:3IzBTisrs0KMpxFL1eStapseweA=
Xref: g2news1.google.com comp.lang.ada:19974
Date: 2011-06-21T07:31:10-04:00
List-Id: <comp.lang.ada>

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.

Body?

>...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;

This has nothing to do with invariants.  Incomplete types can only
be used in very restricted ways.  Not as components.  You need to
use an access type.

This dates back to Ada 83 -- it's always been illegal, and still is.

When compiling clients of P1 that declare objects of type T1,
how would the compiler know the size?  It could treat it as
dynamic, or it could take a peek at the body, but if either of
those was the intended compilation model, then there would be no
need for private parts in the first place -- we'd put the completion
of a private type in the body, where it belongs.

I suggest you erase the invariant, fix the errors, and then put the
invariant back in.  There's nothing wrong with your invariant.

- Bob