Version 1.18 of ai05s/ai05-0153-3.txt

Unformatted version of ai05s/ai05-0153-3.txt version 1.18
Other versions for file ai05s/ai05-0153-3.txt

!standard 3.2.4(0)          11-06-02 AI05-0153-3/11
!standard 3.8.1(5)
!standard 3.8.1(8)
!standard 3.8.1(11)
!standard 3.8.1(15)
!standard 4.3.3(17)
!standard 4.5.2(29)
!standard 4.5.2(30/2)
!standard 4.6(51/2)
!standard 4.9(26/2)
!standard 4.9.1(2/2)
!standard 4.9.1(4)
!standard 5.4(5)
!standard 5.4(7)
!standard 6.4.1(13)
!standard 13.9.2(3)
!class Amendment 09-05-27
!status Amendment 2012 11-03-04
!status ARG Approved 7-0-1 11-02-18
!status work item 09-05-27
!status received 09-05-27
!priority Medium
!difficulty Medium
!subject Subtype predicates
!summary
A subtype predicate is an arbitrary boolean expression attached to a subtype. Predicates are checked on assignment, parameter passing, etc, and raise an exception on failure. Membership tests and the 'Valid attribute take the predicate into account.
In many ways, predicates are similar to, but more general than, constraints.
There are two predicate aspects: Static_Predicate and Dynamic_Predicate. Static_Predicates must obey certain restrictions, and the subtype can be static, so it can be used as a choice in case statements and the like. 'for' loops are also defined over subtypes with static predicates.
!problem
Ada's constraints are a powerful way to enhance the contract of an object (including formal parameters). But the constraints that can be expressed are limited.
For instance, it isn't possible to specify that a record subtype may have any of several discriminant values -- for discriminants we can only specify a single value or allow all discriminants. Similarly, it isn't possible for a subtype to define a noncontiguous subset of an enumeration type. Even in cases where contiguous subranges work, it is more maintainable to avoid depending on the order, if there is no natural order to a particular enumeration type.
!proposal
We define two new aspect predicate aspects, "Static_Predicate" and "Dynamic_Predicate", which take a condition (i.e. a BOOLEAN_expression). The condition can use the defining_identifier of the subtype to mean the "current instance" of the subtype (that is, the object to test the predicate against), as defined in AI05-0183-1.
The difference between Static_Predicate and Dynamic_Predicate is that in the former case, the expression is restricted to certain sort-of-static forms, which allows such subtypes to be used in situations requiring static subtypes, such as in case statements.
Example:
type T is ...; function Is_Good(X: T) return Boolean; subtype Good_T is T with Dynamic_Predicate => Is_Good(Good_T);
Good_T conceptually represents the subset of values of type T for which Is_Good returns True.
A predicate may be given on a subtype_declaration, in which case it applies to that subtype. A predicate may also be given on a type_declaration, in which case it applies to the first subtype.
The predicate is checked at certain places, such as assignment statements, explicit initialization, and parameter passing; an exception is raised if the predicate is False at such places.
Membership tests and 'Valid take the predicate into account, so "X in S" will be False if the predicate of S is False for X, and (for scalars) "X'Valid" will be False if the predicate of S is False for X,
The base subtype always has the predicate "True". Thus, the 'Base attribute may be used to remove the predicate; S'Base means "S without any constraint or predicate". (Note that 'Base is allowed only for scalars. There is no "remove the predicate" feature for nonscalars.)
Scalar subtypes with user-defined predicates cannot be used in cases that would make sense only for contiguous subranges -- 'First is illegal, use as an array index subtype is illegal, and so on. Thus, we avoid anomalies like "S'First in S" being False.
Certain subtypes with Static_Predicates are defined to be static. For example,
subtype Letter is Character with Static_Predicate => Letter in 'A'..'Z' | 'a'..'z';
Letter is a static subtype. (Actually, it should probably include things like 'À' -- this is just an example!)
Like any static subtype, Letter may be used as a choice in a case statement, case expression, variant record, or array aggregate, with all the benefits of full coverage checking.
Letter is also allowed in a 'for' loop, but nonstatic cases are not.
Note that case_expression and if_expression are defined in AI05-0188-1.
!wording
This AI depends on AI05-0183-1, which defines the syntax for aspect_specifications, which may be attached to declarations. It also depends on AI05-0158-1, which defines generalized membership tests as used in subtype Letter above.
AARM-3.2(1.b/2) says:
1.b/2 Glossary entry: {Subtype} A subtype is a type together with a
constraint or null exclusion, which constrains the values of the subtype to satisfy a certain condition. The values of a subtype are a subset of the values of its type.
Change it to:
1.b/2 Glossary entry: {Subtype} A subtype is a type together with optional
constraints, null exclusions, and predicates, which constrain the values of the subtype to satisfy a certain condition. The values of a subtype are a subset of the values of its type.
[Note: RM-3.2(8) says:
... The set of values of a subtype consists of the values of its type that satisfy its constraint. Such values belong to the subtype.
We are not changing this definition.]
Add new section 3.2.4:
3.2.4 Subtype Predicates
The language-defined "predicate aspects" Static_Predicate and Dynamic_Predicate may be used to define properties of subtypes. A "predicate specification" is an aspect_specification for one of the two predicate aspects.
Name Resolution Rules
The expected type for a predicate aspect expression is any boolean type.
Static Semantics
A predicate specification may be given on a type_declaration or a subtype_declaration, and applies to the declared subtype. In addition, predicate specifications apply to certain other subtypes:
- For a (first) subtype defined by a derived type
declaration, the predicates of the parent subtype and the progenitor subtypes apply.
- For a subtype created by a subtype_indication, the
predicate of the subtype denoted by the subtype_mark applies.
The "predicate" of a subtype consists of all predicate specifications that apply, and-ed together; if no predicate specifications apply, the predicate is True Redundant[(in particular, the predicate of a base subtype is True)].
Legality Rules
The expression of a Static_Predicate specification shall be "predicate-static"; that is, one of the following:
- a static expression that does not raise any exception;
- a membership test whose simple_expression is the current instance,
and whose membership_choice_list meets the requirements for a static membership test (see 4.9);
- a case_expression whose selecting_expression is the current instance,
and whose dependent_expressions are static expressions;
- a call to a predefined equality or ordering operator, where one operand
is the current instance, and the other is a static expression;
- a call to a predefined boolean logical operator, where both operands
are predicate-static; or
- a parenthesized predicate-static expression.
An index subtype, discrete_range of an index_constraint or slice, or a discrete_subtype_definition of a constrained_array_definition, entry_declaration, or entry_index_specification shall not denote a subtype to which predicate specifications apply.
The prefix of an attribute_reference whose attribute_designator is First, Last, or Range shall not denote a scalar subtype to which predicate specifications apply.
The discrete_subtype_definition of a loop_parameter_specification or a discrete_choice of a named_array_aggregate shall not denote a subtype to which Dynamic_Predicate specifications apply.
Dynamic Semantics
If the assertion policy (see 11.4.2) in effect is Check, then:
Redundant[On every subtype conversion, the predicate of the target subtype is evaluated, and a check is made that the predicate is True. This includes all parameter passing, except for certain parameters passed by reference, which are covered by the following rule: ] After normal completion and leaving of a subprogram, for each in out or out parameter that is passed by reference, the predicate of the subtype of the actual is evaluated, and a check is made that the predicate is True. For an object created by an object_declaration with no explicit initialization expression, or by an uninitialized allocator, if any subcomponents have default_expressions, the predicate of the nominal subtype of the created object is evaluated, and a check is made that the predicate is True. Assertions.Assertion_Error is raised if any of these checks fail.
AARM Ramification: Predicates are not evaluated at the point of the [sub]type declaration.
AARM Implementation Note: Static_Predicate checks can be removed even in the presence of potentially invalid values, just as constraint checks can be removed.
If any of the above Legality Rules is violated in an instance of a generic unit, Program_Error is raised. In addition to the places where Legality Rules normally apply (see 12.3), this rule applies also in the private part of an instance of a generic unit.
AARM Note: This is the usual way around the contract model; this applies even in generic bodies. The "In addition..." wording is included for consistency with similar rules, even though it's not really necessary, since Program_Error will be raised anyway.
NOTE: A predicate specification does not cause a subtype to be considered "constrained".
NOTE: A Static_Predicate, like a constraint, always remains True for all objects of the subtype, except in the case of uninitialized variables and other invalid values. A Dynamic_Predicate, on the other hand, is checked as specified above, but can become False at other times. For example, the predicate of a record is not checked when a subcomponent is modified.
[End of 3.2.4.]
3.8.1(5,8,11,15) says:
5 discrete_choice ::= expression | discrete_range | others
8 The expressions and discrete_ranges given as discrete_choices in a variant_part shall
be static. ...
11 * A discrete_choice that is a discrete_range covers all values
(possibly none) that belong to the range.
15 * If the discriminant is of a static constrained scalar subtype, then
each non-others discrete_choice shall cover only values in that subtype, and each value of that subtype shall be covered by some discrete_- choice [(either explicitly or by others)];
Modify 3.8.1(5,8,11,15) so the full coverage rules take predicates into account. This applies only in the static case:
5 discrete_choice ::= choice_expression | discrete_subtype_indication | range | others
[Note: AI05-0158-1 changes "expression" to "choice_expression". We are no longer using discrete_range here, because it's not necessarily a contiguous range.]
8 The choice_expressions, subtype_indications, and ranges given as discrete_choices
in a variant_part shall be static. ...
11 * A discrete_choice that is a subtype_indication covers all values
(possibly none) that belong to the subtype.
11.1 * A discrete_choice that is a range covers all values
(possibly none) that belong to the range.
15 * If the discriminant is of a static constrained scalar subtype, then
each non-others discrete_choice shall cover only values in that subtype {that satisfy the predicate}, and each value of that subtype {that satisfies the predicate} shall be covered by some discrete_choice [(either explicitly or by others)];
Modify 4.3.3(17) to take the syntax change above into account:
"...that is a {subtype_indication or range}[discrete_range] that defines a nonstatic or null range..."
Replace 4.5.2(29) so membership tests take the predicate into account (this includes the modifications of AI05-0158-1):
The membership_choice is a range and the value of the simple_expression belongs to the given range.
[Note: We don't have to mention that the type is scalar here because there aren't any non-scalar ranges.]
The membership_choice is a subtype_mark, the tested type is scalar, the value of the simple_expression belongs to the range of the named subtype, and the predicate of the named subtype evaluates to True.
Modify AARM-4.5.2(29.a):
Ramification: The scalar membership test only does a range check {and a predicate check}. It does not perform any other check, such as whether a value falls in a "hole" of a "holey" enumeration type. The Pos attribute function can be used for that purpose.
Modify 4.5.2(30/2):
The tested type is not scalar, and the value of the simple_expression satisfies any constraints of the named subtype, {the predicate of the named subtype evaluates to True,} and:
Add at the end of 4.6(51/2), so subtype conversions raise an exception on predicate failure:
If the assertion policy (see 11.4.2) in effect is Check, the predicate of the target subtype is applied to the value and Assertions.Assertion_Error is raised if the result is False.
Add to the end of 4.9(26/2), so subtypes with Static_Predicates can be static, but those with Dynamic_Predicate are not:
Also, a subtype is not static if any Dynamic_Predicate specifications apply to it.
Modify 4.9.1(2/2), so static matching takes predicates into account:
A subtype statically matches another subtype of the same type if they have statically matching constraints, {all predicate specifications that apply to them come from the same declarations, }and, for access subtypes, either both or neither exclude null. ...
Modify 4.9.1(4/3), so "statically compatible" takes predicates into account:
A constraint is statically compatible with a scalar subtype if it statically matches the constraint of the subtype, or if both are static and the constraint is compatible with the subtype. A constraint is statically compatible with an access or composite subtype if it statically matches the constraint of the subtype, or if the subtype is unconstrained. [One subtype is statically compatible with a second subtype if the constraint of the first is statically compatible with the second subtype, and in the case of an access type, if the second subtype excludes null, then so does the first.]
{Two statically matching subtypes are statically compatible with each other. In addition, a subtype S1 is statically compatible with a subtype S2 if:
- the constraint of S1 is statically compatible with S2, and
- if S2 excludes null, so does S1, and
- either:
- all predicate specifications that apply to S2 apply also to S1, or
- both subtypes are static, and every value that obeys S1's predicate also obeys S2's predicate.}
Modify 5.4(5), so that the removal of discrete_ranges from discrete_choice is reflected:
5 The choice_expressions, subtype_indications, and ranges given as discrete_choices
in a case_statement shall be static. ...
Modify 5.4(7/3), so the full coverage rules for case statements take predicates into account:
7/3 * {AI05-0003-1} If the expression is a name [(including a
type_conversion, a qualified_expression, or a function_call)] having a static and constrained nominal subtype, then each non-others discrete_choice shall cover only values in that subtype {that satisfy the predicate}, and each value of that subtype {that satisfies the predicate} shall be covered by some discrete_choice [(either explicitly or by others)].
Modify 6.4.1(13/3) (as modifed by AI05-0196-1):
For an access type, the formal parameter is initialized from the value of the actual, without checking that the value satisfies any constraint{, any predicate,} or any null exclusion;
Modify 13.9.2(3), so 'Valid takes predicates into account:
X'Valid Yields True if and only if the object denoted by X is normal[ and]{,}
has a valid representation{, and the predicate of the nominal subtype of X evaluates to True}. The value of this attribute is of the predefined type Boolean.
!discussion
We considered various ways to define 'First (and the like) on subtypes with predicates. They all seemed to lead to nothing but confusion, so the best idea is to simply forbid such things.
The rules forbidding 'First and the like are intended to forbid cases where the values that obey the predicate do not form a contiguous range. We could relax this somewhat. For example, we could allow 'First in the following cases:
Static_Predicate => True -- which is what you get by default Static_Predicate => 1 > 0 -- static expression with value True Static_Predicate => Cur_Inst in 1..10 -- contiguous range Static_Predicate => Cur_Inst >= 0 -- contiguous range 0..'Base'Last
However, it seems simplest to forbid 'First if there is any user-defined predicate.
Note that 'First is forbidden even in the static case. It would be easy for the compiler to calculate 'First as the smallest value that obeys the predicate and range constraint (taking care with null ranges), but it would still be error prone, because code that uses 'First tends to assume a contiguous range. If we need that functionality, we should define a new attribute to return the minimum value -- but we don't.
Note, however, that there is no problem with attributes like 'Succ, 'Pred, 'Image, etc, because these are defined on the base subtype. These ignore any range constraints, so it makes sense for them to ignore predicates. Of course, there's still a check on assignment, so:
X: S := ...; X := S'Succ(X);
the assignment to X will raise an exception if S'Succ(X) is out of the range of S, or the predicate of S is False for S'Succ(X).
---
Note that "in" and 'Valid return False if the predicate is False. This is unaffected by the Implementation Permissions of 3.2.4, which allow omission of certain predicate CHECKs (i.e. cases that raise an exception on predicate failure). Likewise, assertion policy => Ignore does not change the semantics of membership tests and 'Valid.
This means that "S'(X) in S" could be False if the assertion policy is Ignore. This is similar to suppressing checks (strange things can happen), but milder, because suppressing checks can cause erroneous behavior, whereas here, we get True, or False, or Constraint_Error.
---
Static Predicated Subtypes.
The following operations are allowed in Static_Predicate expressions: "=", "/=", "<", ">", "<=" ">=", "and", "or", "xor", "not", "in", "not in". The following are not: "and then", "or else", "mod", etc -- except that these are of course allowed in fully-static subexpressions (i.e. not involving the current instance). E.g., "X mod 2" is allowed if X is a static constant, but not if X is the current instance.
The purpose of defining some subtypes with user-defined predicates to be static is to allow those subtypes in places where the language provides full coverage checking: case statements, case expressions, variant parts, and array aggregates. For example, Ada has always allowed:
case Current_Char is when 'A'..'Z' | 'a'..'z' => ...
but it was previously impossible to give a subtype name for 'A'..'Z' | 'a'..'z'. We now allow:
subtype Letter is Character with Static_Predicate => Letter in 'A'..'Z' | 'a'..'z';
case Current_Char is when Letter => ... -- Allowed by this AI.
Table : constant array (Character) of Boolean := (Letter => True, -- Allowed by this AI. others => False);
Every predicate-static expression necessarily has the property that if you plug in a static expression in place of every occurrence of the current instance, you get a static expression. However, not every expression with this property is predicate-static. For example, "Cur_Inst > 2" is predicate-static, but "Cur_Inst mod 2 = 0" is not, even though both have the above plug-in property. The idea is that the set of values for which a predicate-static expression is True should be representable as a sequence of static subranges whose size is roughly proportional to the size of the relevant source text. For example:
subtype Even is Natural with Static_Predicate => Cur_Inst mod 2 = 0; -- Illegal!
doesn't qualify, because the the subrange sequence would be something like 0..0, 2..2, 4..4, ... 2**31-2..2**31-2, which is enormous. We expect implementations to actually form such subrange sequences at compile time, which is unreasonable in the "mod 2" case. "Cur_Inst > 2", on the other hand, can be represented as "3..2**31-1". The above would be legal if we said Dynamic_Predicate.
Note that the definition of static subtypes allows predicates coming from other subtypes:
subtype S1 is Natural with Static_Predicate => S1 < 100 or S1 > 1000; subtype S2 is S1 with Static_Predicate => S2 <= 50_000;
S1 is a static subtype, with the subrange sequence 0..99, 1001..Natural'Last. S2 is also static, with the subrange sequence 0..99, 1001..50_000. Note that the bounds of these subranges can come from both range constraints and from predicates -- all and-ed together at compile time.
Note that "Cur_Inst xor Static_Expr" is predicate-static. Why allow "xor"? Well, why not? We want to allow all the other logical operators, and "xor" is equivalent to "/=", so it seems trivial to implement. Note that "and" (etc.) on modulars are not included. Also, "and then" and "or else" are not included (if they were, they would mean the same thing as "and" and "or").
A membership_test with a list of values can be used as a Static_Predicate:
type Animal is (Dog, Cat, Shark, Boa_Constrictor);
subtype Pet is Animal with Static_Predicate => Pet in Dog | Cat;
But now if Parrot is added to Animal, there is no warning that the programmer had better decide whether it makes a good pet. It might be better to use a case_expression, in order to benefit from the full coverage rule:
subtype Pet is Animal with Static_Predicate => (case Pet is when Dog | Cat => True, when Shark | Boa_Constrictor => False);
Now adding Parrot to Animal causes a compile-time error on Pet.
In other words, a case_expression whose type is Boolean represents a set, with a requirement that you specify what's IN the set and also what's NOT IN the set.
Note that the last bullet in the definition of "predicate-static" allows parentheses, but not qualification. Qualification within a static subexpression is OK, but qualification of a subexpression involving the current instance leads to a non-predicate-static predicate. For example, "Cur_Inst > Natural'(2)" is predicate-static, but "Boolean'(Cur_Inst > 2)" is not. The reason is to ensure (without knowing the value of the current instance) that predicate-static expressions cannot raise exceptions.
----------------
An earlier version of this AI proposed a single Predicate aspect, which could allow static subtypes or not, depending on whether the expression happened to be predicate-static. We decided to split it into two aspects, Static_Predicate and Dynamic_Predicate, in part because otherwise, if you change a static predicate to a nonstatic one, faraway parts of your program can become illegal.
The following arguments against this argument were rejected:
- They won't change their run-time behavior, just become illegal.
- Changing the VALUES can have the same effect, so different
syntax doesn't really solve the problem. (E.g. "Cur_Inst in 1..10" changed to "Cur_Inst in 1..10 | 20".)
- We already have this "problem" for other static things
(changing "subtype S is Integer range 1..10" to "1..Non_Static" or "1..11" can cause faraway illegalities).
- Although it might be mildly useful, we don't say
"C: static constant Integer := ...", so why should we do so for predicates?
Another, perhaps more compelling reason for the split is that Static_Predicates are like constraints, in that they can only become False in the presence of invalid values (ignoring erroneous executions, of course). In contrast, Dynamic_Predicates are more dangerous to rely on, because they can become False in more cases: for example, the Dynamic_Predicate of a record is not checked when components of that record or global variables are modified.
---
Interactions with generics.
If a scalar subtype with a predicate is passed to a generic, the generic might assume that the subtype has a contiguous range. For example, it might say "for X in S'First .. S'Last - 1 loop", which probably won't work. This problem is quite likely if a new Ada 2012 subtype is passed to an existing Ada 2005 generic. Possible solutions:
1. Forbid passing such subtypes to generics if the formal is
discrete. (There's no problem for formal private types, because the generic doesn't know about 'First and the like.)
2. Allow it. But then generic contract model problems rear their ugly heads
-- we want 'First to be illegal, for example. We use the normal kludge: define things that should be illegal to raise Program_Error instead. This is fine; most compilers will warn in the problematic cases.
3. Add the "might have user-defined predicates" property to the contract.
The formal would say, "type T is ... with Predicate => <>;". This would allow actuals with and without predicates. Without this new syntax, actuals would not be allowed to have predicates. We would need to think about which language-defined generics should have "Predicate => <>" added. This seems like unnecessary complexity, especially now that Predicate has been split into Static_Predicate and Dynamic_Predicate; the Program_Error solution seems sufficient.
4. The predicate of the actual is ignored in the instance. This seems
like a bad idea for obvious reasons.
---
'for' loops.
We allow "for X in S loop" if S has a Static_Predicate, but not if it has a Dynamic_Predicate. It means the same as:
for X in S'Base loop if X in S then -- query the predicate ...
This is out of the question in the dynamic case, because the obvious implementation is grossly inefficient if S'Base is large and sparsely populated with values in S; there is no generally-applicable optimization that makes it efficient. Therefore, looping through all values is the programmer's problem in the dynamic case.
One generally-applicable implementation technique for the static case is to construct the compile-time-known array of disjoint subranges, and loop through those:
for Subrange_Index in Subranges'range loop for X in Subranges(Subrange_Index).First .. Subranges(Subrange_Index).Last loop ... -- loop body
The compiler would weed out null ranges (and generate no code at all if they are all null), coalesce overlapping ranges, and store them in increasing order.
Another generally-applicable technique is to encode the same sequence-of-subrange thing as loop containing a case statement for going to the next value. For example, if the sequence of subranges is 1..10, 200..300, the generated code would look like this:
X := 1; loop ... -- loop body case X is when 10 => X := 200; -- skip to next subrange when 300 => exit; -- end of last subrange when 1..9 | 200..299 => X := X + 1; end case; end loop;
In some cases, the compiler might unroll the loop. For example:
subtype RGB is Color with Static_Predicate => RGB in Red | Green | Blue; for X in RGB loop Do_Something(X); end loop;
could become:
Do_Something(Red); Do_Something(Green); Do_Something(Blue);
Note that one compiler writer reports that 'for' loops came in very handy while testing a prototype implementation of predicates.
---
Predicates are similar to constraints. The differences are:
- Constraints are restricted to certain particular forms (range
constraints, discriminant constraints, and so forth), whereas predicates can be arbitrary conditions.
- Constraints can only be violated for invalid values, whereas predicates
can be violated in various ways (important side effects in predicates, for example, could cause reevaluation of the predicate to get a different answer). However, it is possible to write well-behaved predicates. We don't know how to FORCE the programmer to write well-behaved predicates without being too restrictive.
- For "subtype S2 is S1 ...", the constraint on S2 is checked for
compatibility with the constraint on S1. We can't do that for predicates; instead we "and" them together.
Predicates are similar to type invariants. The differences are:
- A type invariant is a requirement on all values of a type outside of the
type's defining package(s). That is, invariants are specifically allowed to become False "within the abstraction".
- Therefore, invariants are only allowed for private TYPES,
whereas predicates are allowed for any SUBtype.
---
Although predicates are conceptually similar to constraints from a programmer's point of view, predicates are kept separate from constraints for detailed technical reasons. For example, if a predicate is applied to an indefinite subtype, the resulting subtype is still indefinite. If a predicate is applied to an unconstrained subtype, the resulting subtype is unconstrained.
This mirrors the semantics of null exclusions (which also are not constraints, despite the conceptual similarity).
---
We define predicates to be part of static matching, so that subtypes with different predicates are not considered identical.
---
Note that in general, predicates are only known to be True at the point where the language defines the check, so the compiler can't always assume they are True at some later point in the code. However, there are cases where the compiler can usefully deduce such later truths.
For example:
type String1 is new String with Dynamic_Predicate => String1'First = 1;
The compiler can deduce (if the assertion policy is Check) that all objects of type String1 have 'First = 1, and optimize accordingly. It could avoid storing the lower bound at run time.
For example:
type Rec is record A : Natural; end record; subtype Decimal_Rec is Rec with Dynamic_Predicate => Rec.A mod 10 = 0;
Obj : Decimal_Rec := (A => 10); -- (1)
procedure Do_It (P : in out Decimal_Rec) is begin P.A := 5; -- (2) Put (Obj in Decimal_Rec); -- (3) end Do_It;
Do_It (Obj); -- (4)
The predicate on Decimal_Rec will be checked at (1). The assignment at (2) makes the predicate False, so (3) will print False. However, after the call at (4) returns, a predicate check will be made which will raise an exception.
Such loopholes are unfortunate, but we really have no choice. There is no way to prevent "bad" predicates without being overly restrictive. Compilers may, of course, give warnings about questionable predicates. Note that predicates are no worse than other assertions, such as preconditions, in this regard.
Consider the alternatives: One can already specify predicates in comments, but of course such predicates can be false. Alternatively, one can sprinkle preconditions and pragmas Assert all over the place, but those can be false, too -- for the same reasons predicates can be false, and for the additional reason that one might forget some places to sprinkle.
---
We considered allowing implementations to check predicates at places where such checks are not required. However, that seems too complicated, since we can't allow checks just anywhere -- that would allow the implementation to introduce arbitrary race conditions into the program!
---
When an object is created with an explicit initial value, as in "X: T := ...;" or "new T'(...)", the predicate is checked. Without an explicit initial value, as in "X: T;" or "new T", we want to check the predicate if and only if the type has meaningful defaults. We define it like this:
- If T is elementary, the predicate is not checked.
- If T is composite, the predicate is checked only if there are default
values, indeed only for _explicit_ defaults -- the implicit default of null for access compnents doesn't count.
Examples:
subtype S is Integer range 1..10 with Static_Predicate => ...; X: S; -- neither constraint nor predicate is checked
The idea is that X will be initialized later, and the range and predicate will be checked at that time. It makes no sense to check the predicate on the declaration of X, since X will have some arbitrary junk (possibly invalid) value.
type T is access all String; subtype S is T with Dynamic_Predicate => S.all'First = 1; X: S; -- predicate is not checked Y: S := null; -- raises an exception
Same idea here; X will be initialized later. It makes no sense to check the predicate on the declaration of X, since X will be null, so evaluating "S.all'First = 1" would raise Constraint_Error, which is unhelpful. On the other hand, the predicate IS checked for Y, and will raise Constraint_Error.
Consider:
type Inner_Record is record A: Integer := ...; B: Some_Access := ...; end record; type Outer_Record is record Inner: Inner_Record; end record; subtype S is Outer_Record with Dynamic_Predicate => ...; X: S; -- predicate IS checked
But if we remove the explicit defaults for A and B, then the predicate would NOT be checked on the declaration of X -- like the simple integer case, the assumption is that X will be explicitly initialized later.
---
RM-3.2(8/2) says:
...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.
We considered changing it to:
...The set of values of a subtype consists of the values of its type that satisfy its constraint, any exclusion of the null value, and the predicate.
because conceptually, the values of the subtype include only values that obey the predicate, and indeed membership tests reflect that (X in T returns False if the predicate is False for X). This view makes sense for well-defined predicates. However, 13.9.1(2) says:
A scalar object can have an invalid representation, which means that the object's representation does not represent any value of the object's subtype.
and there are all kinds of permissions to check for invalid data. We don't want to allow optional evaluation of predicates in such cases. Anyway, an implementation can always have a mode where it does additional predicate checks. An implementation-defined assertion policy could be used for this.
However, we do say that the X'Valid is False if the predicate is False.
---
Note that overlapping subsets are allowed in the static case:
subtype S1 is Integer with Static_Predicate => S1 in 1..10; subtype S2 is Integer with Static_Predicate => S2 in 4..20; subtype S3 is Integer with Static_Predicate => S3 in S1 | S2; -- overlapping; same as 1..20
case ... is when S3 => -- OK
But:
case ... is when S1 | S2 => -- Still illegal!
----------------
We are deliberately vague about what "assertion policy in effect" means. In particular, about precisely WHERE in the source text it matters. We don't want to impose any implementation burden in this regard, since in practise, assertion policies will be determined rather globally, by compiler switches. Unlike for pragma Suppress, there is no compelling reason to nail this down, since there's no erroneousness involved in assertion policy => Ignore. In any case, it's not the job of THIS AI to worry about such matters.
!example
In a compiler familar to the author, type Symbol_Ptr references a symbol table entry. Most routines that take a symbol table entry only allow certain kinds of entry. It would be valuable to be able to specify those kinds of entry as part of the profile of the routine.
A simplified example:
type Entity_Kind is (Proc, Func, A_Type, A_Subtype, A_Package, An_Entry);
type Symbol_Record (Entity : Entity_Kind) is record ...
type Symbol_Ptr is access all Symbol_Record;
subtype Type_Symbol_Ptr is not null Symbol_Ptr with Dynamic_Predicate => Type_Symbol_Ptr.Entity = A_Type; subtype Callable_Symbol_Ptr is not null Symbol_Ptr with Dynamic_Predicate => Callable_Symbol_Ptr.Entity = Proc or Callable_Symbol_Ptr.Entity = Func or Callable_Symbol_Ptr.Entity = An_Entry;
function Type_Size (A_Type : Type_Symbol_Ptr) return Size_Type;
procedure Generate_Call_Parameters (Callee : Callable_Symbol_Ptr; ...);
Now, a call to Type_Size or Generate_Call_Parameters with a pointer to the wrong kind of symbol record will be detected at the call site rather than at some later point. The call site is closer to the source of the error; in addition, it is possible that the compiler can prove that the predicate will succeed and be able to remove the check altogether. That can't happen for a check inside of a subprogram.
Other examples of useful predicates:
If you plan to divide by X, its subtype should exclude zero.
An OS interface requires a size-in-bytes, but it must be a multiple of the page size.
Ada measures sizes in bits, but it's sometimes necessary to measure in storage units. "Dynamic_Predicate => Blah mod System.Storage_Unit = 0" might come in handy.
A Sort function produces an array (or other sequence) of subtype Sorted_Sequence. Binary_Search takes a parameter of that subtype. Very useful to keep track of which objects have been sorted (can I pass this to Binary_Search, or must I sort it first?).
To prevent SQL injection bugs, keep track of which data is "tainted" and which is "trusted", using predicates.
In a program that processes objects through multiple phases, you want to keep track of which phase(s) have been applied to each object, via subtypes.
Temporal logic: you can't land the airplane until the wheels are down. So Land_Airplane takes a parameter of subtype Airplane_That_Is_Ready_To_Land, which is a subtype of Airplane.
!corrigendum 3.2.4(0)
Insert new clause:
The language-defined predicate aspects Static_Predicate and Dynamic_Predicate may be used to define properties of subtypes. A predicate specification is an aspect_specification for one of the two predicate aspects.
Name Resolution Rules
The expected type for a predicate aspect expression is any boolean type.
Static Semantics
A predicate specification may be given on a type_declaration or a subtype_declaration, and applies to the declared subtype. In addition, predicate specifications apply to certain other subtypes:
The predicate of a subtype consists of all predicate specifications that apply, and-ed together; if no predicate specifications apply, the predicate is True (in particular, the predicate of a base subtype is True).
Legality Rules
The expression of a Static_Predicate specification shall be predicate-static; that is, one of the following:
An index subtype, discrete_range of an index_constraint or slice, or a discrete_subtype_definition of a constrained_array_definition, entry_declaration, or entry_index_specification shall not denote a subtype to which predicate specifications apply.
The prefix of an attribute_reference whose attribute_designator is First, Last, or Range shall not denote a scalar subtype to which predicate specifications apply.
The discrete_subtype_definition of a loop_parameter_specification or a discrete_choice of a named_array_aggregate shall not denote a subtype to which Dynamic_Predicate specifications apply.
Dynamic Semantics
If the assertion policy (see 11.4.2) in effect is Check, then:
On every subtype conversion, the predicate of the target subtype is evaluated, and a check is made that the predicate is True. This includes all parameter passing, except for certain parameters passed by reference, which are covered by the following rule: After normal completion and leaving of a subprogram, for each in out or out parameter that is passed by reference, the predicate of the subtype of the actual is evaluated, and a check is made that the predicate is True. For an object created by an object_declaration with no explicit initialization expression, or by an uninitialized allocator, if any subcomponents have default_expressions, the predicate of the nominal subtype of the created object is evaluated, and a check is made that the predicate is True. Assertions.Assertion_Error is raised if any of these checks fail.
If any of the above Legality Rules is violated in an instance of a generic unit, Program_Error is raised. In addition to the places where Legality Rules normally apply (see 12.3), this rule applies also in the private part of an instance of a generic unit.
NOTES
5 A predicate specification does not cause a subtype to be considered constrained.
6 A Static_Predicate, like a constraint, always remains True for all objects of the subtype, except in the case of uninitialized variables and other invalid values. A Dynamic_Predicate, on the other hand, is checked as specified above, but can become False at other times. For example, the predicate of a record is not checked when a subcomponent is modified.
!corrigendum 3.8.1(5)
Replace the paragraph:
discrete_choice ::= expression | discrete_range | others
by:
discrete_choice ::= choice_expression | discrete_subtype_indication | range | others
!corrigendum 3.8.1(8)
Replace the paragraph:
The expressions and discrete_ranges given as discrete_choices in a variant_part shall be static. The discrete_choice others shall appear alone in a discrete_choice_list, and such a discrete_choice_list, if it appears, shall be the last one in the enclosing construct.
by:
The choice_expressions, subtype_indications, and ranges given as discrete_choices in a variant_part shall be static. The discrete_choice others shall appear alone in a discrete_choice_list, and such a discrete_choice_list, if it appears, shall be the last one in the enclosing construct.
!corrigendum 3.8.1(11)
Replace the paragraph:
by:
!corrigendum 3.8.1(15)
Replace the paragraph:
by:
!corrigendum 4.3.3(17)
Replace the paragraph:
The discrete_choice_list of an array_component_association is allowed to have a discrete_choice that is a nonstatic expression or that is a discrete_range that defines a nonstatic or null range, only if it is the single discrete_choice of its discrete_choice_list, and there is only one array_component_association in the array_aggregate.
by:
The discrete_choice_list of an array_component_association is allowed to have a discrete_choice that is a nonstatic choice_expression or that is a subtype_indication or range that defines a nonstatic or null range, only if it is the single discrete_choice of its discrete_choice_list, and there is only one array_component_association in the array_aggregate.
!corrigendum 4.5.2(29)
Replace the paragraph:
by:
!corrigendum 4.5.2(30/2)
Replace the paragraph:
The tested type is not scalar, and the value of the simple_expression satisfies any constraints of the named subtype, and:
by:
!corrigendum 4.6(51/2)
Replace the paragraph:
After conversion of the value to the target type, if the target subtype is constrained, a check is performed that the value satisfies this constraint. If the target subtype excludes null, then a check is made that the value is not null.
by:
After conversion of the value to the target type, if the target subtype is constrained, a check is performed that the value satisfies this constraint. If the target subtype excludes null, then a check is made that the value is not null. If the assertion policy (see 11.4.2) in effect is Check, the predicate of the target subtype is applied to the value and Assertions.Assertion_Error is raised if the result is False.
!corrigendum 4.9(26)
Replace the paragraph:
A static subtype is either a static scalar subtype or a static string subtype. A static scalar subtype is an unconstrained scalar subtype whose type is not a descendant of a formal type, or a constrained scalar subtype formed by imposing a compatible static constraint on a static scalar subtype. A static string subtype is an unconstrained string subtype whose index subtype and component subtype are static, or a constrained string subtype formed by imposing a compatible static constraint on a static string subtype. In any case, the subtype of a generic formal object of mode in out, and the result subtype of a generic formal function, are not static.
by:
A static subtype is either a static scalar subtype or a static string subtype. A static scalar subtype is an unconstrained scalar subtype whose type is not a descendant of a formal type, or a constrained scalar subtype formed by imposing a compatible static constraint on a static scalar subtype. A static string subtype is an unconstrained string subtype whose index subtype and component subtype are static, or a constrained string subtype formed by imposing a compatible static constraint on a static string subtype. In any case, the subtype of a generic formal object of mode in out, and the result subtype of a generic formal function, are not static. Also, a subtype is not static if any Dynamic_Predicate specifications apply to it.
!corrigendum 4.9.1(2/2)
Replace the paragraph:
A subtype statically matches another subtype of the same type if they have statically matching constraints, and, for access subtypes, either both or neither exclude null. Two anonymous access-to-object subtypes statically match if their designated subtypes statically match, and either both or neither exclude null, and either both or neither are access-to-constant. Two anonymous access-to-subprogram subtypes statically match if their designated profiles are subtype conformant, and either both or neither exclude null.
by:
A subtype statically matches another subtype of the same type if they have statically matching constraints, all predicate specifications that apply to them come from the same declarations, and, for access subtypes, either both or neither exclude null. Two anonymous access-to-object subtypes statically match if their designated subtypes statically match, and either both or neither exclude null, and either both or neither are access-to-constant. Two anonymous access-to-subprogram subtypes statically match if their designated profiles are subtype conformant, and either both or neither exclude null.
!corrigendum 4.9.1(4)
Replace the paragraph:
A constraint is statically compatible with a scalar subtype if it statically matches the constraint of the subtype, or if both are static and the constraint is compatible with the subtype. A constraint is statically compatible with an access or composite subtype if it statically matches the constraint of the subtype, or if the subtype is unconstrained. One subtype is statically compatible with a second subtype if the constraint of the first is statically compatible with the second subtype.
by:
A constraint is statically compatible with a scalar subtype if it statically matches the constraint of the subtype, or if both are static and the constraint is compatible with the subtype. A constraint is statically compatible with an access or composite subtype if it statically matches the constraint of the subtype, or if the subtype is unconstrained.
Two statically matching subtypes are statically compatible with each other. In addition, a subtype S1 is statically compatible with a subtype S2 if:
!corrigendum 5.4(5)
Replace the paragraph:
The expressions and discrete_ranges given as discrete_choices of a case_statement shall be static. A discrete_choice others, if present, shall appear alone and in the last discrete_choice_list.
by:
The choice_expressions, subtype_indications, and rangess given as discrete_choices of a case_statement shall be static. A discrete_choice others, if present, shall appear alone and in the last discrete_choice_list.
!corrigendum 5.4(7)
Replace the paragraph:
by:
!corrigendum 6.4.1(13)
Replace the paragraph:
by:
!corrigendum 13.9.2(3)
Replace the paragraph:
X'Valid
Yields True if and only if the object denoted by X is normal and has a valid representation. The value of this attribute is of the predefined type Boolean.
by:

X'Valid
Yields True if and only if the object denoted by X is normal, has a valid representation, and the predicate of the nominal subtype of X evaluates to True. The value of this attribute is of the predefined type Boolean.
!ACATS test
Add ACATS B and C tests for this feature.
!appendix

From: Jean-Pierre Rosen
Sent: Thursday, December 23, 2010  10:01 AM

[Part of a message mostly about the minutes of meeting #42 - Editor]

- From AI05-0153-3(legality rules)

"An index subtype [...] shall not denote a subtype with a
user-specified predicate."
The two following paragraphs also refer to user-specified predicate.

This seems to be too narrow. Consider:
subtype S1 is Integer with Predicate S1 mod 2 = 0; subtype S2 is S1;

Is S2 a subtype with a user specified predicate? Hopefully
yes, but the formulation is not clear. The definition of a
predicate of a subtype implies that /part/ of a subtype
predicate can be user-specified.
Suggestion:
"... whose predicate includes parts that are user specified".

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

From: Bob Duff
Sent: Sunday, January 23, 2011  5:25 PM

New version of AI05-0153-3, Subtype predicates. [This is version /02 of
this AI. - Editor]
The big change is to split the Predicate aspect in two:
Static_Predicate and Dynamic_Predicate.

As you all know, I really HATE this "compromise".
It will certainly enhance Ada's well-deserved reputation for being overly
complicated!  :-(

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

From: Robert Dewar
Sent: Sunday, January 23, 2011  5:44 PM

> The big change is to split the Predicate aspect in two:
> Static_Predicate and Dynamic_Predicate.
>
> As you all know, I really HATE this "compromise".
> It will certainly enhance Ada's well-deserved reputation for being
> overly complicated!  :-(

I dislike it too! GNAT implements this, but under protest :-) and we still have
the simple Predicate aspect that encompasses both together, and intend to
maintain that implementation, so in practice I suspect people using GNAT will
likely use that rather than the split ones.

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

From: John Barnes
Sent: Monday, January 24, 2011  6:24 AM

Having missed the last meeting, I hadn't realised how messy these predicates
were going. And the dynamic ones sound really dodgy. Why don't we just get rid
of the dynamic version. Surely the static version is what people will find most
valueable. This just adds to the feeling that Ada is just as dodgy as other
languages. Yuk. I feel as if I am going to have to write a rationale that I just
don't believe in.

PS It is most unlikely that I will get to the Florida meeting. Although
improved, I am still not fully OK. (I haven't been fully OK for years but I am
sure you know what I mean!)

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

From: Robert Dewar
Sent: Monday, January 24, 2011  7:02 AM

I think the dynamic predicates are useful, something like

    subtype X is Integer with
      Predicate => Is_Prime (X),
      Default_Value => 1;

makes good sense to me!

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

From: John Barnes
Sent: Monday, January 24, 2011  6:57 AM

Having thought about it over lunch, I am changing my mind.

Since pre and postconditions can call any old stuff and so are as watertight as
a colander, the subtype predicates might as well be the same. So get rid of the
static ones.

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

From: Robert Dewar
Sent: Monday, January 24, 2011  7:12 AM

Well you need the special capabilities of static ones, to use them in membership
tests and case statements. This is the capability that provides non-contiguous
enumeration types, which to me is *the* most important capability.

   type Colors is (Red, Blue, Yellow, Green, .....)

   subtype RBG is Colors with
     Predicate => RBG in Red | Blue | Green;

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

From: Bob Duff
Sent: Monday, January 24, 2011  7:48 AM

> Having thought about it over lunch, I am changing my mind.

Hey, I see your health really IS improving today.  Good!
I'm glad your fever dreams regarding predicates have vanished.

> Since pre and postconditions can call any old stuff and so are as
> watertight as a colander, the subtype predicates might as well be the
> same. So get rid of the static ones.

Since you missed the last meeting, let me clue you in:
I strongly advocated having a single Predicate aspect, which can be used in case
statements and the like only if it obeys certain sort-of-staticness rules. [In
fact, I was already annoyed that we have predicates, invariants, constraints,
and null exclusions, all of which are the same thing -- as everybody would see
if I could get them to remove their Language Lawyer Hats for just a moment!
Language Lawyer Blindfolds?]

Others were nervous about the colander-like aspects of this aspect.  Giving the
colander-like ones a different name (Dynamic_Predicate) was a compromise to make
those people less nervous.  Tucker bullied me incessantly during the meeting,
until I finally agreed to it.  ;-)

Although Static_Predicate is the more useful of the two, I'm firmly convinced
that the dynamic ones are necessary. Everybody agrees that we want
non-contiguous enums. But as soon as you have that, you will certainly want to
constrain discriminants of that enum type in the same way.

Please don't worry about "dodginess".  Nobody is forcing, or even encouraging,
anyone to write dodgy predicates.  Just don't do that.

I can give you plenty of non-dodgy examples for your Rat, by the way.

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

From: John Barnes
Sent: Monday, January 24, 2011  7:52 AM

Why can't the one predicate do both?

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

From: Bob Duff
Sent: Monday, January 24, 2011  8:17 AM

> Why can't the one predicate do both?   John

Because that will cause Randy and others to "snap", and we won't have this
extremely useful feature at all.

To understand that point of view, consider this analogy:
Why can't we have a single feature that does what type conversions do, and also
does what Unchecked_Conversions do? Well, because one is more dangerous, so it's
a good idea to have separate syntax.

Consider C:  some casts are extremely dangerous, and others are relatively
innocuous, and it's hard to tell which is which by reading the code.

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

From: Tucker Taft
Sent: Monday, January 24, 2011  8:17 AM

> New version of AI05-0153-3, Subtype predicates.
> The big change is to split the Predicate aspect in two:
> Static_Predicate and Dynamic_Predicate.
>
> As you all know, I really HATE this "compromise".
> It will certainly enhance Ada's well-deserved reputation for being
> overly complicated!  :-( ...

There was a tremendous amount of discussion which led up to this compromise.
Unfortunately, reopening such discussions can waste a lot of time, unless there
is some new information.

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

From: Bob Duff
Sent: Monday, January 24, 2011  8:29 AM

> There was a tremendous amount of discussion which led up to this
> compromise.  Unfortunately, reopening such discussions can waste a lot
> of time, unless there is some new information.

I'm not reopening anything.  I'm just venting my frustration.

John wasn't present for those discussions, so I've tried to bring him up to
speed.  As far as I'm concerned, the issue is settled.

But I'm not like Robert, who thinks that if lots of smart people believe the
wrong thing, it must therefore be the right thing.

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

From: Bob Duff
Sent: Monday, January 24, 2011  8:21 AM

By the way, if I had to choose just one AI for Ada 2012, with all the others
rejected, subtype predicates would be the one.  It's that useful.

And that usefulness comes from its generality.  It's simply impossible to plug
all the holes in the colander without severely damaging the feature.  Plugging
just some holes is pointless.

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

From: Tucker Taft
Sent: Monday, January 24, 2011  8:25 AM

> Why can't the one predicate do both? John

The issue here is maintenance.  With just one aspect, a small change can
dramatically affect where the subtype can be used, and that might not be
detected until much later.  If the code where the predicate is specified is
compiled at one time, and the code where the subtype is used is compiled much
later, by a different developer, then it could be very painful.

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

From: Bob Duff
Sent: Monday, January 24, 2011  8:31 AM

An obviously-bogus argument, as I explained at the meeting, and also in the AI.

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

From: Tucker Taft
Sent: Monday, January 24, 2011  8:27 AM

> Because that will cause Randy and others to "snap", and we won't have
> this extremely useful feature at all.

I think maintenance issues were underlying Randy's concern, as I mentioned in my
prior response.

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

From: Robert Dewar
Sent: Monday, January 24, 2011  9:00 AM

But don't worry too much, in the forseeable future only GNAT will implement Ada
2012 and there you will have one predicate that does both :-)

> Because that will cause Randy and others to "snap", and we won't have
> this extremely useful feature at all.

And of course it will be just fine to have coding standards forbidding the use
of the Predicate aspect in GNAT.

P.S. should we have a restriction

No_Implementation_Aspects

Seems like we should, I think I will implement that in GNAT in any case.

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

From: Robert Dewar
Sent: Monday, January 24, 2011  9:01 AM

> By the way, if I had to choose just one AI for Ada 2012, with all the
> others rejected, subtype predicates would be the one.  It's that
> useful.
>
> And that usefulness comes from its generality.  It's simply impossible
> to plug all the holes in the colander without severely damaging the
> feature.  Plugging just some holes is pointless.

I fully agree!

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

From: Robert Dewar
Sent: Monday, January 24, 2011  9:05 AM

> I think maintenance issues were underlying Randy's concern, as I
> mentioned in my prior response.

Right, the argument is something like

static predicates: good, easy to maintain, useful etc.

dynamic predicates: bad, hard to maintain, potentially expensive etc.

But if you separate them into two aspects, then I can easily have coding
standards forbidding or limiting the bad, without affecting the good.

A perfectly reasonable argument, not one I ultimately agree with, but I am happy
with the AI the way it is separating these, given that I can still implement the
more general Predicate aspect encompassing them both in GNAT, and furthermore
this extension does not create problems for those who agree with the argument
above.

If you find Dynamic_Predicate dangerous and want to restrict its use, then you
just do the same with Predicate.

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

From: Robert Dewar
Sent: Monday, January 24, 2011  9:07 AM

> But I'm not like Robert, who thinks that if lots of smart people
> believe the wrong thing, it must therefore be the right thing.

That's not quite the robert philosophy, which goes like this

If you believe that X is correct, but the majority overrules you in a smart
group of people like the ARG then either

a) you are wrong, and X is not correct

b) you are right, but you are incompetent at presenting your argument
   sufficiently convincingly.

:-) :-)

