Re: Quantified expressions: no support for restriction predicates

[phil.clayton@lineone.net]

On Sunday, April 29, 2012 8:35:18 PM UTC+1, Robert A Duff wrote:
> phil.c...@lineone.net writes:
> 
> > Is that actually possible for a Dynamic_Predicate?  Section 3.2.4 Subtype Predicates, para 27/3 says:
> >
> >   The discrete_subtype_definition of a loop_parameter_specification
> >   shall not denote ... or any subtype to which Dynamic_Predicate
> >   specifications apply.
> 
> Yeah, I think you're right.  The idea is that we didn't want hidden
> inefficiencies.
> 
>     type T is new Integer with
>         Dynamic_Predicate => T mod 10_000 = 0;
>     for X in T loop -- Illegal!
> 
> If that were legal, it would probably be grossly inefficient.

Right, this is the key point.  Writing pre- and postconditions where many elements are quantified over but immediately ignored due to a 'restriction predicate' is not good style, given these conditions are to be evaluated.  It would be preferable to quantify over just the elements that satisfy the restriction predicate in the first place.

For a subtype with a static predicate, presumably there is no efficiency issue because the restrictions placed on a static predicate enable the compiler to generate code that skips the elements not satisfying the predicate.

For static analysis, one would not worry about efficiency of evaluation and restriction predicates are common-place.  

Phil