Re: Ada 2012 Constraints (WRT an Ada IR)

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

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:o1s71b$oi7$1@gioia.aioe.org...
> On 01/12/2016 23:26, Randy Brukardt wrote:
>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
>> news:o1oohd$13nu$1@gioia.aioe.org...
>> ...
>>> On the contrary, predicates is useless and dangerous mess.
>>
>> I can understand "useless" (that's an opinion I don't share, but it's 
>> fair
>> to have it), and I understand "mess" (the difference between static and
>> dynamic predicates shouldn't have happened; I wanted set constraints 
>> instead
>> of static predicates, which would have been more consistent), but I don't
>> understand dangerous. Predicates (and all contracts, for that matter) are
>> designed not the affect the semantics of a program at all if they are
>> removed (or "Ignored").
>
> When the contract specifies some behavior, e.g. raising or not raising 
> exceptions?

That's a bad contract. (Especially for predicates.)

Some of us (including me) wanted to have Ada require no side-effects in 
contracts, but we got bogged down in deciding precisely what is a 
side-effect and it ended up as an unimplementable implementation permission. 
Hopefully, Ada 202x will handle this better.

>> Moreover, predicates are inherited in much the same way that constraints
>> (and null exclusions as well, those also aren't formally constraints);
>
> Inheritance by no means imply safety.
>
> Unconditional substitutability requires strengthening constraints of the 
> out-parameters and weakening constraints of the in-parameters. For in-out 
> it is both weakening the pre- and strengthening post-conditions, i.e. 
> always wrong unless proven otherwise...
>
> If under "inheritance" you mean conjunction with the parent's predicate it 
> is strengthening.

Constraints work the same way. So why the difference??

>> there's little difference in the way any of these work. So it's hard to 
>> see
>> why constraints would be OK and predicates would be dangerous. (It's
>> actually more the other way around, since suppressing a contraint can
>> actually make a program dangerous; that's not possible for a predicate.)
>
> Selected constraints are OK, because they are known to do known things. 
> Predicates are just arbitrary expressions the programmer sets without 
> understanding all effects of his actions. There is no language support to 
> eliminate undesired effects or to define in any form the behavior expected 
> to be checked against one in effect.

I agree with the last statement (outside of static predicates, which are 
quite restricted expressions and thus can only do limited things), but that 
should change in the next version of Ada. At least I hope it does.

                          Randy.