CVS difference for ai05s/ai05-0153-1.txt

Differences between 1.7 and version 1.8
Log of other versions for file ai05s/ai05-0153-1.txt

--- ai05s/ai05-0153-1.txt	2010/04/08 02:00:07	1.7
+++ ai05s/ai05-0153-1.txt	2010/04/29 04:18:06	1.8
@@ -1,4 +1,4 @@
-!standard  3.2.2(2)                                   10-02-11    AI05-0153-1/04
+!standard  3.2.4(0)                                10-04-27    AI05-0153-1/05
 !class Amendment 09-05-27
 !status work item 09-05-27
 !status received 09-05-27
@@ -8,7 +8,9 @@
 
 !summary
 
-Add subtype predicates to the language.
+Add subtype predicates to the language. Predicates are checked on every subtype
+conversion (which includes assignments, most cases of parameter passing, etc),
+and on all parameter passing.
 
 !problem
 
@@ -26,128 +28,159 @@
 
 !wording
 
-[Author's note: This very simple proposal is closest to my original
-intent. It is likely to be cheap to implement and fairly powerful,
-but could create some anomolies. A less powerful proposal better
-integrated into the language (but far more expensive to implement
-is given in AI05-0153-2)].
+This AI depends on AI05-0183-1, which defines a syntax for
+aspect_specifications, which may be attached to declarations.
 
-We depend on the following part of AI05-0183-1:
+Informal: 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.
 
-Replace 3.2.2(2) with:
+AARM-3.2(1.b/2) says:
 
-subtype_declaration ::=
-   subtype defining_identifier is subtype_indication [aspect_clause];
+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.
 
-Informal: We define a new aspect "Predicate". It takes a Boolean_expression.
-The Boolean_expression could use the defining_identifier of the
-subtype, to mean the "current instance" of the subtype (that is,
-the object to test the predicate against). [Editor's note:
-I'll leave the formal wording of this to Tucker's proposal. No
-sense in beating my head on a wall to figure this out!]
+Change it to:
 
-The actual predicate is the given expression anded with the predicate
-(if any) of the parent subtype. (The predicate of any subtype that
-does not have one can be assumed to be the boolean literal True.)
+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.
 
-[Editor's note: The predicate has no effect on the static or
-dynamic semantics of the subtype indication except as noted here. In
-particular, it has no effect on the range of scalar subtypes.]
+RM-3.2(8/2) says:
 
-Bounded Errors [where to put this?? It seems related to 13.9.1 - Data validity]
+    ...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.
 
-It is a bounded error to use a value or access an object of a subtype that has
-a predicate to violate the predicate (that is, for the predicate to evaluate
-to false on the value or object). If the error is detected,
-Assertions.Predicate_Error or Program_Error is raised; otherwise, the use
-of the value or access of the object proceeds normally. An implementation
-may evaluate a predicate at any such use or access in order to detect this
-bounded error.
+Change it to:
 
-[Editor's note: We allow Program_Error because all bounded errors can raise
-Program_Error. The "proceeds normally" wording is the same as 4.8(11.1/2).]
+    ...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 any predicate.
 
-AARM Ramification: An implementation can evaluate a predicate any time an
-object is accessed in any way, if it desires. We have to say this so that
-any side-effects of the predicate (bad practice, but surely allowed) cannot
-be depended upon. Note that this isn't the same as being allowed to check
-the predicate anywhere at all; there has to be some use of a value or object
-that has the subtype. That's necessary so that it is possible to write
-the predicate without an evaluation of itself being triggered.
 
