Re: Pure function aspect?...

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

"Martin" <martin@thedowies.com> wrote in message 
news:9f0669ff-6cb9-4936-9a05-655867639fed@hs8g2000vbb.googlegroups.com...
On Jan 14, 12:00 am, "Randy Brukardt" <ra...@rrsoftware.com> wrote:
> <stefan-lu...@see-the.signature> wrote in message
...
>> 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"?

Something on that line. The global in/out proposal handling that in terms of 
allowing the specification of what state is modified. If that state doesn't 
conflict with other routines, then optimization is still possible.

But one of the important points is that side-effects really ought to prevent 
optimization (and assumptions) unless the compiler (or proof tool) can 
actually prove they don't matter. A call that is being logged, for instance, 
probably shouldn't be eliminated even if the results are the same (because 
you couldn't easily relate the actual calls to the source code).

One can argue the other side of this, too, and it's obvious there are no 
easy answers. In which case I prefer to stay as close to the "canonical" 
semantics as possible.

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

Well, clearly it would be an aspect (like the other contracts), and each 
exception ought to be able to have an optional postcondition as well (which 
defines when the exception might be raised). So more like:

   function Foo (P1 : Integer) return Integer
      when Pre => ...
               Post => ...
               Raises => Program_Error, Storage_Error,
                                My_Defined_Error when P1 not in Even,
               Global in => null,
               Global out => null;

The exception contract would require that the compiler prove that 
Constraint_Error and Tasking_Error are not propagated. (The same would  be 
true for Storage_Error, but that would be impossible for the vast majority 
of compilers). I'm also proposing a way to name a group of exceptions, so 
you wouldn't have to write huge sets repeatedly. (All of the exceptions in 
package IO_Exceptions could be named "IO_Exceptions" so it wouldn't be 
necessary to write about them individually.)

I of course have no idea how far any of this will get, it won't be taken up 
for a while and won't be standardized for years, and in any case, it is all 
optional. No one is going to be required to have complete contracts (I 
suspect that will be going too far).

                                            Randy.