Re: Ada 2012 Constraints (WRT an Ada IR)

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

On 2016-12-21 01:59, Randy Brukardt wrote:
> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
> news:o3b316$153k$2@gioia.aioe.org...
>> On 2016-12-19 23:33, Randy Brukardt wrote:
> ...
>>> And I'm not sure why
>>>     subtype Y is X range 1 .. 100;
>>> is OK and
>>>     subtype Z is X with Static_Predicate => Z > 0;
>>> is not. They both have explicit declarations of the subtype, and the
>>> semantics is effectively the same.
>>
>> The former declares a continuous range from which the semantics of numeric
>> operations and attributes can be deduced. For the later, nobody has any
>> idea without looking at the expression = implementation.
>
> The expression is just a poor way of describing a set.

It is not about the way you specifying a set it is about what properties 
the parent's mathematical structure retains on that set. If the set is 
any, the answer is just none.

>> "Effectively same" is meaningless on its own. The generated object code is
>> "effectively same" too.
>
> I said "effectively the same" because there are subtle wording differences
> which only matter in a few cases. Had we had first-class set constraints,
> we'd have had the same rules (as we didn't want to support discontigous
> arrays).
>
> So far as the set of operations and reasoning goes, there's no difference
> between reasoning for a set and for a single range (which is just a subset
> of a set anyway).

It is a continuous subset. This preserves a lot of properties like being 
a convex set a,b in S => (a+b)/2 in S etc.

>> As I said, it is low-level and useless from SW design POV. You must be
>> able to answer questions like if you used Z in an algorithm of X, would it
>> work? If not, how, when, where etc. A range allows answering such
>> questions, an arbitrary constraint does not.
>
> A static_predicate is not an *arbitrary* constraint. It's restricted to
> expressions that can easily be represented as a set with a small number of
> ranges.

Implementation is irrelevant.

> One certainly can reason about it.

You can tell nothing about such subsets, they are general case subsets. 
They are worse than that, if the constraint is allowed to use non-local 
dynamic Boolean functions. That would produce non-sets.

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