-Add to the end of 3.3.1(18/2) (which describes the meaning of "initialized
-by default"):
+Add new section 3.2.4:
 
-If the nominal subtype has a predicate, the predicate is applied to the
-object and Assertions.Predicate_Error is raised if the result is False.
+3.2.4 Subtype Predicates
 
-[Editor's note: We need to check that default initialized objects don't violate
-their predicate.]
+The language-defined aspect Predicate is defined for subtypes.
+The expected type for a Predicate expression is any boolean type.
 
-Modify 3.4(18-22/2):
+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:
 
-Informally, the predicate of the corresponding subtype is that of the
-subtype of the parent/progenitor type anded with the predicate of the
-derived type. The new (sub)type is considered to have a predicate (even if none
-is explicitly given).
+    - 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.
 
-AARM Reason: If a subprogram has parameter(s) whose subtype(s) have
-defined predicate(s), the generated code of the subprogram body may depend on
-those predicates being checked. (A compiler could assume that they had been
-checked at the point of a call.) If the predicates did not compose, a call
-of the derived subprogram might not actually check the predicates, and that
-would cause big trouble.
+    - For a (first) subtype defined by a non-derived type declaration,
+      the specified Predicate.
 
-Add as the last sentence of 3.6(9):
+    - For a subtype created by a subtype_declaration, the specified Predicate,
+      and-ed with the predicate of the subtype denoted by the subtype_mark.
 
-An index subtype shall not statically denote a subtype with a predicate.
+    - 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.
 
-Add as the last sentence of 3.6(21):
+    - For a base subtype, True.
 
-The elaboration of an array_type_definition raises Program_Error if the index
-subtype has a predicate.
+    [???I don't think we need to say anything about ranges or discrete_ranges,
+    here.]
 
-AARM Reason: We don't want to create "holey" array types; it is very confusing
-as to whether the values for which the predicate returns False have associated
-elements. By raising Program_Error, we prevent generic contract problems. But we
-also have a legality rule so when it is statically known (outside of a generic)
-we detect the problem at compile-time.]
+[Editor's note: The predicate has no effect on the static or dynamic semantics of the subtype indication except as noted here. In particular, it has no effect on the range of scalar subtypes.]
 
-Add after 3.6.1(5):
 
-The discrete_range of an index_constraint shall not statically denote a
-subtype with a predicate.
+                               Dynamic Semantics
 
-Add as the last sentence of 3.6.1(8):
+On every subtype conversion, the predicate of the target subtype is evaluated,
+and a check is made that the predicate is True. Redundant[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.
 
-The elaboration of an index_constraint raises Program_Error if any
-discrete_range is a subtype with a predicate.
+AARM Ramification: Predicates are not evaluated at the point of the [sub]type
+declaration.
 
-AARM Reason: We don't want to create "holey" array subtypes. By raising
-Program_Error, we prevent generic contract problems. But we also have a legality
-rule so when it is statically known (outside of a generic) we detect the problem
-at compile-time.]
+AARM Ramification: Predicates are not checked on object creation for elementary
+types. For composite types, they are checked only if there are default values,
+and only if those defaults are used. Also, only for explicit defaults -- the
+implicit default of null for access types doesn't count.
 
-Add after 4.1.2(4):
 
-Legality Rules
+                                Legality Rules
 
-The discrete_range of a slice shall not statically denote a subtype with
-a predicate.
+An index subtype, discrete_range of an index_constraint or slice, or a
+discrete_subtype_definition is illegal if it statically denotes a subtype with a
+user-specified predicate.
 
-Add as the last sentence of 4.1.2(7):
+[???Question: The above disallows for loops. Maybe we should allow predicates
+for the discrete_subtype_definition of a loop_parameter_specification. The
+implementation model for:
 
-The evaluation of a slice raises Program_Error if any discrete_range is a
-subtype with a predicate.
+    for X in S loop ...
 
-AARM Reason: We don't want to create "holey" slices, especially as slices can be
-required to be passed by reference (for by-reference component types), and ignoring
-the predicate would be very confusing. By raising Program_Error, we prevent generic
-contract problems. But we also have a
-legality rule so when it is statically known (outside of a generic) we detect
-the problem at compile-time.]
+would be:
 
+    for X in S'Range loop
+        if X'Predicate then
+            ...
+]
 