In either case, no point in holding on to the minority view point :-)


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

From: Randy Brukardt
Sent: Monday, January 24, 2011  9:29 PM

> Because that will cause Randy and others to "snap", and we won't have
> this extremely useful feature at all.
>
> To understand that point of view, consider this analogy:
> Why can't we have a single feature that does what type conversions do,
> and also does what Unchecked_Conversions do?
> Well, because one is more dangerous, so it's a good idea to have
> separate syntax.
>
> Consider C:  some casts are extremely dangerous, and others are
> relatively innocuous, and it's hard to tell which is which by reading
> the code.

I hope it doesn't cause me to "snap" (although you never know... :-).

At the risk of prelonging a discussion that is almost over, let me explain my
position a bit.

A static predicate, to me, is really a kind of constraint. (I would have
preferred that it be treated that way, but no need to go there.) In particular,
all of the properties that scalar constraints have also hold for static
predicates. That means that, once checked, such a predicate holds for an object
until it is assigned again. (And presumably, the assignment check will again
check it, so it will still be in range.) That means that they can be included in
reasoning about the semantics of a particular object. In addition, you can use
them the same ways in case statements and loops.

OTOH, a dynamic predicate is really a kind of Assert pragma (automatically
inserted). Like all assert pragmas, the predicate can only be assumed true at
the point at which it is checked. (And, unlike an assert pragma, it's harder to
figure out where those points are.) That means that you have to be very careful
when including these in reasoning about your program. Moreover, even predicates
that "look" like they hold for the life of an object might not for composite
objects (as they are not checked when individual components are changed).

