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

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

!standard 3.2.4(0)          11-01-23 AI05-0153-3/02
!class Amendment 09-05-27
!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 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.
!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 clause" is an aspect clause specifying 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 clause may be given on a type_declaration or a subtype_declaration, and applies to the declared subtype. In addition, predicate clauses 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 clauses that apply, and-ed together; if no predicate clauses apply, the predicate is True Redundant[(in particular, the predicate of a base subtype is True)].
Legality Rules
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;
[Author's Question: Does that allow "S in (Foo | Bar | Baz)"?]
- 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 clauses apply.
The prefix of an attribute_reference whose attribute_designator is First, Last, or Range shall not denote a subtype to which predicate clauses apply.
The discrete_subtype_definition of a loop_parameter_specification shall not denote a subtype to which Dynamic_Predicate clauses apply.
Dynamic Semantics
If the Assertion_Policy 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 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.
AARM Ramification: Predicates are not evaluated at the point of the [sub]type declaration.
If any of the above Legality Rules is violated in an instance of a generic unit, Program_Error is raised. AARM Note: This is usual way around the contract model.
Implementation Permissions
A predicate check may be omitted if the subtype with the predicate statically matches the nominal subtype of the value being checked. [???I'm not sure this is the right rule. But I don't think the exact rule here is important, and I'd prefer to argue about it after dealing with all the other stuff.]
AARM Reason: Well-behaved predicates should not have side effects that matter, so omitting the check is pretty harmless. It is possible to write non-well-behaved predicates, which is why the permission is needed. If the implementation does omit a predicate check, it cannot later assume that the predicate was True.
NOTE: A predicate clause does not cause a subtype to be considered "constrained".
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.
[End of 3.2.4.]
3.8.1(5,11) says:
5 discrete_choice ::= expression | discrete_range | others
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,11,15) so the full coverage rules take predicates into account. This applies only in the static case (by existing wording):
5 discrete_choice ::= choice_expression | discrete_subtype_indication | range | others [Note: AI-158 changes "expression" to "choice_expression". We are no longer using discrete_range here, because it's not necessarily a contiguous range.]
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.5.2(29) so membership tests take the predicate into account:
The tested type is scalar, and the value of the simple_expression belongs to the given range, or the range of the named subtype {and the predicate of the named subtype evaluates to True}; or
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 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 clauses 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 clauses 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. {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.}
[Author's question: Is that reasonable to implement?]
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}{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{, the 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 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").
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, 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?
---
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.2(2)
!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.

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

[The following mail should go into a new AI, still TBD:]

From: Bob Duff
Sent: Monday, January 24, 2011  9:52 AM

> P.S. should we have a restriction
>
> No_Implementation_Aspects

Yes, good idea.

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

From: Bob Duff
Sent: Monday, January 24, 2011  10:02 AM

By the way, obviously some folks would like to forbid Dynamic_Predicate, so
there should be a restriction for that.  Instead of doing it piecemeal, we
should do like we did for No_Dependence, and have a general feature for
forbidding any aspect.  Something like:

    pragma Restrictions (No_Aspect => Dynamic_Predicate);

We could have an enum type somewhere that lists all the aspect names.  Or we
could just allow an "aspect_identifier" there, without involving visibility --
like pragma arguments.  For aspects that are also attributes or pragmas, the
restriction should forbid both forms.

I've got no problem with self-imposed or project-imposed restrictions!  If,
someday, some customer requests No_Evil_Predicates, I expect AdaCore would
implement it (if we can come up with a coherent definition of "evil").

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

From: Tucker Taft
Sent: Monday, January 24, 2011  10:19 AM

Or perhaps something like:

   pragma Restrictions(No_Aspect_Specification => Dynamic_Predicate);

to be analogous to "No_Dependence => ...".

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

From: Bob Duff
Sent: Monday, January 24, 2011  10:38 AM

Yes, that's better.  For those aspects that are also attributes, you probably
want to restrict the specification, but not the query.

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

From: Robert Dewar
Sent: Tuesday, January 25, 2011   6:14 AM

> Or perhaps something like:
>
>     pragma Restrictions(No_Aspect_Specification =>
> Dynamic_Predicate);
>
> to be analogous to "No_Dependence =>  ...".

Can't we just have

   No_Aspect => name

I see no advantage to reader or writer in adding the Specification part here,
especially if it also bans a corresponding pragma or attribute.

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

From: Robert Dewar
Sent: Tuesday, January 25, 2011   6:15 AM

> Yes, that's better.  For those aspects that are also attributes, you
> probably want to restrict the specification, but not the query.
>
>> to be analogous to "No_Dependence =>  ...".

OK, I see, grumble, I guess the long name will have to do

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

From: Robert Dewar
Sent: Monday, July 26, 2010   7:46 PM

Implementations are allowed to add grandchildren to Ada etc. And GNAT
takes advantage of this, e.g. to add the encoding packages to earlier
versions of Ada.

But this creates portability problems, we should really have a
restriction to prevent this, in the style of No_Implementation_Pragmas.

How about No_Implementation_Units

?

I am not really suggesting a new AI at this stage, just some guidance
on whether this is a good idea so that implementations can adopt it
(and then we can put it into Ada 2019 :-))

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

From: Tucker Taft
Sent: Monday, July 26, 2010   8:14 PM

This sounds like a very good idea.
Users are often confused about what
packages are "standard" Ada and what
are not.

Does this also cover System.* and Interfaces.*?
One rule might be to disallow any package that starts with "Ada", "System",
or "Interfaces" that is not in the reference manual.  These are the ones
that confuse users.

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

From: Robert Dewar
Sent: Monday, July 26, 2010   8:33 PM

Right, that's what I had in mind.

And the idea would be in particular to forbid use of RM packages in an
inappropriately earlier version of Ada (e.g. using the string encoding packages
in Ada 2005 mode). Of course I know that can't be part of the standard, but
that would be the encouraged usage (and is what GNAT intends to do).

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

Questions? Ask the ACAA Technical Agent