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.211.195 with SMTP id ne3mr294708pbc.2.1326412812647; Thu, 12 Jan 2012 16:00:12 -0800 (PST) MIME-Version: 1.0 Path: lh20ni175482pbb.0!nntp.google.com!news2.google.com!goblin2!goblin.stu.neva.ru!multikabel.net!newsfeed20.multikabel.net!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: Thu, 12 Jan 2012 18:00:05 -0600 Organization: Jacob Sparre Andersen Research & Innovation Message-ID: References: <1d74a186-2599-4de5-af49-ffca2529ea96@do4g2000vbb.googlegroups.com> NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net X-Trace: munin.nbi.dk 1326412810 3563 69.95.181.76 (13 Jan 2012 00:00:10 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Fri, 13 Jan 2012 00:00:10 +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-12T18:00:05-06:00 List-Id: "Martin" wrote in message news:1d74a186-2599-4de5-af49-ffca2529ea96@do4g2000vbb.googlegroups.com... > Now Ada has bitten the bullet and allowed "in out" mode parameters in > functions, is it time to allow users to contract the other extreme and > allow a function to be declared Pure (no state changes, not even > hidden ones)? e.g. > > package P is > type T is tagged private; > function Pure_F (Self : T) return Integer > with Pure; > function Impure_F (Self : T) return Integer; > private > type T is tagged record > I : Integer := 0; > end record; > end P; > > > Functions with a Pure contract would be allowed to call other > functions with pure contracts, read values/parameters but promise to > change nothing (not even via 'tricks' a la random number generator!!). We've argued this for a long time within the ARG, and we haven't been able to get a real consensus. This discussion goes back to Ada 79 (which is even before I got involved in Ada) -- early drafts of Ada had both functions (which were what we now call pure) and value-returning procedures (which were not). The concern was that there was not a clear line between them, and moreover there are many sorts of functions that are "logically" pure but still do change things (the "memo function" being the banner carrier for that idea). Personally, I would be happy to have strong checks on such functions, and I don't much care about what gets left out (it's not that important, and any such functions are not task-safe anyway, so it is already a good idea to avoid them in Ada code). But not everyone agrees. We just had another version of this discussion in Denver; we ended up adopting an undetectable bounded error for this case (in the case of assertions, including preconditions, et. al.). I had tried an alternative approach for Ada 2012, by suggesting the addition of checked global in/out contracts to subprograms. Eventually, this was dropped from Ada 2012 as being insufficiently mature. My understanding is that AdaCore is experimenting with a version of it in their formal methods research, so it isn't necessarily gone forever (which is good, considering the amount of time I put in on it). You can see the last proposal at http://www.ada-auth.org/cgi-bin/cvsweb.cgi/ai05s/ai05-0186-1.txt. Randy.