I wouldn't want to claim that dynamic predicates aren't useful, just that they
need a different approach when thinking about the effect on program semantics.
And that need is best handled by some sort of differentiation between the two,
especially for the human readers that need to do program reasoning (which is
most of them).

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

From: Jean-Pierre Rosen
Sent: Tuesday, January 25, 2011  12:38 AM

> And that need is best handled by some sort of differentiation between
> the two, especially for the human readers that need to do program
> reasoning (which is most of them).
            ^^^^^^^^^^^^^^^^^^^^^^^
Alas, wishful thinking!
(sorry, couldn't resist)

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

From: Randy Brukardt
Sent: Tuesday, January 25, 2011  12:49 AM

[Specific wording comments here, no political discussion.]

Bob Duff writes:
...
> The expression of a Static_Predicate clause shall be
> "predicate-static"; that is, one of the following:
>
>     - a static expression that does not raise any exception;
>
>     - a membership test whose left-hand side is the current instance,
>       and whose right-hand side is static; ???Does that allow "S in
> (Foo | Bar | Baz)"?

No, because the above isn't syntactally correct :-) (no parens needed). And
still no even with the parens removed; the right-hand side here is not an
expression at all, but just a list of choices. It can't be static by itself. You
probably want to borrow the 4.9(13) wording for memberships:

...and whose membership_choice_list consists only of membership_choices each of
which is either a static choice_expression, a static range, or a subtype_mark
that denotes range is a static range or whose subtype_mark denotes a static
[(scalar or string)] subtype;

Probably there is some way to simplify this, but I'll leave that as an exercise
for the author.

> NOTE: A predicate is not necessarily True for all objects of the
> subtype at all times. Predicates are checked as specified above, but
> can become False at other times. For example, the predicate of a
> record is not checked when a component is modified. Similarly to
> constraints, predicates can be False for uninitialized variables and
> other invalid values.

I would have thought that this note would only apply to Dynamic_Predicates. The
only time it could apply for Static_Predicates is for uninitialized values, and
that doesn't seem to be worth a note -- it's inclusion in the note mainly seems
to be to somehow justify making the bogus claim that these are not different in
how they work. And I don't think it is possible for an non-erroneous program to
have a Static_Predicate become False for an object for which it previously was
True. So most of the note seems to imply that Static_Predicates are no better
than their dynamic brethren, which is baloney. (The last sentence is fine, of
course I would think it would be a good idea for the *real* difference between
the kinds of predicates to be explained here, otherwise it might be too
mysterious. Perhaps something like:

NOTE: A Dynamic_Predicate is not necessarily True for all objects of the subtype
at all times. Dynamic_Predicates are checked as specified above, but can become
False at other times. For example, the predicate of a record is not checked when
a component is modified. In contrast, in the absence of erroneous execution or
uninitialized variables and other invalid values, a Static_Predicate (like a
constraint) will remain True all of the time.

[Sorry, didn't realize that there was a political note in the wording when I put
the "no political discussions" banner at the top.]

...
> Modify 4.9.1(4/3), so "statically compatible" takes predicates into
> account:
>
>   A constraint is statically compatible with a scalar subtype if it statically
>   matches the constraint of the subtype, or if both are static and the
>   constraint is compatible with the subtype.  A constraint is statically
>   compatible with an access or composite subtype if it statically matches the
>   constraint of the subtype, or if the subtype is unconstrained.  One subtype
>   is statically compatible with a second subtype if the constraint of the first
>   is statically compatible with the second subtype, and in the case of an
>   access type, if the second subtype excludes null, then so does the first.
>   {Also, if either subtype has a user-defined predicate, then the first is
>   statically compatible with the second only if both subtypes are static, and
>   every value that obeys the predicate of the first obeys the predicate of the
>   second.}
>???Is that reasonable to implement?

Since the subtypes are static, this is just a set comparison, and the sets are
static. So that shouldn't be a problem. It should be possible to turn any
Static_Predicate (including those with comparison and boolean operators) into a
set representation, and then a simple compare should give the answer. If you
couldn't convert to a set, you couldn't test case completeness, so I think it
has to be doable and you'll have to do it for case statements even if we didn't
require it here (so doing so here won't add any cost).

> !discussion
>
> ???Much of this discussion probably belongs in the AARM!

Well, since AI authors are supposed to propose AARM notes, we know who should
have done that. :-) I'd certainly appreciate it if you did suggest the notes
that you think are necessary (and where they should go).

> ----------------
>
> An earlier version of this AI proposed a single Predicate aspect,
> which could allow static subtypes or not, depending on whether the
> expression happened to be predicate-static. We decided to split it
> into two aspects, Static_Predicate and Dynamic_Predicate, because
> otherwise, if you change a static predicate to a nonstatic one,
> faraway parts of your program can become illegal.
>
> The following arguments against the split were rejected:
>
>     - They won't change their run-time behavior, just become illegal.
>
>     - Changing the VALUES can have the same effect, so different
>       syntax doesn't really solve the problem.  (E.g. "Cur_Inst
>       in 1..10" changed to "Cur_Inst in 1..10 | 20".)
>
>     - We already have this "problem" for other static things
>       (changing "subtype S is Integer range 1..10" to
>       "1..Non_Static" or "1..11" can cause faraway
>       illegalities).
>
>     - Although it might be mildly useful, we don't say
>       "C: static constant Integer := ...", so why should we
>       do so for predicates?

It would be nice to say more in *favor* of the split as well; the text seems (to
me at least) to be biased against the solution we chose. I realize that it is
asking a lot of you to provide those arguments, as you don't believe in them.
I'll help you do it if needed.

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

From: Bob Duff
Sent: Tuesday, January 25, 2011   10:07 AM

> It would be nice to say more in *favor* of the split as well; the text
> seems (to me at least) to be biased against the solution we chose.

Indeed, it is biased in that direction.

>..I realize that
> it is asking a lot of you to provide those arguments, as you don't
>believe  in them. I'll help you do it if needed.

I can cut&paste your other e-mail (the one that mentions snapping) as a
counter-argument.

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

From: John Barnes
Sent: Wednesday, January 26, 2011   7:57 AM

I have lost track of this topic slightly.

If we have to have two and the static one is just like the dynamic one but
requires the stuff to be static then why don't we call them Subtype_Predicate
and Static_Subtype_Predicate.

Without Subtype it is not so clear what they refer to.

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

From: Bob Duff
Sent: Wednesday, January 26, 2011   8:11 AM

> I have lost track of this topic slightly.
>
> If we have to have two and the static one is just like the dynamic one
> but requires the stuff to be static

That's one difference.  The other difference is that the static ones are allowed
in more places (e.g. in case stms).

>...then why don't we call them
> Subtype_Predicate and Static_Subtype_Predicate.
>
> Without Subtype it is not so clear what they refer to.

    subtype Nonzero is Integer with Static_Predicate => Nonzero /= 0;

It seems pretty clear from the syntax what the predicate refers to!

I think adding "Subtype_" is just extra noise.
The names are too long as it is.

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

From: Yannick Moy
Sent: Wednesday, January 26, 2011   8:48 AM

>> Without Subtype it is not so clear what they refer to.
>
>     subtype Nonzero is Integer with Static_Predicate => Nonzero /= 0;
>
> It seems pretty clear from the syntax what the predicate refers to!
>
> I think adding "Subtype_" is just extra noise.
> The names are too long as it is.

plus it would be confusing when the predicate aspect is applied to a type
definition, I think:

  type Nonzero_Small is range -10 .. 10 with
    Subtype?_Static_Predicate => Nonzero_Small /= 0;

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

From: Tucker Taft
Sent: Wednesday, January 26, 2011   9:33 AM

I think the difference is bigger than what you imply.

Dynamic_Predicates aren't reevaluated every time they might become false,
whereas Static_Predicates are designed so that (barring erroneous execution)
they are rechecked at every point where they might become false.

So Dynamic_Predicates are sort of like assertions that are periodically
rechecked, while a Static_Predicate is something that is continuously True.

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

From: Robert Dewar
Sent: Wednesday, January 26, 2011  10:31 AM

> plus it would be confusing when the predicate aspect is applied to a
> type definition, I think:
>
>    type Nonzero_Small is range -10 .. 10 with
>      Subtype?_Static_Predicate =>  Nonzero_Small /= 0;

Right, I agree, in the above, Nonzero_Small is technically a subtype name, but
real programmers consider it a type name :-)

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

From: Bob Duff
Sent: Wednesday, January 26, 2011  10:41 AM

> So Dynamic_Predicates are sort of like assertions that are
> periodically rechecked, while a Static_Predicate is something that is
> continuously True.

That's not quite true.  I suppose you could say it's almost true.  ;-) It's as
true for static predicates as it is for constraints. And you're right that it's
less true for dynamic predicates that for static predicates and constraints.

    subtype S is Integer range -10..10 with Static_Predicate => S /= 0;

    X : S;
    Y : S := 1; -- (1)

    Y := X; -- (2)

