Version 1.4 of ai12s/ai12-0100-1.txt

Unformatted version of ai12s/ai12-0100-1.txt version 1.4
Other versions for file ai12s/ai12-0100-1.txt
!standard 4.7(4)          14-07-14 AI05-0100-1/02
!class binding interpretation 14-05-12
!status Corrigendum 2015 14-07-14
!status ARG Approved 9-0-0 13-06-28
!status work item 14-05-12
!status received 14-03-11
!priority Medium
!difficulty Easy
!qualifier Omission
!subject A qualified expression makes a predicate check
!summary
A qualified expression checks that the value satisfies any predicates of the qualified subtype.
!question
If the subtype of a qualified expression has a predicate, is that predicate checked? (Yes.)
4.7(4) says that the evaluation of a qualified_expression "...checks that its value belongs to the subtype denoted by the subtype_mark." The AARM note 4.7(4.a) makes it clear that a subtype conversion is NOT performed here, so the predicate check associated with a subtype conversion doesn't happen here.
3.2(8) defines "belongs" for this context: "The set of values of a subtype consists of the values of its type that satisfy its constraint and any exclusion of the null value. Such values belong to the subtype."
As we know, a predicate doesn't change the set of values. So it doesn't appear here, either.
Thus there is no predicate check for a qualified expression. This seems weird, since a similar type conversion would make a predicate check. Should the wording make it clear that a qualified expression does make a predicate check? (Yes.)
!recommendation
(See Summary.)
!wording
Modify 4.7(4):
The evaluation of a qualified_expression evaluates the operand (and if of a universal type, converts it to the type determined by the subtype_mark) and checks that its value belongs to the subtype denoted by the subtype_mark. The exception Constraint_Error is raised if this check fails. {Furthermore, if predicate checks are enabled for the subtype denoted by the subtype_mark, a check is performed as defined in subclause 3.2.4, "Subtype Predicates" that the value satifies the predicates of the subtype.}
!discussion
We certainly want the checks made by a qualified expression to be at least as strict as those associated with an explicit type conversion (the type conversion will allow additional things where a conversion happens).
For example:
subtype Even is Natural with Dynamic_Predicate => Even mod 2 = 0;
Var : Natural; Three : constant Natural := 3;
Var := Even'(Three); -- Needs new wording for a predicate check.
Var := Even(Three); -- Predicate check, thus raises Assertion_Error.
Without the new wording, Even'(Three) would not raise an exception, while Even(Three) would. [Aside: Even'(3) would raise an exception, as in that case 3 would have a universal type and that would be subtype converted, thus checking the predicate.]
We need to refer to the effect defined in 3.2.4 for the same reason that we do that in 4.6 (see AI12-0096-1). We don't want to repeat the somewhat complex rules as to what happens when a predicate check fails.
!corrigendum 4.7(4)
Replace the paragraph:
The evaluation of a qualified_expression evaluates the operand (and if of a universal type, converts it to the type determined by the subtype_mark) and checks that its value belongs to the subtype denoted by the subtype_mark. The exception Constraint_Error is raised if this check fails.
by:
The evaluation of a qualified_expression evaluates the operand (and if of a universal type, converts it to the type determined by the subtype_mark) and checks that its value belongs to the subtype denoted by the subtype_mark. The exception Constraint_Error is raised if this check fails. Furthermore, if predicate checks are enabled for the subtype denoted by the subtype_mark, a check is performed as defined in subclause 3.2.4, "Subtype Predicates" that the value satifies the predicates of the subtype.
!ASIS
No ASIS effect.
!ACATS test
An ACATS C-Test should ensure that this check is made. There is a commented-out subtest at the bottom of ACATS 4.0 test C324002; once this AI is approved that test case can be uncommented.
!appendix

From: Randy Brukardt
Sent: Tuesday, March 11, 2014  4:59 PM

If the subtype of a qualified expression has a predicate, is that predicate
checked?

4.7(4) says that the evaluation of a qualified_expression "...checks that its
value belongs to the subtype denoted by the subtype_mark." The AARM note
4.7(4.a) makes it clear that a subtype conversion is NOT performed here, so
the predicate check associated with that doesn't happen here.

3.2(8) defines belongs for this context: "The set of values of a subtype 
onsists of the values of its type that satisfy its constraint and any exclusion
of the null value. Such values belong to the subtype."

As we know, a predicate doesn't change the set of values. So it doesn't appear
here, either.

So, according to this wording (and the lack of any specific wording to the
contrary), a qualified expression appears to not check whether the value
satisfies the predicate of the subtype.

That seems weird, given that an explicit type conversion would make such a
check. Thus,

   subtype Even is Natural with Dynamic_Predicate => Even mod 2 = 0;

   Var : Natural;

   Var := Even'(3); -- No predicate check, thus no exception

   Var := Even(3); -- Predicate check, thus raises Assertion_Error.

I think this is wrong and we need some wording in either 4.7 or 3.2.4 to say
that the predicate (if any) is checked for a qualified expression.

I was going to put such a test case (to ensure that the check was made) into
an ACATS test that I'm working on, but it appears that there would be no
justification for such a test. And I surely don't want a test insisting that
the check isn't made unless we agree that we really want that. As such, it is
best left for the round 2 tests (which will include tests for Binding
Interpretations like AI12-0071-1).

Thoughts?

****************************************************************

From: Gary Dismukes
Sent: Tuesday, March 11, 2014  5:24 PM

> I think this is wrong and we need some wording in either 4.7 or 3.2.4 
> to say that the predicate (if any) is checked for a qualified expression.

It looks like your reading is right, and I agree that it seems wrong (and
definitely surprising) not to do the predicate check along with the
constraint check.  An RM correction seems in order.

****************************************************************

From: Steve Baird
Sent: Tuesday, March 11, 2014  5:29 PM

I agree on all points.

****************************************************************

From: Randy Brukardt
Sent: Tuesday, March 11, 2014  6:17 PM

FYI, GNAT does not appear to make a predicate check for a qualified expression.

****************************************************************
Questions? Ask the ACAA Technical Agent