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,FREEMAIL_FROM
	autolearn=ham autolearn_force=no version=3.4.4
X-Google-Thread: a07f3367d7,39579ad87542da0e
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII-7-bit
X-Received: by 10.224.10.6 with SMTP id n6mr15354564qan.4.1368314347422;
        Sat, 11 May 2013 16:19:07 -0700 (PDT)
X-Received: by 10.50.50.138 with SMTP id c10mr945987igo.5.1368314347205; Sat,
 11 May 2013 16:19:07 -0700 (PDT)
Path: 
 y6ni29564qax.0!nntp.google.com!m7no4876222qam.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Sat, 11 May 2013 16:19:06 -0700 (PDT)
In-Reply-To: <av7q6hF8evqU1@mid.individual.net>
Complaints-To: groups-abuse@google.com
Injection-Info: glegroupsg2000goo.googlegroups.com;
 posting-host=69.20.190.126;
 posting-account=lJ3JNwoAAAAQfH3VV9vttJLkThaxtTfC
NNTP-Posting-Host: 69.20.190.126
References: <op.wv8jh1c1ule2fv@cardamome> <op.wwnp2zkrule2fv@cardamome>
 <u3jaslg5kca7.1gk5ds3d4sx2y$.dlg@40tude.net> <op.wwnsmtteule2fv@cardamome>
 <17ceq51ydy3s0.s94miqqzbg5w.dlg@40tude.net> <op.wwny5jerule2fv@cardamome>
 <1vrhb7oc4qbob$.q02vuouyovp5$.dlg@40tude.net> <op.wwn4oak8ule2fv@cardamome>
 <19lrzzbgm77v6.1dzpgqckptaj6.dlg@40tude.net> <kmbohm$elb$1@loke.gir.dk>
 <p0pf97g5w6xg.jhca6ztjwpde$.dlg@40tude.net> <op.wwq9s4l6ule2fv@cardamome>
 <1bfhq7jo34xpi.p8n2vq6yjsea.dlg@40tude.net> <op.wwrefx1pule2fv@cardamome>
 <cps71yzogw24$.7ol98fxcaurj$.dlg@40tude.net> <op.wwriky0dule2fv@cardamome>
 <nd22gfeezrwf$.tlj4yyygrwq3$.dlg@40tude.net> <kmecg6$et4$1@loke.gir.dk>
 <12gn9wvv1gwfk.10ikfju4rzmnj.dlg@40tude.net> <kmh7d4$up3$1@loke.gir.dk>
 <op.wwumn3r2ule2fv@cardamome> <av4r5qFitfiU1@mid.individual.net>
 <kmk2on$tij$1@loke.gir.dk> <av7q6hF8evqU1@mid.individual.net>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <6416a096-def9-4a95-a4e0-7ba6a4ece524@googlegroups.com>
Subject: Re: Seeking for papers about tagged types vs access to subprograms
From: Shark8 <onewingedshark@gmail.com>
Injection-Date: Sat, 11 May 2013 23:19:07 +0000
Content-Type: text/plain; charset=ISO-8859-1
Date: 2013-05-11T16:19:06-07:00
List-Id: <comp.lang.ada>

On Saturday, May 11, 2013 3:06:25 PM UTC-6, Niklas Holsti wrote:
>
> Well, why is Ada limited in this way? There is no real reason why an "in
> out" parameter should have the same constraints on input and on output. 

What? Ada's not constrained like that, at least as you're implying:

Given the types you have:
> 
>    type File_State is (Is_Closed, Is_Open);
> 
>    type File_Object (State : File_State := Is_Closed) is
>    record
>       case State is
>       when Is_Closed => null;
>       when Is_Open   => Handle : System.IO.File_Handle;
>       end case;
>    end record;
> 
>    subtype Closed_File is File_Object (State => Is_Closed);
>    subtype Open_File   is File_Object (State => Is_Open  ); 

the proper way to formulate _EXACTLY_ what you want is this:

procedure Read  (File : in out File_Object; ...)
  with pre => File in Closed_File, post => file in Open_File;

Or am I wrong?