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 Received: by 10.68.197.100 with SMTP id it4mr556466pbc.5.1326452507564; Fri, 13 Jan 2012 03:01:47 -0800 (PST) Path: lh20ni177152pbb.0!nntp.google.com!news2.google.com!postnews.google.com!m20g2000vbf.googlegroups.com!not-for-mail From: Martin Newsgroups: comp.lang.ada Subject: Re: Pure function aspect?... Date: Fri, 13 Jan 2012 02:55:04 -0800 (PST) Organization: http://groups.google.com Message-ID: References: <1d74a186-2599-4de5-af49-ffca2529ea96@do4g2000vbb.googlegroups.com> NNTP-Posting-Host: 20.133.0.8 Mime-Version: 1.0 X-Trace: posting.google.com 1326452507 10814 127.0.0.1 (13 Jan 2012 11:01:47 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Fri, 13 Jan 2012 11:01:47 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: m20g2000vbf.googlegroups.com; posting-host=20.133.0.8; posting-account=g4n69woAAACHKbpceNrvOhHWViIbdQ9G User-Agent: G2/1.0 X-Google-Web-Client: true X-Google-Header-Order: HUALERCFNK X-HTTP-UserAgent: Mozilla/5.0 (Windows NT 5.1; rv:10.0) Gecko/20100101 Firefox/10.0,gzip(gfe) Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Date: 2012-01-13T02:55:04-08:00 List-Id: On Jan 13, 12:00=A0am, "Randy Brukardt" wrote: > "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 > > =A0 type T is tagged private; > > =A0 function Pure_F =A0 (Self : T) return Integer > > =A0 =A0 =A0with Pure; > > =A0 function Impure_F (Self : T) return Integer; > > private > > =A0 type T is tagged record > > =A0 =A0 =A0I : Integer :=3D 0; > > =A0 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 abl= e > to get a real consensus. This discussion goes back to Ada 79 (which is ev= en > 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 an= y > 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 undetectabl= e > 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 addit= ion > 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 method= s > research, so it isn't necessarily gone forever (which is good, considerin= g > the amount of time I put in on it). You can see the last proposal athttp:= //www.ada-auth.org/cgi-bin/cvsweb.cgi/ai05s/ai05-0186-1.txt. > > =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 = =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0Randy. Interesting...to my untrained-in-SPARK eye, it looks a little SPARK- ish! :-) How would that work together with "limited with"? I'm thinking of times when I have mutually dependent packages (hence the limited withs!) _and_ functions that 'tamper' with objects in the other package. If you have mutually dependent packages, I would have thought it was almost guaranteed that each would 'tamper' with the other! -- Martin -- Martin