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 X-Received: by 10.224.59.205 with SMTP id m13mr21044199qah.7.1368534028897; Tue, 14 May 2013 05:20:28 -0700 (PDT) Path: y6ni42402qax.0!nntp.google.com!border1.nntp.dca.giganews.com!nntp.giganews.com!news-in-01.newsfeed.easynews.com!easynews.com!easynews!news-out.news.tds.net!news.ripco.com!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 00:06:25 +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> Mime-Version: 1.0 X-Trace: individual.net /wk8tea78u/gsJq7aUzqUAInkkeSR8yHYerk8kfBgMhyGQ6Z5E Cancel-Lock: sha1:fvt61gSGy5QtyrNSVjFwgENOvPo= User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:17.0) Gecko/20130328 Thunderbird/17.0.5 In-Reply-To: X-Received-Bytes: 6932 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit Date: 2013-05-12T00:06:25+03:00 List-Id: On 13-05-11 03:18 , Randy Brukardt wrote: > "Niklas Holsti" wrote in message > news:av4r5qFitfiU1@mid.individual.net... >> On 13-05-10 06:29 , Yannick Duch�ne (Hibou57) wrote: >>> Le Fri, 10 May 2013 00:19:14 +0200, Randy Brukardt >> ... >>>> Yes, because we need to move beyond typing to other forms of static >>>> error >>>> detection. Typing is too rigid to do a good job -- you need to include >>>> statically known information about the contents of variables and >>>> parameters, >>>> which can change from line-to-line in a program. >>> >>> I feel the same. I often though typing can't do everything if it comes >>> with value type checking, while in some occasions, I tried to express >>> each validity condition with types and then type checking (that ends to >>> be crazy, indeed). A simple example, is paired invocation, where >>> whenever a sub-program is is invoked, sooner or later, another >>> sub-program must be invoked too on the same argument, ex. like `Open` >>> and later `Close`. This cannot be expressed with types and indeed >>> requires assertions. >> >> Are you familiar with the "typestate" concept? As I understand it, the >> intent is to check state-sequence rules such as Open-followed-by-Close. >> See http://en.wikipedia.org/wiki/Typestate_analysis. > > Thanks for the reference. I doubted that the idea was new (there are no new > ideas), but I hadn't heard of it before. I'm not sure if "typestate" matches all of what you were describing or thinking of -- I meant it only as a pointer to Yannick for things like the Open-Close protocol example. But if it resonates with your thinking, good. > I don't like the name much, because > it feeds into the "type is everything" madness that Dmitry exhibits so > clearly. This clearly (just like constraints and predicates) is something > that's added in addition to type analysis; it's not part of it at all. I haven't studied typestate analysis at all deeply. I had a look at the "Plaid" language referenced from the Wikipedia article, at http://www.cs.cmu.edu/~aldrich/plaid/, and was a bit surprised to understand that Ada subtypes come rather close to it, in particular subtypes of discriminated record types with variants. The value of the discriminant represents the state, with certain components of the record (= attributes of the object or type) existing or not existing depending on the variant selected by the discriminant. For the Open-Close example: 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 ); By using subtypes on formal parameters, we can indicate that the available operations on a File_Object depend on the actual subtype (i.e. the state), except for one deficiency, on which more below. First, reading and writing is possible only for open files: procedure Read (File : in Open_File; ...) procedure Write (File : in Open_File; ...) Second, a Closed file can be Opened, and an Open file can be Closed: procedure Open (File : in out Closed_File); procedure Close (File : in out Open_File ); The problem here is that these operations should change the subtype of the "in out" parameter: Open changes the File from Closed_File to Open_File, and Close changes it from Open_File to Closed_File. However, Ada does not let us specify such changes, in the subprogram profile. (This can of course be specified with pre- and post-conditions, but I'm looking for a closer connection between the subprogram profile and the subtypes.) 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. So let us extend Ada to allow different "in" and "out" subtypes: -- Extended Ada: procedure Open (File : in Closed_File out Open_File ; ...); procedure Close (File : in Open_File out Closed_File; ...); This gives us exactly the open/close typestate example. A compiler with strong value-range analysis should then be able to deduce, for example, that the "in" constraint check on a particular call of Open, Close, Read, or Write always succeeds (= typestate correctness) or may or must fail (various degrees of typestate incorrectness). I believe that many current compilers could do such value-range analysis, and thus Ada could support this kind of typestate concept with rather small language changes. (You may ask: if an "in out" parameter has different "in" and "out" subtypes, what subtype is applied when the formal parameter is used or assigned within the subprogram body? I think the logical answer would be the "disjunctive subtype" that represents the union of the "in" and "out" subtypes, which unfortunately could be a subtype with "holes". But I think that would be manageable, since this disjunctive subtype would have at most two separate components, i.e. at most one hole.) -- Niklas Holsti Tidorum Ltd niklas holsti tidorum fi . @ .