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,UTF8 X-Received: by 10.66.122.39 with SMTP id lp7mr5415789pab.44.1368583682463; Tue, 14 May 2013 19:08:02 -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!news.etla.org!aioe.org!.POSTED!not-for-mail From: =?utf-8?Q?Yannick_Duch=C3=AAne_=28Hibou57?= =?utf-8?Q?=29?= Newsgroups: comp.lang.ada Subject: Re: Seeking for papers about tagged types vs access to subprograms Date: Fri, 10 May 2013 21:33:32 +0200 Organization: Ada @ Home 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> NNTP-Posting-Host: uGUognJZXpdb++Da0QvCqg.user.speranza.aioe.org Mime-Version: 1.0 X-Complaints-To: abuse@aioe.org User-Agent: Opera Mail/12.15 (Linux) X-Notice: Filtered by postfilter v. 0.8.2 X-Received-Bytes: 4178 Content-Type: text/plain; charset=utf-8; format=flowed; delsp=yes Content-Transfer-Encoding: Quoted-Printable Date: 2013-05-10T21:33:32+02:00 List-Id: Le Fri, 10 May 2013 20:04:42 +0200, Niklas Holsti = a =C3=A9crit: > 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. I did not knew it before. Thanks for the pointer, that's always good to = = know the name of things (may be interesting to see if it's related to = temporal logic). Just for the anecdote, the way I tried to solve it with static check, wa= s = using typed tokens, returned and/or required by operations. Say an = operation B is allowed to occur only if an operation A occurred before. = = The operation A returns a value of type TA. As B requires to occurs only= = after A, then it can requires a token of type TA as its input arguments.= = Similarly, B may return a token of type TB, which may be required by any= = operation which must occur only after B. To be trustable, it requires TA, TB and so on, cannot be created out of = = control of A, B an so on, so it must be limited types with unknown = discriminant (the latter to force initialization). Well, that looks a nice hack, it's statically checked, but that's limite= d = and bloats everything, and near to be unusable due to the required = initialisation (imagine writing a program all in the declarative part). = = Then, no way to tell B must always occur later after A if ever A occurre= d. = It also only know about simple sequence, and can't differentiate between= = A;B;C and A;C. It can't differentiate neither between instances (there i= s = no way to check a token was return by an operation on this or that = instance). So finally, I gave up with this hack. That's what I was thinking about, when I said it can indeed become crazy= = to try to express all validity rules using the type system. There is another less restrictive way to do, except it cannot statically= = check, which ends to be the same as pre/post, and that's finally better = to = just use pre/post in this case (at that time, Ada 2012 was not there). -- = =E2=80=9CSyntactic sugar causes cancer of the semi-colons.=E2=80=9D [1] =E2=80=9CStructured Programming supports the law of the excluded muddle.= =E2=80=9D [1] [1]: Epigrams on Programming =E2=80=94 Alan J. =E2=80=94 P. Yale Univers= ity