Re: Pure function aspect?...

[stefan-lucks@see-the.signature]

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