+                               Dynamic Semantics
+
+The elaboration of the declaration or body of an instance of a generic unit
+raises Program_Error if it contains an index subtype, discrete_range of an
+index_constraint or slice, or a discrete_subtype_definition with a
+user-specified predicate.
+
+AARM Reason: We don't want to have arrays with holes determined by arbitrary
+predicate expressions -- that would be very confusing. The same goes for entry
+families. It would be particularly troublesome for slices that are required to
+be passed by reference. The run-time check is needed to prevent generic contract
+model problems, but we also have a legality rule for cases where we can detect
+the problem at compile time.
+
+                          Implementation Permissions
+
+A predicate check may be omitted if the subtype with the predicate statically
+matches the nominal subtype of the value being checked.
+
+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.]
+
+6.4.1(13) says:
+
+13      * For an access type, the formal parameter is initialized from the
+          value of the actual, without a constraint check;
+
+Change it to:
+
+13      * For an access type, the formal parameter is initialized from the
+          value of the actual, without any constraint, null-exclusion, or
+          predicate checks;
+
 Modify 4.5.2(29):
 
 The tested type is scalar, and the value of the simple_expression belongs
@@ -164,130 +197,82 @@
 evaluated to True,} and:
 
 Add at the end of 4.6(51/2):
-
-If the target subtype has a predicate, the predicate is applied to the value
-and Assertions.Predicate_Error is raised if the result is False.
-
-Add after 4.6(58):
-
-Implementation Permissions
 
-If the target subtype of a conversion has a predicate, and the nominal subtype
-of the operand is that same subtype, an implementation may omit the application
-of a predicate to the operand.
+If the target subtype has a predicate, the predicate is applied to the value and
+Assertions.Assertion_Error is raised if the result is False.
 
-AARM Reason: We have to say this because (bad) predicates can have side-effects,
-and because intermediate operations can make good predicates become False. For
-instance, assignment to individual components of a record type might cause the
-value to violate a previously checked predicate.
-
-AARM Discussion: If the implementation does omit the check of the predicate, it
-cannot later assume that the predicate is true.
-
 Modify 4.9.1(2/2):
 
 A subtype statically matches another subtype of the same type if they have
 statically matching constraints, {neither has a predicate or both predicates
-come from the same predicate_clause, }and, for access subtypes, either both
-or neither exclude null. ...
+come from the same predicate_clause, }and, for access subtypes, either both or
+neither exclude null. ...
 
-Add after 11.4.2(13/2):
+Modify 6.4.1(13/3) (as modifed by AI05-0196-1):
 
-Predicate_Error : exception; -- See 4.6
+For an access type, the formal parameter is initialized from the value of the
+actual, without checking that the value satisfies any
+constraint{, any predicate,} or any exclusion of the null value;
 
 
 !discussion
 
-This proposal seems similar to type invariants on the surface. However,
-these two constructs solve different problems. A type invariant is a
-requirement on all values of a type outside of the type's defining
-package(s). In particular, it does not vary depending on the view of
-an object. A constraint and/or predicate is a requirement on a particular
-view of an object. It can be different on different views of the same object
-(as in a formal parameter). Thus it can be used to specify temporary or
-transient requirements on an object.
+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.
+
+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".
 
-The model here is that a predicate has *no* effect on the static or dynamic
-semantics of a constraint. That is, if a predicate is applied to an indefinite
-type, the resulting subtype is indefinite. If a predicate is applied to an
-unconstrained subtype, the resulting subtype is unconstrained. And so on.
+    - Therefore, invariants are only allowed for private TYPES,
+      whereas predicates are allowed for any SUBtype.
 