The constraint and predicate of Y are both true at (1), but either could become
false at (2).  This is of course a bounded error, but it's not quite erroneous.

The AI allows to omit the predicate check at (2), but I'm not sure I got the
wording right.  I wanted to defer arguing about that until after we agree on the
other (more important) rules.

In any case, I think it's important to keep the "invalid data"
loophole in mind, when arguing about whether the sky is falling or the colander
is leaky or whatever.

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

From: Randy Brukardt
Sent: Wednesday, January 26, 2011   5:19 PM

> The constraint and predicate of Y are both true at (1), but either
> could become false at (2).  This is of course a bounded error, but
> it's not quite erroneous.

Your point is technically correct, but this example doesn't illustrate it very
well. Virtually every compiler implementation has some concept like "known to be
valid". For any object that is "known to be valid", checks on assignment can
only be eliminated if the source is also "known to be valid" (otherwise the
property is a lie). In this example, Y is "known to be valid" in Janus/Ada (and
I would expect in most other compilers). The reason for the property is so that
checks can be eliminated on use; array and case checks, for example, can never
be eliminated unless the source object is "known to be valid" (since eliminating
the checks would change from a bounded error to erroneous execution, which is
not allowed).

So I would consider any implementation that removed the checks at (2) broken, in
a practical if not language lawyer sense. (It's also *very* user-unfriendly.)
[All of the above is assuming no pragma Suppresses and no erroneous execution,
of course.]

However, if you make the example more complex, the issue becomes murkier.
Janus/Ada is very syntax-based, and thus just moving the initialization changes
the "known to be valid" property:

      X, Y : S;

      Y := 1; -- (1)
      Y := X; -- (2)

Y is not "known to be valid", so the checks at (2) aren't generated unless the
user has set strict checking mode.

A static_predicate will follow the same exact model for checking and checking
elimination in Janus/Ada (and I would expect other compilers as well). I'm not
sure about dynamic_predicates; I would guess that eliminating them would be a
serious mistake unless the compiler can prove no side-effects (often hard).

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

From: Robert Dewar
Sent: Wednesday, January 26, 2011   5:41 PM

> So I would consider any implementation that removed the checks at (2)
> broken, in a practical if not language lawyer sense. (It's also *very*
> user-unfriendly.) [All of the above is assuming no pragma Suppresses
> and no erroneous execution, of course.]

You can consider what you like, but the language quite deliberately does NOT
require a check here, and I personally would consider any compiler which always
did the check here as broken. Certainly GNAT will NOT do the check by default
(though it can be forced on with full non-standard validity checking).

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

From: Tucker Taft
Sent: Wednesday, January 26, 2011   6:18 PM

There seem to be (at least) two basic strategies for dealing with uninitialized
variables in Ada 95+:

One approach deals with the potential for invalid values on the few uses where
they can turn into erroneous execution, such as array indexing and case
statements.  The other approach has the notion of objects whose subtypes can be
"trusted" and objects whose subtypes cannot be trusted.  With this latter
approach, when assigning from an "untrusted" object to a "trusted" object, you
always do a check.

Either approach can work, and I don't consider either approach "broken."  I
believe GNAT takes the first approach by default, but can be convinced to take
one more nearly approximating the second approach. AdaMagic (and it sounds like
Janus/Ada) takes the second approach, or something close to it.

We should try to keep these two approaches in mind rather than making overly
general statements about how code involving uninitialized variables should be
compiled.

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

From: Robert Dewar
Sent: Wednesday, January 26, 2011   6:30 PM

Fair enough!

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

From: Randy Brukardt
Sent: Wednesday, January 26, 2011   9:17 PM

I apologize for using an inflamatory word like "broken" in relationship to a
particular compiler. It's unfair mainly because the problem is with the language
and not the compiler.

The only people who ought to have to even consider the effect of uninitialized
variables in code are language lawyers and compiler implementers. To the extent
that that is not true, it is the language, and not any specific implementation,
that is broken.

It is very unfriendly to the user to allow values that are out of range to be
assigned to objects. Period. We allow that for code efficiency reasons, of
course, but that also makes it far harder for the user to understand their
programs.

To the extent possible, checks should be made as early as possible, and should
be as close as possible to the canonical semantics. The "trusted" approach (as
Tucker called it) does this better (IMHO) than any other approach. And I think
compilers always should go for user-friendliness when the choice of two nearly
equal approaches occur.

But of course there are other considerations as well. And the real issue is that
the language allows unfriendly approaches in the first place.

In any case, all of this is not relevant to any current discussion. So let's
drop it here.

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

From: Tucker Taft
Sent: Thursday, February 10, 2011  2:01 PM

[Refering to version /04.]

> There are two predicate aspects: Static_Predicate and Dynamic_Predicate.
> Static_Predicates must obey certain restrictions, and the subtype can
> be static, so it be used as a choice in case statements and the like.

              ^^^ "can"

...

> NOTE: Similarly to constraints, a Static_Predicate is always True for
> all objects of the type, except in the case of uninitialized variables
> and other invalid values. A Dynamic_Predicate, on the other hand, is
> checked as specified above, but can become False at other times. For
> example, the predicate of a record is not checked when a subcomponent is
> modified.

I find this NOTE pretty confusing.  How about:

   NOTE: Similarly to constraints, a Static_Predicate is checked in enough
   contexts to ensure that it is not violated by any object of the subtype,
   except in the case of uninitialized variables and other invalid values. A
   Dynamic_Predicate, on the other hand, is checked only as specified above, but
   can become False at other times. For example, the Dynamic_Predicate of a
   record is not checked when a subcomponent is modified.

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

From: Bob Duff
Sent: Thursday, February 10, 2011  2:10 PM

> I find this NOTE pretty confusing.

Please explain why.  I find it crystal clear (but I WOULD say that, wouldn't I?
;-))

