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=-0.3 required=5.0 tests=BAYES_00,
	REPLYTO_WITHOUT_TO_CC autolearn=no 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.190.99 with SMTP id gp3mr547794pbc.1.1326451820396;
        Fri, 13 Jan 2012 02:50:20 -0800 (PST)
Path: 
 lh20ni177125pbb.0!nntp.google.com!news1.google.com!goblin3!goblin.stu.neva.ru!news-1.dfn.de!news.dfn.de!news.uni-weimar.de!not-for-mail
From: stefan-lucks@see-the.signature
Newsgroups: comp.lang.ada
Subject: Re: Pure function aspect?...
Date: Fri, 13 Jan 2012 11:48:55 +0100
Organization: Bauhaus-Universitaet Weimar
Message-ID: <Pine.LNX.4.64.1201131048370.2287@medsec1.medien.uni-weimar.de>
References: 
 <1d74a186-2599-4de5-af49-ffca2529ea96@do4g2000vbb.googlegroups.com>
 <jens6a$3fb$1@munin.nbi.dk>
Reply-To: stefan-lucks@see-the.signature
NNTP-Posting-Host: medsec1.medien.uni-weimar.de
Mime-Version: 1.0
X-Trace: tigger.scc.uni-weimar.de 1326451820 2142 141.54.178.228 (13 Jan 2012
 10:50:20 GMT)
X-Complaints-To: news@tigger.scc.uni-weimar.de
NNTP-Posting-Date: Fri, 13 Jan 2012 10:50:20 +0000 (UTC)
X-X-Sender: lucks@medsec1.medien.uni-weimar.de
In-Reply-To: <jens6a$3fb$1@munin.nbi.dk>
Content-Type: TEXT/PLAIN; charset=US-ASCII
Date: 2012-01-13T11:48:55+01:00
List-Id: <comp.lang.ada>

On Thu, 12 Jan 2012, Randy Brukardt wrote:

> "Martin" <martin@thedowies.com> wrote in message 
[...]
> > 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!!).
>
> 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. 

Very regrettable! 

But reading the AI makes one understand why this is so complicated. There 
are class-wide-operations. If any pure function (or rather, any 
side-effect-free function or procedure) is going to use them, these need 
their own aspect annotations. Thee are the descendents from 
Ada.Finalization.*. There are instances of generic subprograms. Even if 
the generic subprogram is side-effect-free by itself, the 
side-effect-freeness of the instance is likely to depend on the 
side-effect-freeness of the generic parameters ...

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". Now it is too late, but a 
simplified approach, allowing only "with Global in out => null;" with the 
option to extend this later would have been acceptable for Ada 2012. :-/

BTW, why do you write "with Global in out => (null);" with brackets?

> 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.

-- 
---- Stefan.Lucks (at) uni-weimar.de, University of Weimar, Germany  ----
    <http://www.uni-weimar.de/cms/medien/mediensicherheit/home.html>
------  I  love  the  taste  of  Cryptanalysis  in  the  morning!  ------