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,39579ad87542da0e X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,ASCII-7-bit X-Received: by 10.66.197.229 with SMTP id ix5mr702254pac.23.1368584010579; Tue, 14 May 2013 19:13:30 -0700 (PDT) Path: bp1ni2274pbd.1!nntp.google.com!npeer03.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!border3.nntp.dca.giganews.com!border1.nntp.dca.giganews.com!border4.nntp.dca.giganews.com!border2.nntp.dca.giganews.com!nntp.giganews.com!newsfeed.news.ucla.edu!nrc-news.nrc.ca!News.Dal.Ca!news.litech.org!news0.firedrake.org!fu-berlin.de!uni-berlin.de!individual.net!not-for-mail From: Niklas Holsti Newsgroups: comp.lang.ada Subject: Re: Seeking for papers about tagged types vs access to subprograms Date: Sun, 12 May 2013 09:09:01 +0300 Organization: Tidorum Ltd Message-ID: References: <17ceq51ydy3s0.s94miqqzbg5w.dlg@40tude.net> <1vrhb7oc4qbob$.q02vuouyovp5$.dlg@40tude.net> <19lrzzbgm77v6.1dzpgqckptaj6.dlg@40tude.net> <1bfhq7jo34xpi.p8n2vq6yjsea.dlg@40tude.net> <12gn9wvv1gwfk.10ikfju4rzmnj.dlg@40tude.net> <6416a096-def9-4a95-a4e0-7ba6a4ece524@googlegroups.com> Mime-Version: 1.0 X-Trace: individual.net d92xbCO9SyiQIPiVmsvklQMFQwlpHzWiSk+GZConISQXySsJIX Cancel-Lock: sha1:tgx56qHk05Y+wg+Z2DOLULzCj98= User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:17.0) Gecko/20130328 Thunderbird/17.0.5 In-Reply-To: <6416a096-def9-4a95-a4e0-7ba6a4ece524@googlegroups.com> X-Received-Bytes: 6288 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Date: 2013-05-12T09:09:01+03:00 List-Id: On 13-05-12 02:19 , Shark8 wrote: > 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: When you declare an "in out" parameter, Ada now requires that you specify the same subtype for both roles. In the example, if the File parameter to Open is declared as "in out Closed_File", but Open tries to change the parameter to (State => Is_Open, Handle => ...) a Constraint_Error results at run-time. > 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; (I think you mean "procedure Open" there, not "Read".) As I said, it can be expressed with pre- and post-conditions in this way, but then the parameter profile does not mention the subtypes and instead uses the unconstrained type (here File_Object). As I also said, I wanted the subtype changes to be visible in the subprogram profile, to show more clearly (or at least, more traditionally) how the availability of the subprogram depends on the state (i.e. the subtype) of the parameter, and how it affects the state. To condense my points: 1. The typestate concept, as implemented in the Plaid language, seems (after my brief study of Plaid) to be implementable in Ada through discriminated records with variants. 2. The influence of the current typestate of an object, on the set of subprograms (operations) available for the object, can be represented as constraints on the "in" subtype of the object, and the typestate changes can be represented as the "out" subtype. In current Ada, of course, the subtype checks in principle occur at run-time, so typestate correctness is not checked at compile-time. Moreover, current Ada does not allow the formal subtype (as written in the profile) to be different for the "in" and "out" roles. 3. Those different "in" and "out" constraints can be implemented in Ada 2012 as pre/post-conditions, as you say. 4. A closer match to Plaid can be achieved if Ada is extended to allow different subtypes for the "in" and "out" roles of an "in out" parameter. As the pre/post-condition feature of Ada 2012 becomes more familiar, perhaps the pre- and post-conditions will be seen as a more integrated part of the subprogram's profile, and there is no reason to consider changes to the formal subtypes allowed in the language (point 4). On the other hand, it seems to me that there are other cases, not perhaps related to typestate, where it would be natural to specify different "in" and "out" subtypes for an "in out" parameter. Something as simple as: procedure Increment (Counter : in out Natural) could become -- Extended Ada: procedure Increment ( Counter : in Natural range 0 .. Natural'Last - 1 out Positive); Of course, all such different in/out constraints can be expressed using the "heavy guns" of pre/post-conditions, so perhaps this suggestion is out of date after Ada 2012. Any compiler powerful enough to do useful typestate analysis based on the formal parameter subtypes is probably able to do the same analysis using the corresponding pre/post-conditions, at least when the conditions take the simple form "parameter in subtype". It is interesting that Randy thinks his ideas regarding a future replacement for Ada resemble the typestate concept, but that the typestate concept as implemented in Plaid seems to be implementable in Ada 2012. Perhaps Randy's ideas go much further than this, however. -- Niklas Holsti Tidorum Ltd niklas holsti tidorum fi . @ .