Re: Press Release - Ada 2012 Language Standard Approved by ISO

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

On Mon, 24 Dec 2012 07:44:00 +0100, Yannick Duchêne (Hibou57) wrote:

> Indeed, one may argue  
> they are the exceptions an implementation raise it self (either to match a  
> contract or more freely) and they are the ones its dependencies may raise.

The contract: "I raise if you do" is not an exposition of implementation
details.

Exception contracts must be conditional, that is clear. Otherwise closures
and things like Storage_Error will not work.
  
> Some exceptions are under control, some are not. Think about an hardware  
> failure during some processing, as an example…

Such things (faults) are not exceptions. They raise (if ever) in a context
not affected by the fault. E.g. master task, another partition, OS. There
you can contract them.

> May be the contract, instead of specifying exhaustively what exceptions a  
> sub‑program may raises, could instead specify it may raise “this one”, or  
> must not raise “this other one”, all other exceptions being of unspecified  
> occurrence.

Yes "I raise X" does not imply "I do not raise not X." It is intuitionistic
logic. You have X, a negation of X and a gray area between them. P does not
imply not P.

Furthermore exception contracts must include stuff for which people would
misuse post-conditions and predicates. That is

   sqrt(x) raises Constraint_Error if x < 0
[+ sqrt(x) may not raise Constraint_Error if x >= 0 ]

rather than weaker

   sqrt may raise Constraint_Error =
      = sqrt(x) raises Constraint_Error if <unknown>

Merry Christmas,

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