Re: Ada 2012 Constraints (WRT an Ada IR)

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

On 07/12/2016 23:26, Randy Brukardt wrote:
> "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.

That does not change much. In most cases you still cannot do that 
without having the expression as complex as the body itself. Instead of 
one implementation you have two and thus you double the opportunity for 
making an error.

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

Right

> A
> dynamic check that can be proven (or better proven and eliminated by the
> compiler) helps more than specifications with no machine-processable
> description.

Wrong. The proper way to do this is elevate the check into the behavior 
and contract an exception. Later, when proofs are mature, client could 
prove absence of the exception. Nothing lost, everybody is happy.

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