Re: Pure function aspect?...

["Randy Brukardt" <randy@rrsoftware.com>]

"Martin" <martin@thedowies.com> 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.