> ...How about:
>
>    NOTE: Similarly to constraints, a Static_Predicate is checked in enough contexts
>    to ensure that it is not violated by any object of the subtype, except in the
>    case of uninitialized variables and other invalid values. A Dynamic_Predicate,
>    on the other hand, is checked only as specified above, but can become
>    False at other times. For example, the Dynamic_Predicate of a
>    record is not checked when a subcomponent is modified.

I find this version confusing, because the issue isn't where they are checked,
as it seems to imply.  The thing that makes Static_Predicates less colander-like
is the predicate-static restrictions.

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

From: Tucker Taft
Sent: Thursday, February 10, 2011  2:28 PM

>> I find this NOTE pretty confusing.
>
> Please explain why.  I find it crystal clear (but I WOULD say that,
> wouldn't I?  ;-))

A Static_Predicate is an expression associated with a particular subtype of a
type, so at a minimum it seems we would want to say:

   ... a Static_Predicate always evaluates to True
       for every object of the subtype ...

Saying a Static_Predicate is True, to me can easily be interpreted as saying
that the aspect is specified to be the literal "True." And very importantly,
this is a subtype predicate, not a type predicate.

>
>> ...How about:
>>
>>     NOTE: Similarly to constraints, a Static_Predicate is checked in enough contexts
>>     to ensure that it is not violated by any object of the subtype, except in the
>>     case of uninitialized variables and other invalid values. A Dynamic_Predicate,
>>     on the other hand, is checked only as specified above, but can become
>>     False at other times. For example, the Dynamic_Predicate of a
>>     record is not checked when a subcomponent is modified.
>
> I find this version confusing, because the issue isn't where they are
> checked, as it seems to imply.  The thing that makes Static_Predicates
> less colander-like is the predicate-static restrictions.

It is a combination of the fact that they are checked in all the necessary
contexts (those that can create or modify the value), and they can't refer to
other variables and other nasty stuff.

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

From: Bob Duff
Sent: Thursday, February 10, 2011  3:11 PM

> >>> NOTE: Similarly to constraints, a Static_Predicate is always True
> >>> for all objects of the type, except in the case of uninitialized
> >>> variables and other
                  SUBtype!

...

>    ... a Static_Predicate always evaluates to True
>        for every object of the subtype ...
>
> Saying a Static_Predicate is True, to me can easily be interpreted as
> saying that the aspect is specified to be the literal "True."

I don't think that's a likely misinterpretation.  I suppose I could tolerate
"evaluates to True" instead of "is True", but it seems a little misleading: the
point is that the predicate remains true even at points in the code where it is
NOT supposed to be evaluated.

Or how about, "is always True" --> "always remains True"?

What do others think?

> And very importantly, this is a subtype predicate, not a type predicate.

Yes, you're 100% correct about that!  I don't know why I wrote "type" when I
meant "subtype".

...
> It is a combination of the fact that they are checked in all the
> necessary contexts (those that can create or modify the value), and
> they can't refer to other variables and other nasty stuff.

I suppose so, but your version seems to imply that Static_Predicates are checked
more often than Dynamic_Predicates, which isn't true.

I was told in the phone meeting that the purpose of this NOTE is to sing the
praises of Static_Predicates, which are gloriously good just like constraints,
and denigrate the colander-like evils of Dynamic_Predicates.  That is, to
compare/contrast the two.

I think it's better not to explain WHY (too complicated), but just state the
facts (static ones can be trusted (modulo invalid values), whereas dynamic ones
can't).

So I propose to fix my "type" --> "subtype", but otherwise leave my wording
alone.

Opinions?

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

From: Tucker Taft
Sent: Thursday, February 10, 2011  3:28 PM

> Or how about, "is always True" -->  "always remains True"?
>
> What do others think?

I prefer "always remains True".  It avoids saying "is True" which at least to me
was misleading, since the predicate is an expression, not a simple value.  This
is particularly important because other aspects *are* simple values (like 'Size,
'Low_Order_First, etc.).

> So I propose to fix my "type" -->  "subtype", but otherwise leave my
> wording alone.
>
> Opinions?

As indicated above, I would prefer to get rid of the "is always True" phrase
somehow.

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

From: Bob Duff
Sent: Thursday, February 10, 2011  3:32 PM

OK, "is always True" -->  "always remains True", and  "type" -->  "subtype",
resulting in:

    NOTE: Similarly to constraints, a Static_Predicate always remains True for
    all objects of the subtype, except in the case of uninitialized variables
    and other invalid values. A Dynamic_Predicate, on the other hand, is checked
    as specified above, but can become False at other times. For example, the
    predicate of a record is not checked when a subcomponent is modified.

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

From: Randy Brukardt
Sent: Thursday, February 10, 2011  11:18 PM

...
> OK, "is always True" -->  "always remains True", and  "type"
> -->  "subtype", resulting in:

I've inserted this into the "master" AI.

>     NOTE: Similarly to constraints, a Static_Predicate always remains True for all
>     objects of the subtype, except in the case of uninitialized variables and other
>     invalid values. A Dynamic_Predicate, on the other hand, is checked as specified
>     above, but can become False at other times. For example, the predicate of a
>     record is not checked when a subcomponent is modified.

But I have a nit-pick: I've always found it strange that this note starts with
"Similarly". It's jarring, because that is the sort of sentence that you'd
expect in the middle of a paragraph, not starting one. And you have to read
halfway through before you find out what it is about. There is also a mismatch
between the plural "constraints" and the singular "a Static_Predicate". I
haven't mentioned it before because I didn't have a great idea for a
replacement.

Perhaps:

   NOTE: A Static_Predicate always remains True for all objects of the subtype,
   except in the case of uninitialized variables and other invalid values; this
   is similar to the behavior of a constraint. A Dynamic_Predicate, on the other
   hand, is checked as specified above, but can become False at other times. For
   example, the predicate of a record is not checked when a subcomponent is
   modified.

Or more informal:

   NOTE: Like a constraint, a Static_Predicate always remains True for all
   objects of the subtype, except in the case of uninitialized variables and
   other invalid values. A Dynamic_Predicate, on the other hand, is checked as
   specified above, but can become False at other times. For example, the
   predicate of a record is not checked when a subcomponent is modified.

Or:

   NOTE: A Static_Predicate, like a constraint, always remains True for all
   objects of the subtype, except in the case of uninitialized variables and
   other invalid values. A Dynamic_Predicate, on the other hand, is checked as
   specified above, but can become False at other times. For example, the
   predicate of a record is not checked when a subcomponent is modified.

[or replace "like a constraint" with "similar to a constraint" to be a bit more
formal.]

I think I like the last best - it puts the most important thing first, but still
leaves the constraint part up front. A few more commas than I like, though. Any
thoughts??

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

From: Tucker Taft
Sent: Friday, February 11, 2011  9:19 AM

Your third one seems fine to me.

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

From: Bob Duff
Sent: Friday, February 11, 2011  1:47 PM

> ...
> > OK, "is always True" -->  "always remains True", and  "type"
> > -->  "subtype", resulting in:
>
> I've inserted this into the "master" AI.

Thanks.

[3 suggestions]

Any of those 3 are fine with me.

> [or replace "like a constraint" with "similar to a constraint" to be a
> bit more formal.]

Nah, I prefer the 3 as written.

> I think I like the last best - it puts the most important thing first,
> but still leaves the constraint part up front. A few more commas than
> I like, though. Any thoughts??

I agree -- I prefer the 3rd one.

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

From: Steve Baird
Sent: Thursday, February 10, 2011  2:51 PM

> When the Dynamic Semantics calls for a check of a value against a
> Static_Predicate, the check may be omitted if every value that obeys
> the Static_Predicates of the nominal subtype of the value also obeys
> the Static_Predicate being checked against.

Do we need any permission at all here?

With Static_Predicates, the check either passes or fails, but it cannot have
other side effects.

Dynamic_Predicates are different (removing a dynamic predicate check would
indeed require explicit permission) but we are not discussing those here (as of
today - see previous version of the AI).

Thus, do we need an explicit permission to omit a check which can only fail in
the case of an invalid value? We don't have such an explicit permission for a
constraint check (do we?); it just falls out from the rules for dealing with
invalid values.

How is the situation here any different?

P.S. I like your treatment of "is statically compatible".

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

From: Bob Duff
Sent: Thursday, February 10, 2011  3:00 PM

> How is the situation here any different?

I would be very happy to get rid of that para, and put something in the AARM,
like:

    Static_Predicate checks can be removed even in the presence
    of potentially invalid values, just as contraint checks can
    be removed.

> P.S. I like your treatment of "is statically compatible".

Good to know.  I rewrote it about 50 times before I was satisfied!

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

From: Steve Baird
Sent: Thursday, February 10, 2011  3:13 PM

Sounds good to me (now that we are only talking about static predicates).

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

From: Tucker Taft
Sent: Thursday, February 10, 2011  3:17 PM

I don't think we want this permission.
This is a very complicated area, and compilers have different strategies for
dealing with invalid values.  Omitting such a check presumes that doing so is
consistent with the overall strategy of not allowing an invalid value to send
things into erroneous land.  For example, if the compiler is making assumptions
elsewhere that a particular object satisfies the predicate, and the execution
would be erroneous if that turns out to be false, then it had better not
eliminate checks in certain cases.

You might be able to derive that even in the presence of this permission, but
this permission sounds pretty much like a blanket permission, and I am fairly
sure that with AdaMagic's approach to handling invalid values, things would go
haywire if we "obeyed" the implementation permission.

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

From: Bob Duff
Sent: Thursday, February 10, 2011  3:48 PM

> I don't think we want this permission.

Fine with me!

No such permission can be necessary in the Standard, because:

    - If you want the utmost efficiency, you can always turn
      off the checks by using Assertion_Policy.

    - If you want something in between super-efficient and full-checking,
      tell your friendly neighborhood compiler writer to implement
      an impl-def policy (or a mode switch) that does what you want.

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

From: Randy Brukardt
Sent: Thursday, February 10, 2011  11:31 PM

> You might be able to derive that even in the presence of this
> permission, but this permission sounds pretty much like a blanket
> permission, and I am fairly sure that with AdaMagic's approach to
> handling invalid values, things would go haywire if we "obeyed" the
> implementation permission.

I agree that we don't want the permission -- because it isn't necessary.

But this comment confuses me. This is an Implementation PERMISSION -- no one is
forcing you to follow it. If omitting it screws up your object validity model,
then *don't do that*.

It would be different if there was some requirement to omit the check, but there
is no such thing here.

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

From: Randy Brukardt
Sent: Thursday, February 10, 2011  11:33 PM

I've removed the permission from the "master copy" of the AI.

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

From: John Barnes
Sent: Wednesday, February 16, 2011  4:07 AM

I am sorry not to be with you again at the meeting in sunny Florida.
Although improving, I am still very reluctant to fly. I am especially annoyed at
missing the opportunity to see the new Dali museum.

In my absence, Jeff Cousins is taking my place. I am sure I will see you all in
Edinburgh.  Meanwhile, please read the following:

As you will have perceived from reading the latest draft of the Rationale
I am unhappy with two areas of Ada 2012. One is some aspects of
aspects (groan); the other is subtype predicates..

[For the aspect part of the discussion, see AI05-0229-1.]

Subtype predicates

I am very surprised at where we currently stand on subtype predicates.
Namely Static_Predicate which can be used in contexts such as loops, and
Dynamic_Predicate which is more general and cannot.

I understand that the reason given for the fact that a seemingly static
predicate such as in

subtype Even is My_Integer
   with Static_Predicate => Even mod 2 = 0;

is actually not allowed is that an implementation might want to compute and
hold all the allowed values of such a subtype as a sort of set.

The consequences seem foolish. I would expect to be allowed to write

   for E in Even loop ...

especially if My_Integer was not an overwhelming range.

The problem seems to me to be twofold.

First there is the fundamental problem that Ada does not support Sets.
Neither finite sets nor (thankfully?) infinite sets. I recall that many
years ago (long before Ada 83) there was a proposal for unordered
enumeration types which might have formed the foundation for sets. These
were abandoned.

Note that there is an inkling of this in Ada already since Integer'Base is
considered to be unconstrained - and thus almost represents an infinite set.

In the example to hand it would be appropriate if an implementation recorded
 an infinite set as a rule and a finite set as a collection of values. If
the predicate Even is applied to a finite set then clearly a loop could be
compiled as an iteration over the elements of the set. However, if the
predicate Even is applied to an effectively infinite set such as Integer
then the loop can be compiled with a test as if written

for X in Integer loop
   if X mod 2 = 0 then
      ...-- body of loop
   end if;
end loop;



It would perhaps be excellent if Ada did support sets as a real feature.
It might well improve Ada's perception as a good foundation vehicle for
teaching about discrete mathematics in CS degree classes.

However, to put sets into Ada is clearly not a task for this revision. We
need a proper direction to do so and this perhaps could be an objective for
Ada 2020.

Second, there is the problem (for me anyway) that I think of Integer as
really an infinite set. (I see I am repeating myself.) It is an unfortunate
fact that for implementation reasons we have to put limits on Integer.
Taking this infinite view one might want to forbid

   for I in Integer loop

but clearly it is too late for that.

In the absence of sets, I believe we should abandon the subdivision of
subtype predicates into dynamic and static forms. They introduce a whole lot
of new rules for the restricted form of expression allowed in a
Static_Predicate which make the language gross and is liable to confuse
users. In any event the choice of names is misleading.

We should revert to the one predicate, Subtype_Predicate and perhaps
restrict its use so that it cannot be applied to the (effectively)
unconstrained types such as Integer, Long_Integer and so on.

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

From: Robert Dewar
Sent: Wednesday, February 16, 2011  7:11 AM

> I am very surprised at where we currently stand on subtype predicates.
>
> Namely Static_Predicate which can be used in contexts such as loops,
> and Dynamic_Predicate which is more general and cannot.
>
> I understand that the reason given for the fact that a seemingly
> static predicate such as in

I don't think you have the reason right. This is not hard to implement at all,
in fact GNAT for a while had a full implementation. The trouble is that it
potentially involves huge inefficiencies which are hidden, consider

    type R is new Integer with
       R in N .. M;

where N is 1 and M is 2

The obvious implementation is to iterate through all integers doing the test,
yes, in practice you may be able to do better in some simple cases like this,
but in general you cannot, and I think it not in the spirit to have hidden
inefficiencies like this. Let the programmer write

    for J in R'Base loop
      if J in R then
          ...
      end if;
    end loop;

so that the inefficiency is obvious, and furthermore, the programmer might
prefer to write

    for J in R'Base range N .. M loop

to eliminate the inefficiency in this particular case

> is actually not allowed is that an implementation might want to
> compute and hold all the allowed values of such a subtype as a sort of set.

Nope, no implementation would even think of such a silly implementation

>     for E in Even loop ...
>
>
>
> especially if My_Integer was not an overwhelming range.

Well there you go! Surely you don't think legality should depend on what is or
is not an overwhelming range.

> First there is the fundamental problem that Ada does not support Sets.

No, this has nothing to do with the problem at all

> Neither finite sets nor (thankfully?) infinite sets. I recall that
> many years ago (long before Ada 83) there was a proposal for unordered
> enumeration types which might have formed the foundation for sets.
> These were abandoned.

And now of course we DO have the equivalent of unordered enumeration types, in
that we can have noncontiguous subtypes. Note that GNAT also has pragma
Unordered(enum-type) (I suppose we should make that an aspect as well ...) which
warns on inappropriate operations like comparison.

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

From: Robert Dewar
Sent: Wednesday, February 16, 2011  7:28 AM

> In the absence of sets, I believe we should abandon the subdivision of
>
> subtype predicates into dynamic and static forms. They introduce a
> whole lot
>
> of new rules for the restricted form of expression allowed in a
>
> Static_Predicate which make the language gross and is liable to
> confuse
>
> users. In any event the choice of names is misleading.

First of all, as per my previous message, sets have nothing to do with this.

This is an endlessly discussed issue and there is nothing new here (check the
dciscussion threads in gory detail if you want to revisit that discussion).

I think at this stage that we all agree that we should not allow loops through
the dynamic case because of the implicit inefficiency which we never like to see
in Ada. I understand you disagree, but I don't think you bring any new argument
which would change peoples minds.

> We should revert to the one predicate, Subtype_Predicate and perhaps
> restrict its use so that it cannot be applied to the (effectively)
> unconstrained types such as Integer, Long_Integer and so on.

First, I think it would be really unfortunate not to allow

    type Non_Zero_Integer is new Integer with
       R /= 0;

You don't present any convincing argument for taking away this useful
functionality.

Second, given we don't want to allow loops in the dynamic case, the strong
argument against having only one predicate is that it is annoying for legality
to be affected by a small change from static to dynamic (e.g. from 1 .. 10 to M
.. N).

You definitely have some people who agree with you on this (inccluding Bob Duff
and Robert Dewar, and indeed GNAT has this single aspect called simply Predicate
as well as the official ones, and only has a pragma Predicate, we did not do the
pragmas for the two official aspects).

But one extra vote here is not going to change the agreed on result in the
absence of new arguments, and you don't present anything here that has not been
presented before.

You definitely need to understand the ratoinale behind the choice of two
separate aspects to write the rationale!

Summary

1. We don't want to allow loops for dynamic predicates, because in the general
   case that could result in implicit hidden inefficiency which in some case
   could be disastrous (the Integer example I gave earlier).

[you would like to allow them, and ban integer, but neither is going to happen,
so these tastes do not affect the rationale for Ada 2012]

2. Given that static and dynamic predicates behave very differently, we
   deliberately want to distibnguish them,

if we write

     subtype R is Integer with
        Static_Predicate => R in 1 .. 10 or R in 20 .. 30;

then we can have a loop

     for J in R loop ...

and that will be implemented efficiently

Now suppose we want to change 30 to a dynamic value M

     subtype R is Integer with
        Static_Predicate => R in 1 .. 10 or R in 20 .. M;

That will be illegal since the condition is not static, so we get an indication
of a significant change at the point of declaration.

If we had only the single aspect Predicate, we could make the above change and
get no indication of a problem at the site of the declaration, but some client
could now become illegal. This is considered (by some who feel very strongly
about it) to be a significant maintenance issue, which is why we have two
aspects.

Yes, if we allowed the loop, this problem would not surface as an illegality,
but actually things would be even worse, when we change 30 to M, both the
package and the client remain legal, but suddenly we have a drastic inefficiency
in the client.

I do think this argument is pretty strong. For me I still slightly prefer to
have a single predicate, but I don't feel strongly, and the opposition
definitely feels strongly (strongly enough to want to throw out predicates
completely if this were done).

In practice the most useful use of predicates is for constrainining variant
types, and making non-contiguous enumeration types (be sure the rationale has
these two examples!) and those important uses are not affected by this
discussion.

P.S. interestingly, we could allow loops through dynamic predicates in GNAT for
the Predicate aspect, since that one is ours .. interesting thought! We have all
the code in some old revision, so it's tempting to do that.

And if you are worrying about portability, fear not, the pragma Profile
(No_Implementation_Features) will banish this evil GNAT extension from your
programs :-) :-)

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

From: Robert Dewar
Sent: Wednesday, February 16, 2011  7:32 AM

By the way on modern 64-bit machines

    for J in Integer loop
      A(J) := ' ';
    end loop;

is perfectly fine, the array fits fine in memory (it's only
4 gigabytes long, even my notebook has 8 gigs of memory), and it executes pretty
quickly on a fast machine (probably something like a second or two on a
moderately fast single core).

Machines move on!

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

From: Bob Duff
Sent: Wednesday, February 16, 2011  9:16 AM

> Subtype predicates
>
> I am very surprised at where we currently stand on subtype predicates.
> Namely Static_Predicate which can be used in contexts such as loops,
> and Dynamic_Predicate which is more general and cannot.
>
> I understand that the reason given for the fact that a seemingly
> static predicate such as in
>
> subtype Even is My_Integer
>    with Static_Predicate => Even mod 2 = 0;
>
> is actually not allowed is that an implementation might want to
> compute and hold all the allowed values of such a subtype as a sort of set.

The implementation MUST compute such a set, in order to check the full-coverage
rules for case statements, etc.  I expect the internal representation of these
sets in the compiler will be as a sorted sequence of ranges.  That's not the
only possibility, but it seems reasonable.  And representing Even in this way is
infeasible, so it's illegal (no great loss -- you just have to make the above
predicate Dynamic_).

