Re: Pure function aspect?...

[Martin <martin@thedowies.com>]

On Jan 14, 12:00 am, "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 => 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 => 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 => all or (package Logger);
...




> And just declaring "no side-effects" without checking it is actively harmful
> 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 bugs
> or even erroneous execution). (And if you aren't going to let the compiler
> take advantage of this knowledge, declaring it is pointless.)
>
> I have some lengthy examples of this problem that are tooo long to present
> here (and at least get any other work done), but trust me, it is very real.
>
> The lack in global in out isn't a deal breaker for Ada 2012, simply because
> 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