Version 1.1 of ai05s/ai05-0153-3.txt
!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 => ... --
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; --
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 --
...
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
... --
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
... --
case X is
when 10 => X := 200; --
when 300 => exit; --
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); --
procedure Do_It (P : in out Decimal_Rec) is
begin
P.A := 5; --
Put (Obj in Decimal_Rec); --
end Do_It;
Do_It (Obj); --
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; --
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; --
Y: S := null; --
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; --
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; --
case ... is
when S3 => --
But:
case ... is
when S1 | S2 => --
----------------
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
****************************************************************
Questions? Ask the ACAA Technical Agent