Loops are not the main issue.  I originally proposed NOT to allow 'for' loops.  They're merely a "nice to have".
Case statements/expressions are the important feature.  But folks said 'for'
loops are easy enough to implement, so what the heck, let's throw them into the
pot.  Fine with me.

> The consequences seem foolish. I would expect to be allowed to write
>
>    for E in Even loop ...
>
> especially if My_Integer was not an overwhelming range.

As Robert said, this could lead to hidden inefficiencies.
I know how to loop through "Even" efficiently, but I don't know of any general
way that would be efficient for arbitrary predicates.

Besides, we want the rules for case statements and loops to be the same -- it's
bad enough to have two kinds of predicates, three kinds would be worse.

> Note that there is an inkling of this in Ada already since
> Integer'Base is considered to be unconstrained - and thus almost represents an
> infinite set.

Almost infinite?  Hmm.  There are a lot more integers NOT in Integer'Base than
are in it!

It's really annoying to me that Ada doesn't support arbitrary-range integers
(except at compile time).  We've been struggling with that here at AdaCore
lately regarding proof tools.  For example, the precondition of Integer "+" is
conceptually (in part):

    Left + Right <= Integer'Last -- no overflow
         ^
         |
         except that "+" is wrong, because it CAN overflow

And calling this meager subset of the integers "Integer" adds insult to injury.

> for X in Integer loop
>    if X mod 2 = 0 then
>       ...-- body of loop
>    end if;
> end loop;

What if it were "Pre => Page_Aligned mod 2**12 = 0"?

> In the absence of sets, I believe we should abandon the subdivision of
> subtype predicates into dynamic and static forms.

That was my position.  A lot of folks are (inexplicably) uncomfortable with
that.

>...They introduce a whole lot
> of new rules for the restricted form of expression allowed in a
>Static_Predicate which make the language gross and is liable to confuse
>users.

Well, we still need the same rules.  If we recombined the two kinds of predicate
into one aspect, then we would still have the definition, "a predicate is
predicate-static if...", and we would still disallow non-predicate-static
predicates in case statements etc.

>...In any event the choice of names is misleading.

I don't see why.  They're annoyingly long, but why "misleading"?

> We should revert to the one predicate, Subtype_Predicate and perhaps

"Subtype_" is just noise, IMHO.  I'd call it "Predicate".

> restrict its use so that it cannot be applied to the (effectively)
> unconstrained types such as Integer, Long_Integer and so on.

I wouldn't want such arbitrary restrictions.  What about "type T is range
0..2**24".  Is that "effectively infinite"? Where do you draw the line?
Besides, many predicates on Long_Integer CAN be static, and implemented
efficiently. It's the "mod" that causes trouble, not the large number of values.

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

From: Robert Dewar
Sent: Wednesday, February 16, 2011  9:37 AM

> The implementation MUST compute such a set, in order to check the
> full-coverage rules for case statements, etc.  I expect the internal
> representation of these sets in the compiler will be as a sorted
> sequence of ranges.  That's not the only possibility, but it seems
> reasonable.  And representing Even in this way is infeasible, so it's
> illegal (no great loss -- you just have to make the above predicate
> Dynamic_).

That's just not true, you don't need to compute a set for the dynamic case, you just loop through the base range and test the predicate for each value. That's the only general possible approach. It's quite easy, well defined, but can be inefficient.

> That was my position.  A lot of folks are (inexplicably) uncomfortable
> with that.

I find it odd that Bob finds in inexplicable, I find the explanations given by
these "lots of folks" quite reasonable and quite understandable, they don't
balance out my preference for having a single predicate, but I am not set on
this strongly, especially since the implementation can provide it anyway.

> Well, we still need the same rules.  If we recombined the two kinds of
> predicate into one aspect, then we would still have the definition, "a
> predicate is predicate-static if...", and we would still disallow
> non-predicate-static predicates in case statements etc.

Right, obviously we can't have full dynamic predicates in case statements, well
i guess we could with an others, but that's just silly.

> I wouldn't want such arbitrary restrictions.  What about "type T is
> range 0..2**24".  Is that "effectively infinite"?
> Where do you draw the line?  Besides, many predicates on Long_Integer
> CAN be static, and implemented efficiently.
> It's the "mod" that causes trouble, not the large number of values.

Actually the mod causes no trouble if the predicate is just being used for
membership and run time checking.

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

From: Tucker Taft
Sent: Wednesday, February 16, 2011  9:56 AM

> That's just not true, you don't need to compute a set for the dynamic
> case, you just loop through the base range and test the predicate for
> each value. That's the only general possible approach. It's quite
> easy, well defined, but can be inefficient.

I think you are agreeing with Bob.  Bob was explaining why "mod" is not allowed
in Static_Predicates, because of the full coverage requirement for case
statements, which implies being able to enumerate the set efficiently.

...
>> It's the "mod" that causes trouble, not the large number
>> of values.
>
> Actually the mod causes no trouble if the predicate is just being used
> for membership and run time checking.

Again, I think you are agreeing with Bob.  The "mod" is not a problem for
membership, it is a problem for full coverage checks, which makes it a no-no for
Static_Predicates.

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

From: Robert Dewar
Sent: Wednesday, February 16, 2011  10:38 AM

> Again, I think you are agreeing with Bob.  The "mod" is not a problem
> for membership, it is a problem for full coverage checks, which makes
> it a no-no for Static_Predicates.

Yes, of course, that's exactly right and handling that "Right" would be a huge
pain.

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

From: Bob Duff
Sent: Wednesday, February 16, 2011  11:05 AM

> > The implementation MUST compute such a set, in order to check the
> > full-coverage rules for case statements, etc.  I expect the internal
> > representation of these sets in the compiler will be as a sorted
> > sequence of ranges.  That's not the only possibility, but it seems
> > reasonable.  And representing Even in this way is infeasible, so
> > it's illegal (no great loss -- you just have to make the above
> > predicate Dynamic_).
>
> That's just not true, you don't need to compute a set for the dynamic
> case, you just loop through the base range and test the predicate for
> each value. That's the only general possible approach. It's quite
> easy, well defined, but can be inefficient.

I meant that the implementation MUST compute such a set for static predicates.  However we define "static predicates", those are the ones allowed in case statements (etc).

I agree that it need not (and cannot) compute the set for dynamic predicates,
and that it is possible to allow dynamic predicates in 'for' loops.  But it's a
potentially huge hidden inefficiency, which makes it inadvisable. And as I said,
I prefer not to have a different rule for 'for' loops than for case statements.

> > That was my position.  A lot of folks are (inexplicably)
> > uncomfortable with that.
>
> I find it odd that Bob finds in inexplicable, I find the explanations
> given by these "lots of folks" quite reasonable and quite
> understandable, they don't balance out my preference for having a
> single predicate, but I am not set on this strongly, especially since
> the implementation can provide it anyway.

I am going to refrain from answering this question, because I don't see any
value in continuing the argument about a (most likely) settled issue.

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

From: John Barnes
Sent: Friday, February 18, 2011  7:41 AM

The various messages gave me further insight into why we have come to what we
have. It really is quite complex and will give me lots of food for a detailed
section of the rat. I find it quite amazing how easy it is to get out of touch
by missing just one meeting. But my concern remains that we don't mess up any
possible broader feature in the future, it's just an unease and I cannot really
put my finger on anything too specific. But remember how the original rules
about null and access parameters were a pain when null was added more generally.

However the names Static_Predicate and Dynamic_Predicate still seem not ideal.
That's because the static are somewhat different to our usual use of static. But
I must confess I cannot think of much better names. And its a pity to lose
subtype in the name because that distinguished them from type invariants rather
neatly.

Maybe general and special could be a starting point. Or general and restricted.
Hmm.

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

From: Robert Dewar
Sent: Friday, February 18, 2011  7:54 AM

I don't like Subtype in the name. Like Specification, Subtype is a term which
has a different meaning to Ada progammers and RM language lawyers

    type R is new Integer;

to ada programmers, R is a type, not a subtype, to RM LL's it is a subtype. I
HATE this, but we are stuck with it. In GNAT error messages we never use subtype
to mean type as well. If you used it in the name of the predicate, lots of Ada
programmers would assume this means that you can't use it, e.g. in

    type R is new Integer with
      Static_Subtype_Predicate => R /= 0;

since R is not a subtype. Because subtype predicates can perfectly well apply to
all types, I don't see why this distinguishes them from Invariants anyway.

> Maybe general and special could be a starting point. Or general and
> restricted. Hmm.

Static really is better, since this echoes the restriction of case statements to
static expressions. Yes, we don't allow all static expressions because of
implementation difficulties, though we could if we really wanted to (at some
expense!)

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

From: Bob Duff
Sent: Friday, February 18, 2011  7:02 PM

> I don't like Subtype in the name. Like Specification, Subtype is a
> term which has a different meaning to Ada progammers and RM language
> lawyers
>
>     type R is new Integer;
>
> to ada programmers, R is a type, not a subtype, to RM LL's it is a
> subtype. I HATE this, but we are stuck with it. In GNAT error messages
> we never use subtype to mean type as well. If you used it in the name
> of the predicate, lots of Ada programmers would assume this means that
> you can't use it, e.g. in
>
>     type R is new Integer with
>       Static_Subtype_Predicate => R /= 0;
>
> since R is not a subtype. Because subtype predicates can perfectly
> well apply to all types, I don't see why this distinguishes them from
> Invariants anyway.

I agree 100% with Robert's comments above.  Even I think of R as a type, except
when I've got my language-lawyer hat on.

> > Maybe general and special could be a starting point. Or general and
> > restricted. Hmm.
>
> Static really is better, since this echoes the restriction of case
> statements to static expressions. Yes, we don't allow all static
> expressions because of implementation difficulties, though we could if
> we really wanted to (at some expense!)

Right, except it's not just that we're more restrictive with "predicate-static"
than "static".  The main point is that we want the name of the current instance
in there, even though it is not static -- it will be (conceptually) static once
we have a value for it.  When we say:

    subtype S is Integer with
        Static_Predicate => (S /= 0 and S < 100 and S > -100) or S = Integer'Last;

the expression after "=>" is certainly not static, since S is not a static
expression, but we allow it because if you plug in a static value for S, then
that expression is static.  And we can construct a statically-known set,
represented as a sequence of ranges:

    {-99..-1, 1..99, Integer'Last..Integer'Last}

One key point to put in the Rat is that the number of ranges in this set is
roughly proportional to the size of the program text.

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

From: Edmond Schonberg
Sent: Wednesday, March 16, 2011  7:54 AM

An enthusiastic user has detected a problem with a proposed  legality rule
in the new section 3.2.4 :

The prefix of an attribute_reference whose attribute_designator is First, Last,
or Range shall not denote a subtype to which predicate clauses apply.


We know the motivation for this rule (problem with enumerations with holes, etc.)
but the rule only makes sense for scalar types. Otherwise
it is hard to write useful predicates on array subtypes, for example:

package Pred is
   type A is array (Integer range <>) of Integer
     with Predicate => (for all J in A'Range =>
 (for all K in A'Range =>
    (if J /= K then A (J) /= A (K))));
end Pred;

The rule should say  "scalar subtype".

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

From: Bob Duff
Sent: Wednesday, March 16, 2011  8:08 AM

Please make the following editorial change to AI05-0153-3, Subtype
predicates:

The prefix of an attribute_reference whose attribute_designator is First, Last,
or Range shall not denote a {scalar} subtype to which predicate clauses apply.

I think we all meant "scalar" here.  Nothing wrong with doing 'Range an a
predicated array type.

Thanks.

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

From: John Barnes
Sent: Thursday, April 7, 2011  4:07 AM

Since this is up for voting again I am going to take the opportunity to say once
more that I think that this AI is a big mistake (specifically Static_Predicate).
I expect it will be regretted some time in the future when the ARG gets around
to discussing sets properly.

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

