Re: Pure function aspect?...

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Wed, 18 Jan 2012 19:17:45 -0600, Randy Brukardt wrote:

> "Martin" <martin@thedowies.com> wrote in message 

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

The problem here is that the exception contracts do not obey the law of
excluded middle. I.e. raise A or not raise A is not necessarily true. The
syntax should distinguish promises (not to raise A) with obligations (to
raise A). In the above you have a negated promise not raise Program_Error,
i.e. Foo *may* raise Program_Error, but it is not required to do so. On the
contrary, My_Defined_Error is an obligation, Foo is *required* to raise it
when the condition is not met.

This is "intuitionistic logic," a bit complicated thing, but necessary
here. The simplest way to handle it would be to have:

function Foo ...
   <a-nice-name-for-possible-exceptions> => X,
   <necessary-exceptions> => Y

Y is a subset of X. Foo never raises anything from not X.

Inference of contracts of possible exceptions is simple. A conservative
estimation is a union of all exception sets of called subprograms for which
no handler is present.

For necessary exceptions it is in general impossible to do (equivalent to
halting). So it looks more appropriate for SPAK than for Ada.

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

Storage_Error should be a conditional:

   may_raise Storage_Error when Standard_Pool'Free_Space < 1024;

Actually any exception should be. E.g.

   procedure Sort (X : in out Data; F : Order_Func)
      may_raise Program_Error when Order_Func may_raise Program_Error;
         -- Sort does not raise Program_Error by itself

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

It is time to make exception a proper discrete type with another type for
sets of exceptions. It would be nice to have a tree order of exceptions,
i.e. extensible sets of exceptions too.
 
> 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).

No need to have complete contracts because there is a gray area between
'may raise' and 'must raise'.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de