-This mirrors the semantics of null exclusions (which also are not constraints).
-
-Note that this could have lead to some unusual circumstances:
-
-     subtype Even is Integer range 1 .. 10 with Predicate => Even mod 2 = 0;
-     type Evens is array (Even) of Boolean; -- 5 or 10 elements?
-     Obj : Evens;
-     Obj(1) := False; -- Would Raise Predicate_Error.
-
-Type Evens has length 10. Evens'range goes from 1 .. 10. However, attempting
-to index component 1 will raise Predicate_Error. (That's because 1 will be converted
-to subtype Even, as noted in 4.1.1(7), and that will trigger a predicate check.)
-However, the situation gets nastier still when arrays are sliced by subtypes with a
-predicate:
-
-    Str : String := "1234567890";
-
-    Put(Str(Even));
-
-One might expect to have "24680" printed, but since the constraints are unchanged,
-"1234567890" would actually be printed. Because of this weird behavior, we do not
-allow predicates on index subtypes. In order to avoid breaking the contract
-model, we raise Program_Error in generic bodies if the subtype has a predicate.
-
 ---
 
-Originally, this proposal made predicates "user-defined constraints". This
-does not work, however, for a number of reasons:
-(1) A predicate does not provide a unique value for bounds or discriminants,
-thus it is impossible to declare a composite object using such a constraint.
-We then have to define partially constrained subtypes.
-(2) A predicate does not clearly define 'First or 'Last values, so calling
-it a constraint on a scalar subtype brings up many nasty questions. For
-instance,
-     subtype Mapping is Integer range 1 .. 10 with Predicate => Map(Mapping);
-What is Even'First? Without analyzing the body of Map (which may not even have
-been written yet), we can't say. And even if we made it dynamic, Map may
-have side effects and not return the same answer each time it is called.
-(3) A predicate can depend on components other than discriminants. If a
-component is modified, the predicate can become false. This can happen at
-arbitrary points in the program. It is especially bad when the predicate is
-applied to an access type; it is easy to see how it could be violated.
+The model here is that a predicate has *no* effect on the static or dynamic semantics of a constraint. That is, if a predicate is applied to an indefinite type, the resulting subtype is indefinite. If a predicate is applied to an unconstrained subtype, th
e resulting subtype is unconstrained. And so on.
 
-These problems can be worked around by adding various restrictions, but that
-just makes predicates less useful and far more complex.
+This mirrors the semantics of null exclusions (which also are not constraints).
 
 ---
 
-We define predicates to be part of static matching, so that subtypes with
-different predicates are not considered identical.
+We define predicates to be part of static matching, so that subtypes with different predicates are not considered identical.
 
 ---
 
-An alternative way of looking at predicates is to assume that all subtypes
-have a predicate of True by default, and a predicate aspect just replaces
-that with something user-defined. The wording would have to be very different
-in that case.
+???The following para is obsolete, but I'm leaving it in for discussion purposes.
 
----
+  The exception "Constraint_Error" seems wrong for something that is not a
+  constraint. Therefore, failed predicates raise Predicate_Error. This seems
+  necessary in order to avoid confusing constraint checks (which generally can
+  be assumed to remain True after the first check) with predicate checks (which
+  generally cannot be assumed to be remain True).
+
+Bob replies: If we have Predicate_Error, then we should have Precondition_Error
+and Postcondition_Error. But we don't: Those just use Assertion_Error. So I got
+rid of Predicate_Error, and used Assertion_Error.
+
+I'd be just as happy with Constraint_Error. Null exclusions use
+Constraint_Error, even though they aren't constraints. And Constraint_Error is
+used for a whole bunch of other not-quite-constraint things.
 
-The exception "Constraint_Error" seems wrong for something that is not a
-constraint. Therefore, failed predicates raise Predicate_Error. This seems
-necessary in order to avoid confusing constraint checks (which generally can
-be assumed to remain True after the first check) with predicate checks (which
-generally cannot be assumed to be remain True).
-
 ---
 
-Note that predicates are only true at the point where the language does a
-subtype conversion into the subtype, and immediately after default initialization.
-Depending on the predicate, later operations can make the predicate False. This
-is not a major problem for the primary intended use of predicates (on formal
-subprogram parameters), but could be an issue if they are used on subtypes
-in other contexts.
+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:
 
