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.196.130 with SMTP id im2mr7361092pbc.3.1326710909130;
        Mon, 16 Jan 2012 02:48:29 -0800 (PST)
Path: 
 lh20ni188261pbb.0!nntp.google.com!news1.google.com!postnews.google.com!hs8g2000vbb.googlegroups.com!not-for-mail
From: Martin <martin@thedowies.com>
Newsgroups: comp.lang.ada
Subject: Re: Pure function aspect?...
Date: Mon, 16 Jan 2012 02:48:28 -0800 (PST)
Organization: http://groups.google.com
Message-ID: 
 <9f0669ff-6cb9-4936-9a05-655867639fed@hs8g2000vbb.googlegroups.com>
References: 
 <1d74a186-2599-4de5-af49-ffca2529ea96@do4g2000vbb.googlegroups.com>
 <jens6a$3fb$1@munin.nbi.dk>
 <Pine.LNX.4.64.1201131048370.2287@medsec1.medien.uni-weimar.de>
 <jeqgjh$osk$1@munin.nbi.dk>
NNTP-Posting-Host: 20.133.0.8
Mime-Version: 1.0
X-Trace: posting.google.com 1326710909 20542 127.0.0.1 (16 Jan 2012 10:48:29
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Mon, 16 Jan 2012 10:48:29 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: hs8g2000vbb.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-16T02:48:28-08:00
List-Id: <comp.lang.ada>

On Jan 14, 12:00=A0am, "Randy Brukardt" <ra...@rrsoftware.com> wrote:
> <stefan-lu...@see-the.signature> wrote in message
>
> news:Pine.LNX.4.64.1201131048370.2287@medsec1.medien.uni-weimar.de...
>
> > On Thu, 12 Jan 2012, Randy Brukardt wrote:
> ...
> > However, another reason, why the AI became so complex, seems to be the
> > attempt to rather precisely specify side-effects, instead of providing
> > just the ability to declare "no side effects".
>
> There has been strong opposition to a "checked" pure function declaration=
 (I
> had floated that first, and it went nowhere), and global in out =3D> 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"?

with Logger;   -- Perhaps allowing 'limited with' if only needed in
the aspect?
package ... is
   function Foo (P1 : Integer)
      return Integer
      with Pure =3D> all or (Logger.Report (S : String) and
Logger.Report (S : String; I : Integer));
...

I think you'd need to enumerate all 'ignorable' state-changing calls.
Or perhaps a short-hand:

with Logger;   -- Perhaps allowing 'limited with' if only needed in
the aspect?
package ... is
   function Foo (P1 : Integer)
      return Integer
      with Pure =3D> all or (package Logger);
...




> And just declaring "no side-effects" without checking it is actively harm=
ful
> in my opinion because, perversely, it makes a program less safe. That's
> because the compiler is going to take advantage of this declaration to
> remove calls (especially in contracts and assertions), and if the call in
> fact has side-effects, doing that is not safe (and can easily lead to bug=
s
> or even erroneous execution). (And if you aren't going to let the compile=
r
> take advantage of this knowledge, declaring it is pointless.)
>
> I have some lengthy examples of this problem that are tooo long to presen=
t
> here (and at least get any other work done), but trust me, it is very rea=
l.
>
> The lack in global in out isn't a deal breaker for Ada 2012, simply becau=
se
> 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.


> And we need (at least) both of those
> to have enough completeness to really reason formally about Ada programs.
> Hopefully, future versions of Ada will take up both of these again.

Yes, please!

-- Martin