From: Robert Dewar
Sent: Friday, April 8, 2011  6:10 PM

And I think that static predicates are THE most interesting and useful feature
of Ada 2012, I am quite sure that GNAT will implement them even if they are
removed from Ada 2012 (seeing as

a) they are already implemented
b) they turn out to be very useful
c) we are using them!)

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

From: Robert Dewar
Sent: Friday, April 8, 2011  6:11 PM

By the way, I don't see what static predicates have to do with sets per se.

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

From: Randy Brukardt
Sent: Saturday, April 9, 2011  1:18 AM

...
> And I think that static predicates are THE most interesting and useful
> feature of Ada 2012, ...

I wouldn't go quite that far (preconditions would have to be high on the list),
but since they provide the set constraints that Ada never had and always has
needed, I do agree that they are very useful.

> By the way, I don't see what static predicates have to do with sets per se.

Well, they provide a way to get the effect of a set constraint, along with other
sorts of constraints.

Robert was replying to John:

> I expect it will be regretted some time in the future when the ARG gets around
> to discussing sets properly.

I doubt that will ever happen, in part because the static predicates provide all
of the functionality needed. But mainly because AI05-0158-1 has used the
"obvious" syntax for a set in such a way that it is likely that any set
functionality would be ambiguous. That has nothing to do with static predicates;
I don't see any problem with the predicates themselves no matter what other
constructs we might add.

We'd have to add some new dedicated set syntax (like using square brackets) to
add first-class sets. But why would we want them? Set membership is handled by
the extended membership test, and set constraints are handled by static
predicates. So the only thing you can't do natively is dynamically construct a
set to use in those contexts -- and that can be handled adequately by a set
package (and dynamic predicates), since it isn't commonly used.

So I don't see why we'd want to spend a lot of effort on "proper sets", whatever
that is. It's probably about 400th on the priority list for Ada 2020...

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

From: Robert Dewar
Sent: Saturday, April 9, 2011  4:22 AM

> ...
>> And I think that static predicates are THE most interesting and
>> useful feature of Ada 2012, ...
>
> I wouldn't go quite that far (preconditions would have to be high on
> the list), but since they provide the set constraints that Ada never
> had and always has needed, I do agree that they are very useful.

Ah, true, but for me preconditions and postconditions have been around for a
while pre-Ada2012 :-)

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

From: John Barnes
Sent: Monday, April 11, 2011  5:23 AM

> And I think that static predicates are THE most interesting and useful
> feature of Ada 2012, I am quite sure that GNAT will implement them
> even if they are removed from Ada 2012 (seeing as
...

It's not that I dislike the idea of Static predicates. Its just that I dislike
the sort-of-static rules that prevent Even from being allowed just because it
has mod in it.

That has really upset me. I know, I get upset easily.

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

From: Robert Dewar
Sent: Monday, April 11, 2011  1:08 PM

But do you want to throw the baby out with the bathwater here.
The staticness rules and the effect of non-contiguous enumeration subtypes (the
main use of static predicates) are really not impacted by the mod issue (and
*surely* you see the implementation issues in trying to include mod???)

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

From: Bob Duff
Sent: Monday, April 11, 2011  2:11 PM

Even is still allowed.  You can say:

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

You cannot say "when Even =>" in a case statement, but that was true before the
split from Predicate to Static_Predicate/Dynamic_Predicate.

Does this make you happier?

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

From: Bob Duff
Sent: Thursday, April 7, 2011  6:07 PM

New version of AI05-0153-3, Subtype predicates, based on the April 7, 2011 phone
meeting. [This is version /08 - Editor.] Tucker suggested changing "predicate
clause" to "predicate specification".

Gary suggested getting rid of this term altogether, but that would require
saying "specification of a predicate aspect" or some such, which is a bit of a
mouthful, and it's used many times, so I went with Tucker's suggestion.

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

From: Randy Brukardt
Sent: Friday, May 6, 2011  9:54 PM

This one probably doesn't need to be answered (since it seems obvious), but as
it is fairly significant, I wanted to mention it. [Oops; after writing it I
found a more signficant problem. See the bottom. - RLB]

In AI05-0153-3 (Subtype Predicates), the grammar for discrete_choices was
changed from:

5     discrete_choice ::= expression | discrete_range | others

to (including the AI05-0158-1 change):

5     discrete_choice ::= choice_expression | *discrete_*subtype_indication
| range | others

[BTW, the AI had "discrete_subtype_indication", but there is no such thing. I
got errors from the RM tool which makes links for all non-terminal references -
which doesn't work for non-existent NTs. This change seems to have been lifted
from 3.6, where subtype_indication has a "discrete" prefix, so that's what I did
here.]

3.8.1(8) starts:

The expressions and discrete_ranges given as discrete_choices in a variant_part
shall be static. ...

Wait a minute -- what "discrete_ranges"?? There aren't any in the grammar!
Similarly, "expressions" is vaguely wrong. So I replaced this by:

The choice_expressions, subtype_indications, and ranges given as
discrete_choices in a variant_part shall be static. ...

The same thing needs to be done in 5.4(5) [it's virtually the same text].

----------------------------

Oh-oh: discrete_choice is also used by array aggregates. 4.3.3(17) also needs to
be fixed:

"...that is a subtype_indication or range that defines a nonstatic or null
range..."

However, talking about discrete_ranges made subtypes with predicates illegal in
array aggregates (which is what we want, I think); now there is no such
requirement. We could add some text to 3.2.4 to cover this case, but it's not
clear exactly what it should be or whether the modified definition of choice
coverage causes problems. So I'm not sure what wording needs to be added here.

Humm, the wording that Bob proposed doesn't seem to mention array aggregates in
the places where predicate subtypes aren't allowed. Was that an oversight or
intentional?? (Recall that array aggregate choices don't have to be static, so
we seem to be allowing dynamic predicates here. Yikes!)

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

From: Bob Duff
Sent: Saturday, May 7, 2011  10:40 AM

...
> [BTW, the AI had "discrete_subtype_indication", but there is no such thing.
> I got errors from the RM tool which makes links for all non-terminal
> references - which doesn't work for non-existent NTs. This change
> seems to have been lifted from 3.6, where subtype_indication has a
> "discrete" prefix, so that's what I did here.]

Good.  At least there's SOME regression testing on the RM.  ;-)

> 3.8.1(8) starts:
>
> The expressions and discrete_ranges given as discrete_choices in a
> variant_part shall be static. ...
>
> Wait a minute -- what "discrete_ranges"?? There aren't any in the grammar!
> Similarly, "expressions" is vaguely wrong. So I replaced this by:
>
> The choice_expressions, subtype_indications, and ranges given as
> discrete_choices in a variant_part shall be static. ...
>
> The same thing needs to be done in 5.4(5) [it's virtually the same text].

OK.

> ----------------------------
>
> Oh-oh: discrete_choice is also used by array aggregates. 4.3.3(17)
> also needs to be fixed:
>
> "...that is a subtype_indication or range that defines a nonstatic or
> null range..."
>
> However, talking about discrete_ranges made subtypes with predicates
> illegal in array aggregates (which is what we want, I think); ...

The intent is that Static_Predicates can be used whereever full coverage rules
apply.  So you can say:

    subtype Upper is Character range 'A'..'Z';
    subtype Lower is Character range 'a'..'z';
    subtype Letter is Character with
        Static_Predicate => Letter in Upper or Letter in Lower;

    Is_Letter: constant array(Character) of Boolean
        := (Letter => True, others => False);

or:

    Is_Letter: constant array(Character) of Boolean
        := (Upper => True, Lower => True, others => False);

Dynamic_Predicates, on the other hand, are trouble.

>...now there is no such
> requirement. We could add some text to 3.2.4 to cover this case, but
>it's  not clear exactly what it should be or whether the modified
>definition of  choice coverage causes problems. So I'm not sure what
>wording needs to be  added here.
>
> Humm, the wording that Bob proposed doesn't seem to mention array
> aggregates in the places where predicate subtypes aren't allowed. Was
> that an oversight or intentional??

The dynamic part was an oversight.

> ...(Recall that array aggregate choices don't have to be static, so we
> seem to be allowing dynamic predicates here. Yikes!)

Well, a nonstatic subtype_indication is currently only allowed when there is
exacty one choice.  I suggest you modify this paragraph of the AI:

The discrete_subtype_definition of a loop_parameter_specification shall not
denote a subtype to which Dynamic_Predicate specifications apply.

as follows:

The discrete_subtype_definition of a loop_parameter_specification {or a
discrete_choice of a named_array_aggregate} shall not denote a subtype to which
Dynamic_Predicate specifications apply.

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

From: Randy Brukardt
Sent: Monday, May 9, 2011  8:31 PM

...
> > [BTW, the AI had "discrete_subtype_indication", but there is no such thing.
> > I got errors from the RM tool which makes links for all non-terminal
> > references - which doesn't work for non-existent NTs. This change
> > seems to have been lifted from 3.6, where subtype_indication has a
> > "discrete" prefix, so that's what I did here.]
>
> Good.  At least there's SOME regression testing on the RM.  ;-)

There's actually another such test: Pascal created a tool last time to compare
the Amendment document (that is, the !corrigendum sections) to the text in the
Standard. However, I'm not sure I know how to use it (or if I have the most
recent source); I recall that he didn't let me use it again after I spent
several hours attempting to use an early version and wrote him a lengthy message
complaining about it. :-)

...
> > Oh-oh: discrete_choice is also used by array aggregates. 4.3.3(17)
> > also needs to be fixed:
> >
> > "...that is a subtype_indication or range that defines a nonstatic
> > or null range..."
> >
> > However, talking about discrete_ranges made subtypes with predicates
> > illegal in array aggregates (which is what we want, I think); ...
>
> The intent is that Static_Predicates can be used whereever full
> coverage rules apply.  So you can say:
>
>     subtype Upper is Character range 'A'..'Z';
>     subtype Lower is Character range 'a'..'z';
>     subtype Letter is Character with
>         Static_Predicate => Letter in Upper or Letter in Lower;
>
>     Is_Letter: constant array(Character) of Boolean
>         := (Letter => True, others => False);
>
> or:
>
>     Is_Letter: constant array(Character) of Boolean
>         := (Upper => True, Lower => True, others => False);

OK. It is odd that you can't declare an array subtype using a subtype with a
predicate, but you can write the similar aggregate.

    subtype Smallish is Positive
       with Static_Predicate => Smallish <= 10;

   Odd : String(Smallish) -- Illegal.
      := (Smallish => ' '); -- Legal.

But that doesn't seem critical - it only would work when the predicate should
have been written as a range (else the aggregate would violate 4.3.3(18)).

> Dynamic_Predicates, on the other hand, are trouble.

Right. I was thinking about the above oddity and the dynamic cases when I was
thinking about this.

> >...now there is no such
> > requirement. We could add some text to 3.2.4 to cover this case, but
> >it's  not clear exactly what it should be or whether the modified
> >definition of  choice coverage causes problems. So I'm not sure what
> >wording needs to be  added here.
> >
> > Humm, the wording that Bob proposed doesn't seem to mention array
> > aggregates in the places where predicate subtypes aren't allowed.
> > Was that an oversight or intentional??
>
> The dynamic part was an oversight.
>
> > ...(Recall that array aggregate choices don't have to be static, so
> > we seem to be allowing dynamic predicates here. Yikes!)
>
> Well, a nonstatic subtype_indication is currently only allowed when
> there is exacty one choice.  I suggest you modify this paragraph of
> the AI:
>
> The discrete_subtype_definition of a
> loop_parameter_specification shall not denote a subtype to which
> Dynamic_Predicate specifications apply.
>
> as follows:
>
> The discrete_subtype_definition of a
> loop_parameter_specification {or a discrete_choice of a
> named_array_aggregate} shall not denote a subtype to which
> Dynamic_Predicate specifications apply.

OK, I'll do that.

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

From: Bob Duff
Sent: Tuesday, May 10, 2011  4:15 PM

> OK. It is odd that you can't declare an array subtype using a subtype
> with a predicate, but you can write the similar aggregate.
>
>     subtype Smallish is Positive
>        with Static_Predicate => Smallish <= 10;
>
>    Odd : String(Smallish) -- Illegal.

I considered making that legal, by somehow defining which predicates are
known to result in a single subrange. But it just didn't seem worth the trouble.

>       := (Smallish => ' '); -- Legal.
>
> But that doesn't seem critical - it only would work when the predicate
> should have been written as a range (else the aggregate would violate
  ^
  "could", I'd say.  Your "Smallish <= 10" predicate doesn't seem at all evil,
to me, even though it could be expressed as a range. And with the rules as they are,
you'll HAVE to use a range, if you want to say "String(Smallish)".  Oh, well.

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

From: Randy Brukardt
Sent: Friday, May 06, 2011 8:21 PM

I'm working on putting the large AIs into the Standard, and sometimes the
juxtaposition highlights things that I wouldn't otherwise think of. I just
finished AI05-0228-1, which changes 13.13.2(35) to use "implicit initial values"
(in order that Default_Value and Default_Component_Value are captured). [Note
that the term "implicit initial values" dates back at least to Ada 95, we just
extended it a bit.]

I then am working on the following Dynamic Semantics paragraph from 3.2.4 (from
AI05-0153-3):

If the Assertion_Policy (see 11.4.2) in effect is Check, then:

  On every subtype conversion, the predicate of the target subtype is
  evaluated, and a check is made that the predicate is True. This includes all
  parameter passing, except for certain parameters passed by reference, which
  are covered by the following rule: After normal completion and leaving of a
  subprogram, for each in out or out parameter that is passed by reference, the
  predicate of the subtype of the actual is evaluated, and a check is made that
  the predicate is True. For an object created by an object_declaration with no
  explicit initialization expression, or by an uninitialized allocator,
  if any subcomponents have explicit default values, the predicate of the nominal
  subtype is evaluated, and a check is made that the predicate is True.
  Assertions.Assertion_Error is raised if any of these checks fail.

My first concern is "explicit default values". I'm not quite sure what this is
supposed to mean, but I would think it either should use the old wording of
13.13.2 (component_declarations with default_expressions) or the new wording
(implicit initial values). Note that "implicit initial values" is a forward
reference here, it will need (see 3.3.1) following. I think you meant the
latter, but I'm not certain. I'll use the "implicit initial values" unless
someone objects. [Aside: It's funny that the "correct" wording is exactly the
reverse of what you said.]

My second concern is with "the predicate of the nominal subtype is evaluated".
When I first (re)read this, I thought it was talking about the subtype of the
subcomponents. That doesn't make any sense (the subtype conversion of the
default expression - however that is determined - will evaluate the
predicate(s)). I now think that you are talking about the nominal subtype of the
object declaration or allocator. I think we have to say that, because the
wording doesn't associate well otherwise.

So we get:

  On every subtype conversion, the predicate of the target subtype is
  evaluated, and a check is made that the predicate is True. This includes all
  parameter passing, except for certain parameters passed by reference, which
  are covered by the following rule: After normal completion and leaving of a
  subprogram, for each in out or out parameter that is passed by reference, the
  predicate of the subtype of the actual is evaluated, and a check is made that
  the predicate is True. For an object created by an object_declaration with no
  explicit initialization expression, or by an uninitialized allocator,
  if any subcomponents have implicit initial values, the predicate of the nominal
  subtype of the object_declaration or allocator is evaluated, and a check is made
  that the predicate is True. Assertions.Assertion_Error is raised if any of these
  checks fail.

Is this what you meant, or is it something else??

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

From: Bob Duff
Sent: Saturday, May 07, 2011 10:38 AM

> I'm working on putting the large AIs into the Standard, and sometimes
> the juxtaposition highlights things that I wouldn't otherwise think of.

I'm sure there will be lots more such cases.  And I'm sure some of them will
slip through unnoticed, and we'll have to fix them with Ada 2012 AIs.

>... I just
> finished AI05-0228-1, which changes 13.13.2(35) to use "implicit
>initial  values" (in order that Default_Value and
>Default_Component_Value are  captured). [Note that the term "implicit
>initial values" dates back at least  to Ada 95, we just extended it a
>bit.]
>
> I then am working on the following Dynamic Semantics paragraph from
> 3.2.4 (from AI05-0153-3):
>
> If the Assertion_Policy (see 11.4.2) in effect is Check, then:
>
>   On every subtype conversion, the predicate of the target subtype is
>   evaluated, and a check is made that the predicate is True. This includes all
>   parameter passing, except for certain parameters passed by reference, which
>   are covered by the following rule: After normal completion and leaving of a
>   subprogram, for each in out or out parameter that is passed by reference, the
>   predicate of the subtype of the actual is evaluated, and a check is made that
>   the predicate is True. For an object created by an object_declaration with no
>   explicit initialization expression, or by an uninitialized allocator,
>   if any subcomponents have explicit default values, the predicate of the nominal
>   subtype is evaluated, and a check is made that the predicate is True.
>   Assertions.Assertion_Error is raised if any of these checks fail.
>
> My first concern is "explicit default values". I'm not quite sure what
> this is supposed to mean,...

It's supposed to mean that somebody wrote ":= <something>" on a component
declaration, for some subcomponent of the type.  Implicit initial values, such
as "null", and those defined by Default_[Component_]Value, don't count.

>...but I would think it either should use the old wording  of 13.13.2
>(component_declarations with default_expressions)

I'm not sure which "old wording" you're referring to, but yes,
"component_declarations with default_expressions" is what I meant.

>... or the new wording (implicit initial values).

That would be wrong.

>... Note that "implicit initial values" is a  forward reference here,
>it will need (see 3.3.1) following. I think you  meant the latter, but
>I'm not certain. I'll use the "implicit initial  values" unless someone
>objects.

I object.

>...[Aside: It's funny that the "correct"
> wording is exactly the reverse of what you said.]

I think I said what I meant, even if I didn't use proper RM jargon.  ;-)

> My second concern is with "the predicate of the nominal subtype is
> evaluated". When I first (re)read this, I thought it was talking about
> the subtype of the subcomponents. That doesn't make any sense (the
> subtype conversion of the default expression - however that is
> determined - will evaluate the predicate(s)).

Right, that doesn't make sense.

>...I now think that you are talking about the  nominal subtype of the
>object declaration or allocator.

Right.  Except that's not proper RM jargon.  You should add "of the object"
after "nominal subtype".  Or if you think that's still unclear, add "of the
created object".

>...I think we have to
> say that, because the wording doesn't associate well otherwise.
>
> So we get:
>
>   On every subtype conversion, the predicate of the target subtype is
>   evaluated, and a check is made that the predicate is True. This includes all
>   parameter passing, except for certain parameters passed by reference, which
>   are covered by the following rule: After normal completion and leaving of a
>   subprogram, for each in out or out parameter that is passed by reference, the
>   predicate of the subtype of the actual is evaluated, and a check is made that
>   the predicate is True. For an object created by an object_declaration with no
>   explicit initialization expression, or by an uninitialized allocator,
>   if any subcomponents have implicit initial values, the predicate of the nominal
>   subtype of the object_declaration or allocator is evaluated, and a check is made
>   that the predicate is True. Assertions.Assertion_Error is raised if any of these
>   checks fail.
>
> Is this what you meant, or is it something else??

Something else.  ;-)  See above.

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

