Known-on-entry (RM 6.1.1) should include short-circuit and membership operations

[sttaft]

An AdaCore engineer noticed that the definition of known on entry in the Ada RM 6.1.1(20/5-22.10/5) makes no mention of short-circuit control forms or membership tests. That seems weird, since a function call to a pure function is permitted so long as all of the operands are known on entry, and there is nothing preventing such a function containing a short-circuit control form or a membership test.

RM 6.1.1(22.4/5) includes a known on entry:

an invocation of a predefined operator where all of the operands are known on entry;

Perhaps that should be generalized to include short-circuit control forms and membership tests.

[sttaft]

Note also that conditional expressions are permitted as known-on-entry expressions, and any short-circuit control form can be expressed as a conditional expression, so again it seems odd that short-circuit control forms are not allowed.

[ARG-Editor]

I'm sure that even experienced Ada hands often forget that short circuit forms and memberships are not predefined operators and have to be mentioned separately in wording. I suspect that the author of this wording (which I think was me) probably made that mistake. It's unlikely to me that the omission was intentional (and there is no evidence that it is in the AI). I saw that my original idea sketch (first e-mail in !appendix) included a bullet for predefined operators (but not short circuits or memberships). I'm sure that was a sketch of an idea rather than an "every detail worked out" idea (for which including pedantic cases like "short circuit control forms" would have buried the idea), but we never revisited those pedantic cases. "predefined operator {or short circuit control form}" would seem to be enough to allow short circuits. (I'm assuming that short circuits have "operands"; while that's not clear, 4.5.1(7) definitely uses the term in relation to parts of short circuits so I think it is OK here too.) Memberships provide a bit of a challenge as I don't think "known on entry" tries to cover subtypes. (Memberships involving only objects are not a problem, of course). It would seem that range bounds as well as discriminant and index constraints, would also need to be "known on entry". I suppose that we can find wording that would work, but I doubt that we should try to merge that with the existing wording for operators. Are you writing an AI?? Randy.

[sttaft]

I'm sure that even experienced Ada hands often forget that short circuit
forms and memberships are not predefined operators and have to be mentioned
separately in wording. ...

"predefined operator {or short circuit control form}" would seem to be
enough to allow short circuits. (I'm assuming that short circuits have
"operands"; while that's not clear, 4.5.1(7) definitely uses the term in
relation to parts of short circuits so I think it is OK here too.)

Yes, this seems straightforward.

Memberships provide a bit of a challenge as I don't think "known on entry"
tries to cover subtypes. (Memberships involving only objects are not a
problem, of course). It would seem that range bounds as well as discriminant
and index constraints, would also need to be "known on entry". I suppose
that we can find wording that would work, but I doubt that we should try to
merge that with the existing wording for operators.

I don't see a problem here, because this is talking about (named) subtypes that appear in postconditions, and by their very nature all parts of named subtypes are effectively statically-denoted constants, and they must be known on entry since you can't define a subtype between the subprogram specification and the Post aspect specification. Membership tests require subtype_marks, not subtype_indications. Ranges are allowed, but not range constraints, and definitely not index or discriminant constraints. But we do need to worry about ranges where one of the bounds involves an impure function call, but those are pretty well covered by known-on-entry already. The prefix of 'Range would also need to be known-on-entry.

Are you writing an AI??

If you want to assign it to me, that would be fine ...

           Randy.

[ARG-Editor]

... Membership tests require subtype_marks, not subtype_indications.

This is the key point, and one I had to look up to verify (I didn't believe it, even coming from you). I certainly would not have guessed that, given that we allow arbitrary expressions, but not the description of a constraint. Seems like an odd restriction. Be that as it may, I think we need something like "all expression parts of any membership test need to be known on entry". (Except that we can't use "need" in Standard wording. :-) I don't think the bounds of a range or the prefix of the range attribute are clearly covered by the existing wording, which is quite specific to what entities are covered (and one presumes that no others are involved). And the surely needs to be the case for memberships.

>Are you writing an AI?? If you want to assign it to me, that would be fine ...

I think Steve assigns AIs, but I'm not volunteering to do it, and it seems easy enough and non-controversial enough to just get it done. So consider it a strong suggestion! Randy.

[sttaft]

OK, I'll write up an AI on this issue.

[ARG-Editor]

This issue is covered by AI22-0157-1, and will be on the agenda for our next ARG meeting.

[ARG-Editor]

AI22-0157-1 was approved by ARG meeting #63M, so this issue has been closed.

[ARG-Editor]

Brad Moore has noted that the use of Old on A(Y) in the example of AI22-0157-1 did not make any sense, as both A and Y were in parameters, so neither should change during the execution of procedure Check. That example is:

procedure Check  (X : in out Integer; L : Positive; A : String; Y : Positive)   with Post =>     (if X'Old in 1 .. L and then Y in A'Range       then X >= Character'Pos (A(Y)'Old));

Changing the A parameter to be an in out parameter seemed like the best fix, as in that case the bounds of A would be unchanged by the call.

procedure Check  (X : in out Integer; L : Positive; A : in out String; Y : Positive)   with Post =>     (if X'Old in 1 .. L and then Y in A'Range       then X >= Character'Pos (A(Y)'Old));

However, that shows another problem: the expression “Y in A’range” is not known on entry -- regardless of whether A is an in or in out parameter. It’s not completely clear for A’range, but replacing it with the supposedly equivalent “A’First .. A’Last” shows the problem: the prefix A is none of the things that are known on entry. We could fix that by introducing an extra ‘Old (done above). But that doesn’t help, as attribute references are treated as known-on-entry.

This example seems too reasonable to ignore. Any postcondition involving an array is likely to test the bounds of the array somewhere.

It seems like we need to add at least ‘First and ‘Last to the definition of known-on-entry, as they are very likely to be used in such circumstances. Perhaps it would be best to add them with specific prefixes (object prefixes that are known-on-entry, or designate a parameter (of any mode), as the bounds of parameters cannot be changed, even for unconstrained arrays, or are of a constrained array type, or prefixes that are a constrained array subtype or a discrete subtype).

As the deadline for fixes to this AI has passed, I’ve reopened it to consider this question.