Re: Quantified expressions: no support for restriction predicates

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

<phil.clayton@lineone.net> wrote in message 
news:22242340.4097.1335486547825.JavaMail.geo-discussion-forums@vbki8...
...
>I can see the lack of restriction predicates being a potential 'gotcha' 
>when writing/transforming
> pre/postconditions, e.g. incorrectly converting
>
>  not (for all X in T => if Odd(X) then P(X))
>
>into
>
>  (for some X in T => if Odd(X) then not P(X))

This is not a problem, since both of these are illegal. :-) Conditional 
expressions always have to be directly enclosed in parens, and that isn't 
done here. (There are special cases to allow the omission of those parens 
when they are already *directly* there, but in only those cases, like P(if 
Odd(X) then not P(X)); but not P(Param => if Odd(X) then not P(X));.)

Has nothing to do with your point, though.

...
>I haven't followed all the developments in the areas of predicates. 
>Perhaps there are good reasons
> not to have such restriction predicates.  Anyway, just thought I would 
> raise the idea as they seem useful.

We decided to leave all of the contract expressions as code easily 
understandable by any novice Ada programmer (or middle-aged Ada programmer 
who has forgotten most of the advanced mathematics he once knew - like, say, 
me :-).

Conditional expressions and quantified expressions themselves were both a 
bit controversial for this reason. We added conditional expressions mainly 
so that implications and the like could be specified without having to write 
a separate function (which of course would defy compile-time analysis as the 
body wouldn't be present). We rejected the idea of an "implies" operator 
because a lot of people are confused by what it means -- the equivalent 
conditional expression is much clearer, especially at 2 am!

Quantified expressions are hard enough to understand as it is. I don't think 
complicating them further would be helpful, especially for the programmer 
that only saw them rarely (which is likely to be most Ada programmers).

                                         Randy.