From: Randy Brukardt
Sent: Monday, May 09, 2011 9:50 PM

...
> > I then am working on the following Dynamic Semantics paragraph from
> > 3.2.4 (from AI05-0153-3):
> >
> > If the Assertion_Policy (see 11.4.2) in effect is Check, then:
> > ... For an object created by an object_declaration with no
> >   explicit initialization expression, or by an uninitialized allocator,
> >   if any subcomponents have explicit default values, the predicate
> >   of the nominal
> >   subtype is evaluated, and a check is made that the predicate is True.
> >   Assertions.Assertion_Error is raised if any of these checks fail.
> >
> > My first concern is "explicit default values". I'm not quite sure
> > what this is supposed to mean,...
>
> It's supposed to mean that somebody wrote ":= <something>" on a
> component declaration, for some subcomponent of the type.
> Implicit initial values, such as "null", and those defined by
> Default_[Component_]Value, don't count.

OK, but that's weird. We've tried to reduce/eliminate differences between
explicit and implicit initializations. And I'm not sure that it really works
(see below).

In any case, I've fixed up the wording as you indicated for the moment, pending
further discussion (I'm giving the author the benefit of the doubt; I don't want
to change your intent without discussion).

> >...but I would think it either should use the old wording of 13.13.2
> >(component_declarations with default_expressions)
>
> I'm not sure which "old wording" you're referring to, but yes,
> "component_declarations with default_expressions" is what I meant.

OK.

...

> > My second concern is with "the predicate of the nominal subtype is
> > evaluated". When I first (re)read this, I thought it was talking
> > about the subtype of the subcomponents. That doesn't make any sense
> > (the subtype conversion of the default expression - however that is
> > determined - will evaluate the predicate(s)).
>
> Right, that doesn't make sense.
>
> >...I now think that you are talking about the  nominal subtype of the
> >object declaration or allocator.
>
> Right.  Except that's not proper RM jargon.  You should add "of the
> object" after "nominal subtype".  Or if you think that's still
> unclear, add "of the created object".

I'll add "of the created object", it's a bit clearer.

...

Now to back up a bit. The rule we're talking about now reads:

For an object created by an object_declaration with no explicit initialization
expression, or by an uninitialized allocator, if any subcomponents have
default_expressions, the predicate of the nominal subtype of the created object
is evaluated, and a check is made that the predicate is True.

My recollection is that the purpose of this rule is to ensure that composite
objects obey their predicate, but to avoid requiring that composite components
are initialized when using a predicate. If we always evaluated the predicate,
then any components that the predicate depends upon would always have to be
initialized (else the predicate could be depending on invalid values, with the
erratic results that follow from that). Such initializations potentially would
have substantial runtime overhead, so we don't want to force them, and we surely
don't want to make programmers have to choose between efficiency and using
predicates.

OTOH, if the predicate was never evaluated for such object declaration, it would
be easy to create values that fail the predicate and the failures would occur
much later -- making this construct much less like constraints than we would
like. It also would make the behavior of explicitly initialized object
declarations very different from the implicit ones, which is uncomfortable.

Given this intention, it seems to me that the proposed rule fails dismally.

First, there are many cases that are clearly not going to be detected by this
rule. For instance, consider one of Bob's favorite topics, the 1-based string:

     subtype One_Based_String is String
        with Dynamic_Predicate => One_Based_String'First = 1;

     Foo : One_Based_String (2 .. 10); -- No exception here!

     Bar : One_Based_String (2 .. 3) := "AA"; -- Raises Assertion_Error.

Depending on how Foo is used (consider using it as the first operand of a
concatenation), the language might never actually check the predicate, meaning
that the purpose of predicate would never be enforced.

Second, it will be periodically occur that predicates are enforced on
uninitialized components:

     type Some_Rec is record
         Count : Natural := 0;
         Id    : Character;
     end record;

     subtype A_Rec is Some_Rec
        with A_Rec.Id = 'A';

     declare
        A : A_Rec; -- Oops: Id is not initialized, probably will get Assertion_Error.
     begin
        A := (Count => 0, Id => 'A');
        ...


This example is contrived, but almost all of the large records that I have used
in my programs have at least one default expression (which includes
discriminants, of course). So the predicates would almost always be evaluated,
and the initialization would always be forced if the predicates are to work.


Clearly, the rule we really want is something like: "For an uninitialized object
declaration or allocator, if all of the components that the predicate depends on
are initialized, then the predicate is evaluated." [This is purposely sloppy -
it's not a serious proposal.] However, it should be clear that such a rule would
be hard to implement and would cause problems with function calls (how do you
figure out what subcomponents a function call touches??) So the rule we really
want is out.

It's possible that Bob's current rule (and I don't think this was Bob's original
idea, although I don't recall precisely what his original idea was) is the best
that we can do. But I'm dubious; it misses clearly important cases as shown
above, and *still* doesn't prevent touching uninitialized components. Clearly
there is a trade-off here, and it isn't clear where that trade-off is.

Two other options come to mind:

(1) Always check the predicate in the cases noted. "If it hurts to have a
    predicate on type Some_Rec, then don't do that." It's not the nicest
    solution, but remember the problem only occurs on components actually
    touched by the predicate. If you want to reference them in a predicate, then
    you ought to at least consider initializing them. Obviously, no problem
    cases will get through unchecked, but there is a runtime overhead and/or a
    restriction on use that follows from it.

(2) Make sure that a predicate is checked only if *all* of the components are
    initialized. That would avoid the problem of depending on uninitialized
    components, with the result of precates being evaluated much less often on
    uninitialized objects. One could imagine tweaking this based on the actual
    predicate expressions (only requiring components that are touched if there
    are no user-defined functions), but that probably wouldn't help much.

I have to admit that none of these options seems particularly pleasant. I'd
probably lean toward (1) [rather than the current proposal] because it is
simpler and less surprising to users (even if a bit more of a pain), but perhaps
there is something better out there.

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

From: Bob Duff
Sent: Tuesday, May 10, 2011 3:20 PM

> Two other options come to mind:

Before I answer this, could you please clarify this:

> (1) Always check the predicate in the cases noted.

Which cases noted?

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

From: Randy Brukardt
Sent: Tuesday, May 10, 2011 3:34 PM

> Which cases noted?

Uninitialized object_declarations and allocators (of composite types??) I didn't
spend very long thinking about the details. There wouldn't be any value to
requiring it for scalar types, so I think they should be excepted in any case.
But I still haven't spent very long thinking about the details. ;-)

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

From: Bob Duff
Sent: Tuesday, May 10, 2011 4:05 PM

> In any case, I've fixed up the wording as you indicated for the
> moment, pending further discussion (I'm giving the author the benefit
> of the doubt; I don't want to change your intent without discussion).

OK, that seems appropriate.

I think this is the best we can do, although I agree entirely that your
examples (snipped) illustrates that it's not perfect. But we already knew
predicates are imperfect. (I hope this issue won't invite us all to go back
into the mode of "Horrors!  Predicates are imperfect!  Let's add all kinds
of restrictions!  Let's eliminate the feature altogether!")

You have to be careful that if you have one component with a default_exp,
then your predicate had better not look at uninit ones.  I think often that
would fall out naturally:

    type T is
        record
            Length : Natural := 0;
            Elements : array (1..Max) of ...; -- yeah, yeah...
        end record with
            Predicate => Length <= Max
                and then (for all X in 1..Length => Is_Good(Elements(X)));

Ada has a serious flaw:  There's no way to declare "this type has a meaningful
default value".  So when you read "X : T;" you can't easily tell whether it
means "I'm going to initialize X later on, before I use it" or "I want to use
the default value of X, and I'm going to look at it before any explicit
assignment".

Given this rather unfixable flaw, I think the predicate rule we have is the best
we can do.

I'm pretty sure the two options you mentioned (snipped), are not an improvement.
So I think we should stick with what we've got, unless somebody has a
clearly-better idea.

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

From: Randy Brukardt
Sent: Monday, May 09, 2011 11:56 PM

As I was finishing up work on AI05-0153-3, I noticed an issue that is mainly
with the index but might also be a semantic issue.

Some of the wording of AI05-0153-3 says:

"After normal completion and leaving of a subprogram, for each in out or out
parameter that is passed by reference, the predicate of the subtype of the
actual is evaluated, and a check is made that the predicate is True."

There is similar wording for preconditions and postconditions, and probably for
a number of other contract aspects.

I was wondering what the check name to index should be for this. All of the
language-defined checks have a check name, and these are indexed. By using the
word "check", this surely appears to be one of these.

But check names exist mainly to serve as input to pragma Suppress. These
"checks" are controlled separately, via assertion policy; we don't want to
control these with Suppress.

11.4.2 is careful to not call what pragma Assert does "a check".
Interestingly, so is the proposed wording for 4.6(51):

"If the Assertion_Policy in effect is Check, the predicate of the target subtype
is applied to the value and Assertions.Assertion_Error is raised if the result
is False."

It seems odd at best to avoid the word "check" in text describing what happens
for a policy of "check".

Anyway, I'm confused. The best plan would be to reword everything involving
Assertion_Policy to avoid the term "check", but that seems over the top and a
lot of work.

The second best plan is to define a check name "Assertion_Check" and simply
mention in 11.5 that you aren't allowed to use Suppress to control those checks
and use Assertion_Policy instead.

There is no third best plan, perhaps someone has one.

The worst plan is just to ignore the issue and not index these things at all
(but that is annoying for people trying to find checks, and confusing in the
operation of pragma Suppress).

Ideas??

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

From: Bob Duff
Sent: Tuesday, May 10, 2011 3:29 PM

> The worst plan is just to ignore the issue and not index these things
> at all (but that is annoying for people trying to find checks, and
> confusing in the operation of pragma Suppress).

I vote for the "worst plan".  There will certainly be an index entry for
"predicate", so what's the problem?

You say these are not suppressable checks, so why should they be indexed under
"check" names?

I say, "not sufficiently broken".  And if you start doing major rewordings at
this point, there's a risk of making things worse. If there were a serious bug,
then it would be worth the risk.

Anyway, check names are already completely broken -- we define their semantics
only in the AARM, which is supposedly non-normative. That was a deliberate
decision on my part, which I rationalized by "it's no worse than Ada 83".

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

From: Randy Brukardt
Sent: Tuesday, May 10, 2011 3:52 PM

> You say these are not suppressable checks, so why should they be
> indexed under "check" names?

Mainly because the only thing indexed under "checks, language defined" are check
names.

I think it is bad to have checks that are not indexed as checks. And if they are
not checks, then they should be called something else (and indexed there).

> I say, "not sufficiently broken".  And if you start doing major
> rewordings at this point, there's a risk of making things worse.
> If there were a serious bug, then it would be worth the risk.

I agree with that. But not indexing these things (whatever they are) seems bad.

Indeed, I think all of the things controlled by the Assertion_Policy ought to be
indexed somehow -- it's not an obvious list. And so long as these things are
"checks" they need to be indexed there as well.

I did think of a fourth option last night, which is to index these as "checks,
language defined, controlled by Assertion_Policy" or something like that. And
possibly something like: "Assertion_Policy, predicate check".

Since you were the one that created the original useful index, you ought to have
some idea on how to accomplish that. Not indexing this at all (which it the way
it is) doesn't seem acceptable.

> Anyway, check names are already completely broken -- we define their
> semantics only in the AARM, which is supposedly non-normative.
> That was a deliberate decision on my part, which I rationalized by
> "it's no worse than Ada 83".

True enough, although it's not quite true, in the sense that the list in
11.5 is thought to be complete (missing checks have been added, especially by
Ada 2005). But I agree that there the only real connection between check names
and actual checks is in the index and in the AARM - neither of which are
normative.

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

From: Bob Duff
Sent: Tuesday, May 10, 2011 4:11 PM

> I did think of a fourth option last night, which is to index these as
> "checks, language defined, controlled by Assertion_Policy" or
> something like that. And possibly something like: "Assertion_Policy, predicate check".

That sounds like a fine idea.

The index isn't supposed to be language-lawyerly-style normative wording, it's
supposed to be helpful to people who don't know every jot and tittle of Ada.

> Since you were the one that created the original useful index, you
> ought to have some idea on how to accomplish that. Not indexing this
> at all (which it the way it is) doesn't seem acceptable.

Well, I can't get too excited about this issue, so "unacceptable"
seems too strong.  But yeah, your plan above will give us reasonably useful
index entries, which is good.

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

From: Randy Brukardt
Sent: Thursday, June  2, 2011 9:14 PM

> > I did think of a fourth option last night, which is to index these
> > as "checks, language defined, controlled by Assertion_Policy" or
> > something like that. And possibly something like:
> "Assertion_Policy, predicate check".
>
> That sounds like a fine idea.
>
> The index isn't supposed to be language-lawyerly-style normative
> wording, it's supposed to be helpful to people who don't know every
> jot and tittle of Ada.

In adding these index entries, I happened to notice that 11.4.2(18/3) defines
the term "assertion policy" to mean the policy specified by the Assertion_Policy
pragma. However, in most of the new wording, we used "Assertion_Policy" instead.
(I noticed this because I had two similar index entries next to each other...)

As such, I'm going to fix all of the new wording to use "assertion policy"
instead of "Assertion_Policy". Not the most important change ever... (I also see
that there aren't the forward references needed for such a term, not matter how
it is spelled.)

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

Questions? Ask the ACAA Technical Agent