Re: Pure function aspect?...

[Martin <martin@thedowies.com>]

On Jan 13, 12:00 am, "Randy Brukardt" <ra...@rrsoftware.com> wrote:
> "Martin" <mar...@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 athttp://www.ada-auth.org/cgi-bin/cvsweb.cgi/ai05s/ai05-0186-1.txt.
>
>                                                              Randy.


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