Re: Ada 2012 Constraints (WRT an Ada IR)

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

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:o28non$1fn8$1@gioia.aioe.org...
> On 07/12/2016 00:15, Randy Brukardt wrote:
...
>> Moreover, most contracts (at least the ones I'd write) raise specific
>> exceptions (not Assertion_Error). Indeed, this is a far better way to 
>> define
>> something that raises an exception than an English comment. (Which is the
>> only other alternative for the specification - and its the specification
>> that matters, not the body.)
>
> As I said in another post it is a bad idea. The list exceptions, their 
> names, must tell the reader when they are to propagate. You could specify 
> the exact condition in a few very limited cases. In a real life scenario 
> you cannot specify the Boolean expression guarding Disk_Error. Moreover, 
> in most cases that would be an over-specification.

I never meant the above to be exclusive. Sometimes, as you say, an exception 
is raised by something external to the Ada program, and that is probably 
besst described in English. I was just talking about exceptions that depend 
only on the parameter values.

> My point is that either you don't need the expression or else it must/can 
> be statically provable and thus become a proper pre-/post-condition with 
> no exceptions involved.

Not everything can be statically proven (think Unchecked_Conversion), and a 
lot of stuff can only be proven in a full-program scenario, so I'm dubious 
of the above in any case. But even if that turns out to be possible years 
from now, I'm more interested in what I can do today -- especially if it is 
likely to be helpful to present (i.e. Codepeer) and future provers. A 
dynamic check that can be proven (or better proven and eliminated by the 
compiler) helps more than specifications with no machine-processable 
description.

                              Randy.