@@ -305,12 +290,32 @@
 
    Do_It (Obj); -- (2)
    Put (Obj in Decimal_Rec); -- (3)
+
+The predicate on Decimal_Rec will be checked at (1). However, after the call at
+(2), the predicate is no longer True for Obj. The call at (3) will print False.
 
-The predicate on Decimal_Rec will be checked on the aggregate at (1).
-However, after the call at (2), the predicate is no longer true for Obj.
-The call at (3) will print False. Implementations are allowed to check
+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 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 anywhere at all -- that would allow the implementation to introduce
+arbitrary race conditions into the program!
 
+???Question: Should we reconsider this?  Perhaps allow a predicate check on any
+read of an object. Or any read of part of an object?
+
+
 !example
 
 In a compiler familar to the author, type Symbol_Ptr references a symbol
@@ -326,12 +331,13 @@
 
     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;
+    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;
 
@@ -344,6 +350,32 @@
 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
@@ -3104,5 +3136,206 @@
 compiler-like programs in any way. It's just like constraints, except you can do
 more than just subranges of scalars, and single-values for discrims, etc. (And
 it's not quite as airtight as those, but oh, well.)
+
+****************************************************************
+
+From: Bob Duff
+Date: Wednesday, April 28, 2010  5:30 PM
+
+Here's a new version of AI05-0153-1 (subtype predicates), for tomorrow's
+discussion.
+
+We might want to decide that this stuff is too immature to include in Ada 2012.
+If so, I think GNAT will experiment with implementing this stuff, and using it.
+That might be a better approach than standardizing something that we're not sure
+is 100% right.
+
+If this AI is not included in Ada 2012, I am strongly opposed to including type
+invariants, for reasons I've already stated. In that case, perhaps compiler
+writers can experiment with invariants, too.
+
+I did a lot of rewriting.  One thing I should mention: I removed the
+philosophical ramblings that I found objectionable, and replaced them with an
+objective (I hope) list of differences between predicates and invariants (and
+between predicates and constraints). Hopefully, we can all agree on what the
+differences are, even if I think those differences are minor, whereas Randy and
+others think they are major.
+
+[Following is version /05 of the AI.]
+
+****************************************************************
+
+From: Randy Brukardt
+Date: Wednesday, April 28, 2010  11:15 PM
+
+> Here's a new version of AI05-0153-1 (subtype predicates), for
+> tomorrow's discussion.
+
+A few comments.
+
+...
+> 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.
+>
+> Change 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 any predicate.
+
+Here is where we disagree. I don't think a predicate can or should have any
+effect on the values of a subtype, because that changes all of the rules
+involving validity, how iterations work, and the like. If we're doing those
+things, we need to greatly restrict the forms of the predicates, and I think
+that is a very bad idea (this "looks" general). If we're *not* doing those
+things, then lots of rewording is needed.
+
+> Add new section 3.2.4:
+>
+> 3.2.4 Subtype Predicates
+...
+
+>                                Dynamic Semantics
+>
+> On every subtype conversion, the predicate of the target subtype is
+> evaluated, and a check is made that the predicate is True.
+> Redundant[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.
+
+Rules about subtype conversions belong in 4.6. We've been *very* careful to
+maintain that up to this point, and I don't think we should start distributing
+those (especially only in a few cases).
+
+...
+> An index subtype, discrete_range of an index_constraint or slice, or a
+> discrete_subtype_definition is illegal if it statically denotes a
+> subtype with a user-specified predicate.
+
+All of these forward references need section references. (That's why I put those
+rules in the appropriate clauses: to avoid the forward references.)
+
+...
+>
+> 6.4.1(13) says:
+>
+> 13      * For an access type, the formal parameter is initialized from the
+>           value of the actual, without a constraint check;
+>
+> Change it to:
+>
+> 13      * For an access type, the formal parameter is initialized from the
+>           value of the actual, without any constraint, null-exclusion, or
+>           predicate checks;
+
+We changed this wording in AI05-0196-1, approved in Burlington. Moreover this is
+out of order in the AI (clauses are supposed to come in order). The current
+wording is:
+
+For an access type, the formal parameter is initialized from the value of the
+actual, without checking that the value satisfies any constraint or any
+exclusion of the null value;
+
+because what a "constraint check" is not well-defined.
+
+...
+> Add at the end of 4.6(51/2):
+>
+> If the target subtype has a predicate, the predicate is applied to the
+> value and Assertions.Predicate_Error is raised if the result is False.
+
+I think you mean Assertion_Error here. I changed it.
+
+> !discussion
+>
+> 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.
+
+On this bullet, I think our only difference is a matter of degree. It's unlikely
+that anyone will write well-behaved predicates for composite types. The only
+ones that could qualify only involve bounds or discriminants (directly, no
+dereferencing). It's easy to see that: all of the fancy rules that keep access
+to constrained discriminated types from causing problems aren't going to be
+enforced for predicates. So depending on anything other than discriminants will
+not be "well-behaved".
+
+The other major difference between a predicate and a constraint is that the
+predicate cannot affect the value set for the type. If it did, then validity
+would depend on the predicate, and since that cannot be trusted in general, it
+would be impossible to do any reasoning about validity of objects. Which would
+make any check elimination (not just predicate checks, but any check)
+technically wrong - a result we surely don't want.
+
+We had a HUGE amount of trouble with the value set for null exclusions, and this
+would be many times worse. I really don't even want to think about it -- you
+would have to do the careful research to prove that there is no problem (and
+explain why you think that) before I'd even consider voting to abstain on a
+proposal changing the value set based on arbitrary expressions potentially with
+side-effects.
+
+...
+> ???The following para is obsolete, but I'm leaving it in for
+> discussion purposes.
+>
+>   The exception "Constraint_Error" seems wrong for something that is not a
+>   constraint. Therefore, failed predicates raise Predicate_Error. This seems
+>   necessary in order to avoid confusing constraint checks (which generally can
+>   be assumed to remain True after the first check) with predicate checks (which
+>   generally cannot be assumed to be remain True).
+>
+> Bob replies: If we have Predicate_Error, then we should have
+> Precondition_Error and Postcondition_Error. But we don't:
+> Those just use Assertion_Error. So I got rid of Predicate_Error, and
+> used Assertion_Error.
+
+They *should* use Precondition_Error and Postcondition_Error; they're not
+assertions (not in my world anyway; I don't want them at all if they are "just"
+assertions).
+
+> I'd be just as happy with Constraint_Error. Null exclusions use
+> Constraint_Error, even though they aren't constraints.
+> And Constraint_Error is used for a whole bunch of other
+> not-quite-constraint things.
+
+That's true; it really depends on whether you use the names of the exceptions as
+debugging information or you just want to use one and assume your IDE+runtime
+bails you out as to the cause of the problem. With Claw, we used a set of
+different exceptions for different causes, but not one for every possible error
+(about the same level as IO_Exceptions). I think the same would be appropriate
+here.
+
+So I could see using the same exception for Preconditions and Postconditions
+(and maybe even predicates), but I don't think those should be shared with
+anything else.
+
+This is something we could literally argue forever. Not a big deal in any case.
+
+...
+>     subtype Callable_Symbol_Ptr is not null Symbol_Ptr with
+>        Predicate => Callable_Symbol_Ptr.Entity in (Proc, Func, An_Entry);
+
+I'd prefer that you don't use unapproved AIs in examples, unless you really need
+to. This one has serious resolution issues and I for one don't think that they
+can be solved in the general case currently proposed. I left this as I
+originally had it.
 
 ****************************************************************

Questions? Ask the ACAA Technical Agent