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: 103376,1e369abf7da96fac X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Received: by 10.68.213.68 with SMTP id nq4mr26350pbc.2.1326935870853; Wed, 18 Jan 2012 17:17:50 -0800 (PST) MIME-Version: 1.0 Path: lh20ni197964pbb.0!nntp.google.com!news1.google.com!eweka.nl!feeder.eweka.nl!62.179.104.142.MISMATCH!amsnews11.chello.com!nuzba.szn.dk!news.jacob-sparre.dk!pnx.dk!jacob-sparre.dk!ada-dk.org!.POSTED!not-for-mail From: "Randy Brukardt" Newsgroups: comp.lang.ada Subject: Re: Pure function aspect?... Date: Wed, 18 Jan 2012 19:17:45 -0600 Organization: Jacob Sparre Andersen Research & Innovation Message-ID: References: <1d74a186-2599-4de5-af49-ffca2529ea96@do4g2000vbb.googlegroups.com> <9f0669ff-6cb9-4936-9a05-655867639fed@hs8g2000vbb.googlegroups.com> NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net X-Trace: munin.nbi.dk 1326935869 26379 69.95.181.76 (19 Jan 2012 01:17:49 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Thu, 19 Jan 2012 01:17:49 +0000 (UTC) X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2900.5931 X-RFC2646: Format=Flowed; Original X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157 Date: 2012-01-18T19:17:45-06:00 List-Id: "Martin" wrote in message news:9f0669ff-6cb9-4936-9a05-655867639fed@hs8g2000vbb.googlegroups.com... On Jan 14, 12:00 am, "Randy Brukardt" wrote: > wrote in message ... >> There has been strong opposition to a "checked" pure function declaration >> (I >> had floated that first, and it went nowhere), and global in out => null >> is >> essentially the same thing. The reason is the "memo function" idea (more >> sensibly, a function that logs its calls but is otherwise pure) is not >> allowed. I was trying to do something broader that could get more >> support. > >You mean people want a method of saying "these state changing calls >are unimportant"? Something on that line. The global in/out proposal handling that in terms of allowing the specification of what state is modified. If that state doesn't conflict with other routines, then optimization is still possible. But one of the important points is that side-effects really ought to prevent optimization (and assumptions) unless the compiler (or proof tool) can actually prove they don't matter. A call that is being logged, for instance, probably shouldn't be eliminated even if the results are the same (because you couldn't easily relate the actual calls to the source code). One can argue the other side of this, too, and it's obvious there are no easy answers. In which case I prefer to stay as close to the "canonical" semantics as possible. ... >> The lack in global in out isn't a deal breaker for Ada 2012, simply >> because >> it is also missing exception contracts. > >Something like: > > function Foo (P1 : Integer) > return Integer or raise Program_Error or My_Defined_Error; > >? Getting a bit long winded but I guess you just need all that sort of >information. Well, clearly it would be an aspect (like the other contracts), and each exception ought to be able to have an optional postcondition as well (which defines when the exception might be raised). So more like: function Foo (P1 : Integer) return Integer when Pre => ... Post => ... Raises => Program_Error, Storage_Error, My_Defined_Error when P1 not in Even, Global in => null, Global out => null; The exception contract would require that the compiler prove that Constraint_Error and Tasking_Error are not propagated. (The same would be true for Storage_Error, but that would be impossible for the vast majority of compilers). I'm also proposing a way to name a group of exceptions, so you wouldn't have to write huge sets repeatedly. (All of the exceptions in package IO_Exceptions could be named "IO_Exceptions" so it wouldn't be necessary to write about them individually.) I of course have no idea how far any of this will get, it won't be taken up for a while and won't be standardized for years, and in any case, it is all optional. No one is going to be required to have complete contracts (I suspect that will be going too far). Randy.