!standard 3.2.4(0) 10-10-08 AI05-0153-3/01 !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. If a predicate obeys certain restrictions, the subtype is considered static, and can therefore be used as a choice in case statements and the like. 'for' loops are also defined over static subtypes with 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 type 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 a new aspect "Predicate", which takes 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. For example: type T is ...; function Is_Good(X: T) return Boolean; subtype Good_T is T with 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 Predicates are defined to be static. For example, subtype Letter is Character with 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 aspect Predicate is defined for subtypes. Name Resolution Rules The expected type for a Predicate expression is any boolean type. Legality Rules A Predicate may be specified on a type_declaration or a subtype_declaration; if none is given, an implicit "with Predicate => True" is assumed. The predicate of a subtype is defined as follows: - For a (first) subtype defined by a derived type declaration, the specified Predicate, and-ed with the predicate of the parent subtype, and-ed with the predicates of the progenitor subtypes. - For a (first) subtype defined by a non-derived type declaration, the specified Predicate. - For a subtype created by a subtype_declaration, the specified Predicate, and-ed with the predicate of the subtype denoted by the subtype_mark. - For a subtype created by a subtype_indication that is not that of a subtype_declaration, the predicate of the subtype denoted by the subtype_mark. - For a base subtype, True. 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 with a user-specified predicate. The discrete_subtype_definition of a loop_parameter_specification shall not denote a subtype with a user-specified predicate, unless the subtype is static. The prefix of an attribute_reference shall not denote a subtype with a user-specified predicate if the attribute_designator is First, Last, or Range. 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 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. [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 predicates of certain forms are static: Also, a subtype is static only if the predicate is predicate-static. Add new paragraphs after 4.9(32), to define the term "predicate-static" used above in 4.9(26/2): An expression within a predicate is "predicate-static" if it 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; - a call to 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. 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. ... [???Should we allow matching for predicates that happen to have all the same values, in the static case? I think not.] 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.} 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: Predicate => True -- which is what you get by default Predicate => 1 > 0 -- static expression with value True Predicate => Cur_Inst in 1..10 -- contiguous range 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 far 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 predicate-static 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 if X is the current instance, then the subtype is not static. 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 Predicate => Letter in 'A'..'Z' | 'a'..'z'; case Current_Char is when Letter => ... -- Allowed by this AI. 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 rougly proportional to the size of the relevant source text. For example: subtype Even is Natural with Predicate => Cur_Inst mod 2 = 0; -- not predicate-static! 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". Note that the definition of static subtypes allows predicates coming from other subtypes: subtype S1 is Natural with Predicate => S1 < 100 or S1 > 1000; subtype S2 is S1 with 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. We considered using a different name (perhaps Set_Predicate or Static_Predicate) for the static case. We also considered using a completely different syntax for the static case -- that's essentially the AI05-0153-2 version of this AI). One problem is that if you change a static predicate to a nonstatic one, faraway parts of your program can become illegal. However: - 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; 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 user-defined Predicate, but only if S is static. 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 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 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 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 Predicate => ...; X: S; -- neither constraint nor predicate is checked The idea is that X will be initialized later, and the range at 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 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 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 Predicate => S1 in 1..10; subtype S2 is Integer with Predicate => S2 in 4..20; subtype S3 is Integer with 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 Predicate => Type_Symbol_Ptr.Entity = A_Type; subtype Callable_Symbol_Ptr is not null Symbol_Ptr with 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. "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 ****************************************************************