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

Differences between 1.4 and version 1.5
Log of other versions for file ai05s/ai05-0290-1.txt

--- ai05s/ai05-0290-1.txt	2012/03/17 04:18:16	1.4
+++ ai05s/ai05-0290-1.txt	2012/03/17 07:00:18	1.5
@@ -1,4 +1,6 @@
-!standard  3.2.4(0)                               12-02-26    AI05-0290-1/04
+!standard  2.8(3)                                12-02-28    AI05-0290-1/05
+!standard  2.8(4)
+!standard  3.2.4(0)
 !standard  6.1.1(0)
 !standard  7.3.2(0)
 !standard 11.4.2(5/2)
@@ -20,7 +22,8 @@
 !summary
 
 The pragma Assertion_Policy is expanded to allow control of assertion
-expressions in a way that is very similar to pragma Suppress. 
+expressions in a way that is very similar to pragma Suppress, but
+without the possible consequence of erroneous execution.
 
 A perceived problem with Pragma Suppress for inlined calls is fixed.
 
@@ -40,12 +43,15 @@
 postconditions and invariants) are less important - actions of the client
 should not be able to cause these to fail.
 
-Hence, there needs to be fine control over the checks of various kinds
-of assertions. Control for any but the Assert Pragma cannot be
+Hence, there needs to be fine control over the checks of various
+kinds of assertions. Control for any but the Assert Pragma cannot be
 sensibly based on a policy in effect at the point of the check. For
-example, this would make invariant checks to be performed only occasionally. 
-The proposal that the policy in effect at the time of the aspect specification 
-controls all its checks.
+example, this would cause invariant checks to be performed only
+occasionally. The proposal is generally that the policy in effect
+at the time of the aspect specification controls all its checks.
+Subtype predicates use a somewhat different rule, but a key feature
+is that when the policy is "Ignore," the assertion expressions that are
+not evaluated because of the policy are *not* assumed to be true.
 
 !proposal
 
@@ -55,7 +61,7 @@
 
 Modify 2.8(3-4) as follows:
 
-  pragma_argument_association ::= 
+  pragma_argument_association ::=
      [pragma_argument_identifier =>] name
    | [pragma_argument_identifier =>] expression
 {  | [pragma_argument_aspect_mark =>] name
@@ -63,45 +69,105 @@
 
   In a pragma, any pragma_argument_associations without a
   pragma_argument_identifier {or pragma_argument_aspect_mark} shall
-  precede any associations with a pragma_argument_identifier {or 
+  precede any associations with a pragma_argument_identifier {or
   pragma_argument_aspect_mark}.
-  
 
+
 -------------
 
-modify 3.2.4() to:
+modify 3.2.4(22/3-23/3) to be:
 
-   The *predicate* of a subtype consists of {the "and" of} all predicate
-   specifications that apply {to it and occur at a point where the
-   assertion policy in effect requires the corresponding
-   Static_Predicate or Dynamic_Predicate check}[, and-ed together]; if
-   {there are} no {such} predicate specifications[ apply], the predicate
-   is True [Redundant: (in particular, the predicate of a base subtype
-   is True)].
+If required by the Static_Predicate or Dynamic_Predicate assertion
+policies (see 11.4.2) in effect at the point of the use of a
+subtype_mark that denotes a given subtype, the predicate check is
+@i(enabled) for the subtype of the entity or expression to which the
+subtype_mark applies.
+
+  AARM Discussion: The Assertion_Policy for subtype predicate aspects is
+  relevant at the following places where a subtype_mark can occur: alone
+  or as part of a subtype_indication that is defining the subtype of an
+  object (including a formal parameter, a function result, or a generic
+  formal object of mode IN), a component (including a discriminant), a
+  designated object, the parent of a derived type or the ancestor_part
+  of an extension_aggregate, and in an explicit type_conversion or
+  qualified_expression.  In other contexts, the Assertion_Policy is not
+  relevant, as no checks are directly tied to the predicate of the
+  subtype named by the subtype_mark.  In particular, when one subtype is
+  defined in terms of another, the predicate of the precursor subtype is
+  always carried over to the new subtype (and possibly augmented with
+  another predicate expression), and the Assertion_Policy at that point
+  is irrelevant.  What matters is the policy at the point where the new
+  subtype's subtype_mark is later used. This ensures that a
+  subtype_declaration that is merely used as a renaming, such as
+  "subtype S is P.S;" has no direct impact on predicate checks. What
+  matters is where S or P.S are used to define the subtype of an object,
+  and the Assertion_Policy in effect at the point of that object's
+  declaration.
+
+  We use the point of declaration of the object rather than the point of
+  delaration of the subtype because we want "subtype S is P.S;" to create
+  a true equivalence, and because we don't want to deal with "partial"
+  predicates, where some of the predicate checks of a subtype are enabled
+  while some are not.  We use the point of declaration of the object
+  rather than the point of the check, because we want a given predicate
+  to either apply completely or not at all to an object, to avoid
+  erroneous execution due to the use of an incorrect predicate when
+  the assertion policy is Ignore.
+
+
+[Redundant: On a subtype conversion where predicate checks are enabled
+for the target subtype, the predicate of the target subtype is
+evaluated, and a check is made that the predicate is True. If predicate
+checks are not enabled for the target subtype, the predicate is not
+evaluated. This includes subtype conversions as part of 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, if a predicate check is enabled for the subtype of the
+actual, the predicate of the subtype of the actual is evaluated, and a
+check is made that the predicate is True.
+
+If predicate checks are enabled for the nominal subtype of an object
+that is created by an object_declaration with no explicit initialization
+expression, by an uninitialized allocator, or by an ancestor_part of an
+extension_aggregate that is a subtype_mark, and one or more
+subcomponents have default_expressions, then the predicate of the
+nominal subtype is evaluated, and a check is made that it is True.
+
+Assertions.Assertion_Error is raised if any of the above predicate checks fail.
+
+modify 4.6 51/3 to be:
+
+After conversion of the value to the target type, if the target
+subtype is constrained, a check is performed that the value satisfies
+this constraint. If the target subtype excludes null, then a check is
+made that the value is not null. If predicate checks are enabled
+for the target subtype, the predicate of the target subtype is applied to the
+value and Assertions.Assertion_Error is raised if the result is False.
 
-delete 3.2.4 22/3.
+-------------
 
+modify 6.1.1. 19/3 to read
 
-   
--------------
+If required by the Pre, Pre'Class, Post, or Post'Class assertion
+policies (see 11.4.2) in effect at the point of a corresponding aspect
+specification applicable to a given subprogram or entry, then the
+checks for the respective preconditions or postconditions are @i(enabled)
+for that subprogram or entry.
 
+
 Modify 6.1.1 31/3 to:
- 
-If required by the Pre or Pre'Class assertion policies (see 11.4.2) in
-effect at the point of a corresponding aspect specification applicable to a
-given subprogram or entry, then upon a call of the subprogram or entry, after
-evaluating any actual parameters, precondition checks are performed as
-follows:
 
+Upon a call of the subprogram or entry, after evaluating any actual
+parameters, enabled checks for preconditions are performed as follows:
+
+Modify 6.1.1. 35/3, first sentence, to:
 
-Modify 6.1.1. 35/3 to: 
- 
-If required by the Post or Post'Class assertion policies (see 11.4.2) in
-effect at the point of a corresponding aspect specification applicable
-to a given subprogram or entry, then upon successful return from a call of the
-subprogram or entry, prior to copying back any by-copy in out or out
-parameters, the postcondition check is performed.
+Upon successful return from a call of the subprogram or entry, prior to
+copying back any by-copy in out or out parameters, any enabled checks
+for postconditions are performed.
 
+
 delete 6.1.1 40/3
 -------------
 
@@ -110,17 +176,20 @@
 If required by the Type_Invariant or Type_Invariant'Class assertion
 policies (see 11.4.2) in effect at the point of a corresponding aspect
 specification applicable to a type T, then an invariant check is
-performed at the following places, on the specified object(s):
+@i(enabled) for the type, and the check is performed at the following
+places, on the specified object(s):
 
 Delete 7.3.2 23/3
 
+-------------
+
 Replace 11.4.2, 5/2 - 7/2 by:
 
 The form of a pragma Assertion_Policy is as follows:
 
 pragma Assertion_Policy(policy_identifier);
-pragma Assertion_Policy(assertion_kind => policy_identifier
-                        {, assertion_kind => policy_identifier});
+pragma Assertion_Policy(@i(assertion)_aspect_mark => policy_identifier
+                        {, @i(assertion)_aspect_mark => policy_identifier});
 
 Pragma Assertion_Policy is allowed only immediately within a
 declarative_part, immediately within a package_specification, or as a
@@ -128,49 +197,55 @@
 
 -----
 
-Replace 11.4.2, 9/2 and 9/2a by: 
+Replace 11.4.2, 9/2 and 9/2a by:
 
-The assertion_kind of a pragma Assertion_Policy shall be one of
+The @i(assertion)_aspect_mark of a pragma Assertion_Policy shall be one of
 Assert, Static_Predicate, Dynamic_Predicate, Pre, Pre'Class, Post,
 Post'Class, Type_Invariant, Type_Invariant'Class, or some
 implementation defined aspect_mark. The policy_identifier shall be
-Ignore or Check or some implementation defined identifier.
+Ignore or Check or some implementation-defined identifier.
 
 [AARM:
 Implementation defined: Implementation-defined policy_identifiers and
-aspect_marks allowed in a pragma Assertion_Policy.]
+assertion_aspect_marks allowed in a pragma Assertion_Policy.]
 
 
 ------
 Replace 11.4.2, 10/2 by:
 
-Pragma Assertion_Policy determines for each assertion kind named in
-the argument associations whether assertions of the given kind are to be
-enforced by a run-time check. The policy_identifier Check requires that
-assertion expressions of the given kind be checked that they evaluate
-to True at the points specified for the given kind; the policy_identifier 
-Ignore requires that the assertion expression not be evaluated,
-and instead be treated as though it is simply the expression True. 
-If no assertion_kinds are specified in the pragma, the specified policy 
-applies to all assertion kinds.
-
-Pragma Assertion_Policy applies to the named assertion kinds in a
-specific region, and applies to all assertion expressions specified 
-in that region.  A Pragma
+Pragma Assertion_Policy determines for each assertion aspect named in
+the argument associations whether assertions of the given aspect are to
+be enforced by a run-time check. The policy_identifier Check requires
+that assertion expressions of the given aspect be checked that they
+evaluate to True at the points specified for the given aspect; the
+policy_identifier Ignore requires that the assertion expression not be
+evaluated at these points, and the run-time checks not be performed.
+Note that for subtype predicate aspects (see 3.2.4), even when the
+applicable Assertion_Policy is Ignore, the predicate will still be
+evaluated as part of membership tests and Valid attribute_references,
+and if static, will still have an effect on loop iteration over the
+subtype, and the selection of case_alternatives and variant_alternatives.
+
+If no assertion_aspect_marks are specified in the pragma, the specified
+policy applies to all assertion aspects.
+
+Pragma Assertion_Policy applies to the named assertion aspects in a
+specific region, and applies to all assertion expressions (or predicated
+subtype_marks -- see 3.2.4) specified in that region.  A pragma
 Assertion_Policy given in a declarative_part or immediately within a
-package_specification applies from the place of the pragma to the end
-of the innermost enclosing declarative region. The region for a Pragma
+package_specification applies from the place of the pragma to the end of
+the innermost enclosing declarative region. The region for a pragma
 Assertion_Policy given as a configuration pragma is the declarative
 region for the entire compilation unit (or units) to which it applies.
 
-If a Pragma Assertion_Policy applies to a generic_instantiation, then
-the Pragma Assertion_Policy also applies to the entire instance.
+If a pragma Assertion_Policy applies to a generic_instantiation, then
+the pragma Assertion_Policy applies to the entire instance.
 
-If multiple Assertion_Policy pragmas apply to a given construct for a given
-assertion kind, the assertion policy is determined by the one in the
-innermost enclosing declarative region specifying a policy for the
-assertion kind. If no such Assertion_Policy pragma exists, the policy
-is implementation defined.
+If multiple Assertion_Policy pragmas apply to a given construct for a
+given assertion aspect, the assertion policy is determined by the one in
+the innermost enclosing region of a pragma Assertion_Policy specifying a
+policy for the assertion aspect. If no such Assertion_Policy pragma
+exists, the policy is implementation defined.
 
 
 [AARM:
@@ -195,31 +270,103 @@
 
 <<< Note to Editor: 11.5 7.2/3, the inline part was deleted as part of
 these discussions.>>>
-shorten 11.5 7.2/3 to: 
+shorten 11.5 7.2/3 to:
 
 If a checking pragma applies to a generic instantiation, then the
-checking pragma also applies to the entire instance. 
-
-
--------------
+checking pragma also applies to the entire instance.
 
-
 ------------
 
 modify 11.5 25 to:
- 
-All_Checks 
+
+All_Checks
 
 Represents the union of all checks; suppressing All_Checks suppresses
 all checks.  In addition, an implementation is allowed (but not
 required) to behave as if a pragma Assertion_Policy(Ignore) applies to
 any region to which pragma Suppress(All_Checks) applies.
 
-===========================================
+!discussion
 
+In order to achieve the intended effect that library writers stay in
+control over the enforcement of pre- and postconditions as well as
+type invariants, the policy control needs to extend over all uses of
+the respective types and subprograms. The place of usage is
+irrelevant. This is enforced by the rules in the !wording.
+
+For Assert pragmas, the policy in effect for the place of the pragma is
+the controlling policy.
+
+For subtype predicates, the policy that is relevant is the one in effect
+at the point where the subtype_mark is used to define an object, or
+perform an explicit type_conversion or qualified_expression.
+
+The Assertion_Policy pragma allows control over each assertion aspect
+individually, if so desired. The need was clearly identified, e.g., to
+ensure enforcement of preconditions, while postconditions might be left
+to the whims of the library user.
+
+The regions to which Assertion_policy pragmas apply can be nested (as
+in the library example). The simple rule is that "inner" pragmas have
+precedence over "outer" pragmas for any given assertion aspect.
+
+Implementation-defined policies and assertion aspects are allowed in
+order that compiler vendors can experiment with more elaborate
+schemes.
+
+A clear separation was made between language checks that, if failing
+but suppressed, render the program erroneous, and assertions, for
+which suppression does not cause language issues that lead to
+erroneousness. This is one of the reasons why assertion control was
+not subsumed under the pragmas Suppress and Unsuppress with
+appropriate check names. For example, in verified code, the policy
+Ignore for Assertions make sense without impacting the program semantics.
+(Supressing a range check on the other hand can lead to abnormal values.)
+
+The ARG felt the following capability to be very useful, but shied away
+from extending the model so late in the production if the 2012 standard.
+Ada 2020 should consider this capability:
+
+Example: Imagine the following routine in GUI library:
+
+    procedure Show_Window (Window : in out Root_Window);
+       -- Shows the window.
+       -- Raises Not_Valid_Error if Window is not valid.
+
+We would like to be able to use a predicate to check the comment. With an
+"On_Failure" aspect we could do this without changing the semantics:
+
+    subtype Valid_Root_Window is Root_Window
+       with Dynamic_Predicate => Is_Valid (Valid_Root_Window),
+           On_Failure => Not_Valid_Error;
+
+    procedure Show_Window (Window : in out Valid_Root_Window);
+       -- Shows the window.
+
+If we didn't have the "On_Failure" aspect here, using the predicate as a
+precondition in lieu of a condition explicitly checked by the code would
+change the exception raised on this failure to be Assertion_Error. This
+would obviously not be acceptable for existing packages and too limiting
+for future packages. For upward compatibility, similar considerations
+apply to preconditions, so the "On_Failure" aspect is needed for them as
+well. We could also imagine that after one On_Failure aspect has been
+specified, additional preconditions could be defined for the same
+subprogram with distinct On_Failure aspects specifying distinct
+expressions to be raised.
 
-!discussion
+-----
 
+For pragma Inline (and for Assertion_Policy), we decided to eliminate
+the rule that said that the presence of a pragma Suppress or Unsuppress
+at the point of a call would affect the code inside the called body, if
+pragma Inline applies to the body. Given that inlining is merely advice,
+and is not supposed to have any significant semantic effect, having it
+affect the presence or absence of checks in the body, whether or not it
+is actually inlined, seemed unwise.  Furthermore, in many Ada compilers,
+the decision to inline may be made very late, so if the rule is instead
+interpreted as only having an effect if the body is in fact inlined, it
+is still a problem, because the decision to inline may be made after the
+decision is made whether to insert or omit checks.
 
 !ACATS Test
 
@@ -3693,5 +3840,1415 @@
 (I checked for all occurrences of assertion policy in the RM and AARM)
 
 4.9. 34/3 is another, but it is ok as is.
+
+****************************************************************
+
+From: Erhard Ploedereder
+Sent: Sunday, February 26, 2012  11:48 AM
+
+Discovery of 19/3 led to a simplification of 31/3 and 35/3 :
+
+modify 6.1.1. 19/3 to read
+
+If required by the Pre, Pre'Class, Post, or Post'Class assertion policies (see
+11.4.2) in effect at the point of a corresponding aspect specification
+applicable to a given subprogram or entry, then the respective preconditions and
+postconditions are considered to be enabled for that subprogram or entry.
+
+Modify 6.1.1 31/3 to:
+
+Upon a call of the subprogram or entry, after evaluating any actual parameters,
+checks for enabled preconditions are performed as follows:
+
+Modify 6.1.1. 35/3, first sentence, to:
+
+Upon successful return from a call of the subprogram or entry, prior to copying
+back any by-copy in out or out parameters, the check of enabled postconditions
+is performed.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Sunday, February 26, 2012  3:48 PM
+
+Query: for run time checks, the implementation can assume that no check is
+violated if checks are suppressed.
+
+This is certainly not true for ignoring assertions, a compiler should ignore
+assertions if they are off (GNAT at least in one case uses suppressed assertions
+to sharpen warning messages, the case is an assert of
+
+   pragma Assert (S'First = 1);
+
+which suppresses warnings about S'First possibly not being 1 even if assertions
+are suppressed. But warnings are insignificant semantically, so that's OK.
+
+What about preconditions and postconditions that are suppressed, are they also
+required to be totally ignored? Same question with predicates. If predicates are
+suppressed, I assume they still operate as expected in controlling loops etc??
+
+Sorry if this is confused!
+
+****************************************************************
+
+From: Erhard Ploedereder
+Sent: Monday, February 27, 2012  1:46 AM
+
+...
+> What about preconditions and postconditions that are suppressed, are
+> they also required to be totally ignored? Same question with
+> predicates. If predicates are suppressed, I assume they still operate
+> as expected in controlling loops etc??
+>
+> Sorry if this is confused!
+
+Present thinking is that assertions, pre- and postconditions and type invariants
+are ignored in the above sense. Compiler is not allowed to assume truth. I think
+that is a pretty solid position.
+
+On subtype predicates the jury is still out. It was written up as "ignored" in
+the above sense, but then we discovered some issues; that is the one issue
+remaining on the assertion control.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Monday, February 27, 2012  7:20 AM
+
+> Present thinking is that assertions, pre- and postconditions and type
+> invariants are ignored in the above sense. Compiler is not allowed to
+> assume truth. I think that is a pretty solid position.
+
+I think that makes sense. I am also thinking that perhaps in GNAT we will
+implement another setting, which says, assume these are True, but don't generate
+run-time code. That's clearly appropriate for things you have proved true.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Monday, February 27, 2012  10:13 AM
+
+> What about preconditions and postconditions that are suppressed, are
+> they also required to be totally ignored? Same question with
+> predicates. If predicates are suppressed, I assume they still operate
+> as expected in controlling loops etc??
+
+Pragma Suppress has no effect on pre/postconditions, except for pragma
+Suppress(All_Checks), which *allows* the implementation to interpret it as
+Assertion_Policy(Ignore). We intentionally do not want erroneousness to be
+associated with assertion-ish things like pre/postconditions, etc. The exact
+details of that are part of this AI, and for subtype predicates, are pretty
+subtle.  We decided we didn't like the solution currently proposed by this AI
+for subtype predicates, but we have agreed on a different approach which still
+avoids erroneousness.  I will be writing that up in the next couple of days.
+
+> Sorry if this is confused!
+
+This is a confusing area.  We spent several hours on this topic, and visited
+many different places in the design "space."  Personally, I feel pretty good
+about where we "landed," but I haven't written it up yet, so you will have to
+hang in there for a few more days before you will see the full story, at least
+with respect to subtype predicates.  But we all felt it was quite important that
+adding assertion-like things to a program and then specifying
+Assertion_Policy(Ignore) should *not* introduce erroneousness, even if your
+assertion-like things are incorrect.
+
+****************************************************************
+
+From: Steve Baird
+Sent: Monday, February 27, 2012  10:42 PM
+
+How does the design you have in mind handle the following example?
+
+     declare
+       pragma Assertion_Policy (Ignore);
+
+       subtype Non_Zero is Integer with Static_Predicate
+          => Non_Zero /= 0;
+
+       type Rec (D : Non_Zero) is
+         record
+            case D is
+               when Integer'First .. -1 => ...;
+               when 1 .. Integer'Last => ....;
+            end case;
+         end record;
+
+       Zero : Integer := Ident_Int (0);
+
+       X : Rec (D => Zero);
+
+I'm wondering about the general issue of how the Ignore assertion policy
+interacts with the coverage rules for case-ish constructs (case statements, case
+expressions, variant parts) when the nominal subtype is a static subtype with a
+Static_Predicate.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Tuesday, February 28, 2012  6:42 AM
+
+> I'm wondering about the general issue of how the Ignore assertion
+> policy interacts with the coverage rules for case-ish constructs (case
+> statements, case expressions, variant parts) when the nominal subtype
+> is a static subtype with a Static_Predicate.
+
+Ignore should only be about removing checks, not altering any of the other
+semantics of static predicates, it would not be acceptable at all for ignore to
+make a case statement illegal!
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Tuesday, February 28, 2012  9:03 AM
+
+>> I'm wondering about the general issue of how the Ignore assertion
+>> policy interacts with the coverage rules for case-ish constructs
+>> (case statements, case expressions, variant parts) when the nominal
+>> subtype is a static subtype with a Static_Predicate.
+>
+> Ignore should only be about removing checks, not altering any of the
+> other semantics of static predicates, it would not be acceptable at
+> all for ignore to make a case statement illegal!
+
+Correct.  The intent is "Ignore" means "ignore for the purpose of range checks."
+Any non-checking semantics remain, such as membership, full coverage, etc.  Case
+statements luckily include an option to raise Constraint_Error at run-time if
+the value is not covered for some reason (RM 5.4(13)).  The same is true for
+case expressions.  Variant records don't really have such a fall back, but we
+will have to be clear that even if Ignore applies where the discriminant subtype
+is specified, the subtype's predicate still determines whether or not a
+particular discriminant-dependent component exists.  It is as though there were
+a "when others => null;" alternative in the variant record, where the "when
+others" covers values that don't satisfy the predicate.
+
+I suppose one way to think of it is that values that don't satisfy the predicate
+are like values outside of the base range of the subtype.  Some objects of the
+subtype can have them, and some objects can't, but the rules of the language
+should be set up so that values that don't satisfy the predicate, analogous to
+values outside the base range, don't cause erroneousness.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Tuesday, February 28, 2012  9:06 AM
+
+...
+> I suppose one way to think of it is that values that don't satisfy the
+> predicate are like values outside of the base range of the subtype.
+> Some objects of the subtype can have them, and some objects can't, but
+> the rules of the language should be set up so that values that don't
+> satisfy the predicate, analogous to values outside the base range,
+> don't cause erroneousness.
+
+That seems exactly right, and for a case statement, it means that just as you do
+a range check even if checks are suppressed, you will do a predicate check even
+if checks are suppressed.
+
+Interestingly, gnat has a switch -gnatV that forces extra validity checks around
+the place. I think these should also trigger extra predicate checks for
+predicated subtypes.
+
+****************************************************************
+
+From: Jeff Cousins
+Sent: Tuesday, February 28, 2012  9:42 AM
+
+Have we got a definite answer yet as to whether Steve's example
+
+       subtype Non_Zero is Integer with Static_Predicate
+          => Non_Zero /= 0;
+
+       type Rec (D : Non_Zero) is
+         record
+            case D is
+               when Integer'First .. -1 => ...;
+               when 1 .. Integer'Last => ....;
+            end case;
+         end record;
+
+(i.e. without coverage of the Zero case) is always legal, always illegal, or
+dependent on the Assertion Policy (which is implementation defined if not
+specified)?
+
+I could live with either of the first two as long as it's spelt out which.  I
+think that before the meeting we would have been evenly split about which we
+were expecting.  It seems to have been a mistake to have sold predicates as
+being similar to constraints.
+
+****************************************************************
+
+From: Steve Baird
+Sent: Tuesday, February 28, 2012  10:02 AM
+
+...
+>> I'm wondering about the general issue of how the Ignore assertion
+>> policy interacts with the coverage rules for case-ish constructs
+>> (case statements, case expressions, variant parts) when the nominal
+>> subtype is a static subtype with a Static_Predicate.
+
+> Ignore should only be about removing checks, not altering any of the
+> other semantics of static predicates, it would not be acceptable at
+> all for ignore to make a case statement illegal!
+
+Agreed.
+
+My question was about dynamic semantics only.
+
+...
+> Variant records don't really have
+> such a fall back, but we will have to be clear that even if Ignore
+> applies where the discriminant subtype is specified, the subtype's
+> predicate still determines whether or not a particular
+> discriminant-dependent component exists.  It is as though there were a
+> "when others => null;" alternative in the variant record, where the
+> "when others" covers values that don't satisfy the predicate.
+
+I think this is a bad idea. I think (as in the case of case statements)
+Constraint_Error should be raised. Let's detect a problem like this ASAP instead
+of sweeping it under the rug and then seeing mystifying behavior later.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Tuesday, February 28, 2012  10:19 AM
+
+> Have we got a definite answer yet as to whether Steve's example
+...
+> (i.e. without coverage of the Zero case) is always legal, always illegal, or
+> dependent on the Assertion Policy (which is implementation defined if not
+> specified)?
+
+This is always legal.  Legality should not be affected by the Assertion_Policy.
+I will be writing this up shortly.  For case statements, if the case
+expression's value doesn't satisfy the static predicate, then Constraint_Error
+would be raised, per the existing RM paragram 5.4(13).  For variant records, I
+think we have to assume an implicit "when others => null" meaning that if the
+discriminant does not satisfy the predicate, the implicit "null" variant
+alternative is chosen.
+
+> I could live with either of the first two as long as it's spelt out which.  I
+> think that before the meeting we would have been evenly split about which we
+> were expecting.  It seems to have been a mistake to have sold predicates as
+> being similar to constraints.
+
+Stay tuned for my upcoming write-up.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Sunday, February 26, 2012  5:23 PM
+
+> This is certainly not true for ignoring assertions, ...
+...
+> What about preconditions and postconditions that are suppressed,
+
+Note on terminology: "assertion" is not synonymous with "pragma Assert",
+according to the RM.  The term "assertion" includes pragma Assert, and also
+predicates, pre, post, and invariants.  I believe this agrees with the usage in
+Eiffel.
+
+I think the intent is to treat all assertions, including pre/post, the same way
+with respect to your question.  But it's still somewhat up in the air, and there
+was some talk during the meeting of treating some kinds of assertions
+differently.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Sunday, February 26, 2012  7:01 PM
+
+> Note on terminology: "assertion" is not synonymous with "pragma
+> Assert",
+
+great, another case where the RM invents a term that NO Ada programmer will use.
+I will bet you anything that to virtually 100% of Ada programmers, assertion
+will mean what ever it is that pragma Assert does.
+
+> according to the RM.  The term "assertion" includes pragma Assert, and
+> also predicates, pre, post, and invariants.
+
+Why invent inherently confusing terminology
+
+Come up with a new word. Contracts for example or somesuch.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Tuesday, February 28, 2012  7:02 AM
+
+> > according to the RM.  The term "assertion" includes pragma Assert,
+> > and also predicates, pre, post, and invariants.
+>
+> Why invent inherently confusing terminology
+
+ARG didn't invent this terminology.  It's pretty standard to include
+preconditions and the like in "assertion".
+
+> Come up with a new word. Contracts for example or somesuch.
+
+Ada has too many "new" words as it is.  For example, using "access"
+for what everybody else calls "pointer" or "reference" just causes confusion.
+We should go along with industry-wide terms, to the extent possible.
+
+"Contract" is an informal term, which to me means a whole set of assertions,
+such as all the assertions related to a given abstraction.  Using "contract" to
+refer to a particular assertion would confuse things, I think.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Tuesday, February 28, 2012  7:18 AM
+
+> ARG didn't invent this terminology.  It's pretty standard to include
+> preconditions and the like in "assertion".
+
+By the way, you snipped my reference to Eiffel, which agrees that "assertion"
+includes preconditions and the like. Eiffel should be respected when talking
+about contracts.
+
+If you still don't believe me, google "assertion programming language".
+(Note that the 10'th hit is an AdaCore web page that correctly includes pre,
+etc.)
+
+In languages that only have assert statements (C and pre-2012 Ada[1], for
+example), that's all you have.  But in languages that have preconditions and
+invariants[2], those are included.
+
+[1] Yeah, I know it's a macro in C, and a pragma in Ada, but conceptually, it's
+    a statement.
+
+[2] Called "predicates" in Ada.  ;-)
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Tuesday, February 28, 2012  7:25 AM
+
+>> Why invent inherently confusing terminology
+>
+> ARG didn't invent this terminology.  It's pretty standard to include
+> preconditions and the like in "assertion".
+
+I mean it's confusing in the Ada context. It is always a mistake to push
+terminology that no one will use (e.g.
+
+    a generic package is not a package
+    a package spec is not what you think it is
+    a type should be called a subtype
+    a class type has to be called a tagged type
+
+    and yes, I would add access/pointer to that list.
+    etc.)
+
+I am willing to bet that for nearly all Ada programmers Assertion will continue
+to refer to things done by pragma Assert, as it always have. And I often see ARG
+members using this terminology, e.g. something like
+
+"Well a precondition in a subprogram body is really just an assertion."
+
+which is official nonsense, but everyone understands it!
+
+>> Come up with a new word. Contracts for example or somesuch.
+>
+> Ada has too many "new" words as it is.  For example, using "access"
+> for what everybody else calls "pointer" or "reference" just causes
+> confusion.  We should go along with industry-wide terms, to the extent
+> possible.
+>
+> "Contract" is an informal term, which to me means a whole set of
+> assertions, such as all the assertions related to a given abstraction.
+> Using "contract" to refer to a particular assertion would confuse
+> things, I think.
+
+Contract items?
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Tuesday, February 28, 2012  7:30 AM
+
+...
+> By the way, you snipped my reference to Eiffel, which agrees that
+> "assertion" includes preconditions and the like.
+> Eiffel should be respected when talking about contracts.
+
+does Eiffel have assertions in the Ada 2005 sense?
+
+The trouble here is that it is so natural to assume that assertion refers to
+pragma assert because
+
+a) it has always done so in Ada
+b) the name just encourages this identification
+
+That's why I think Ada programmers will continue to use the term assertion to
+mean that which is specified with pragma Assert, and it is futile for the ARG to
+try to push terminology that won't stick.
+
+More Ada 2012 programmers will know previous versions of Ada than Eiffel!!
+
+****************************************************************
+
+From: Bob Duff
+Sent: Tuesday, February 28, 2012  7:45 AM
+
+> does Eiffel have assertions in the Ada 2005 sense?
+
+Yes, but I think it's called "check", so the potential confusion you're worried
+about ("assertion" /= "assert") doesn't arise.
+
+By the way, I don't deny that there's a potential confusion.
+I usually get around it by saying something like "assertions, such as
+preconditions and the like...".
+
+In general, programming language terminology is a mess!
+"Procedure", "function", "method", "subroutine", "routine", "subprogram" -- all
+mean basically the same thing. It really damages communication among people with
+different backgrounds.
+
+Note that the RM often uses the term "remote procedure call" and its
+abbreviation "RPC", even though it could be calling a function.  It doesn't make
+perfect sense, but RPC is so common in the non-Ada world, we decided to use it.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Tuesday, February 28, 2012  7:53 AM
+
+>> does Eiffel have assertions in the Ada 2005 sense?
+>
+> Yes, but I think it's called "check", so the potential confusion
+> you're worried about ("assertion" /= "assert") doesn't arise.
+
+Right, thats what I remembered (no assertions as such).
+
+> By the way, I don't deny that there's a potential confusion.
+> I usually get around it by saying something like "assertions, such as
+> preconditions and the like...".
+
+Yes, but you can't expect people to do that all the time.
+I suppose we should get in the habit of using "asserts"
+to refer to the set of things done with pragma assert.
+(like preconditions).
+
+****************************************************************
+
+From: Jean-Pierre Rosen
+Sent: Tuesday, February 28, 2012  8:04 AM
+
+>> "Contract" is an informal term, which to me means a whole set of
+>> assertions, such as all the assertions related to a given
+>> abstraction.  Using "contract" to refer to a particular assertion
+>> would confuse things, I think.
+>
+> Contract items?
+
+I'd rather avoid "contract", because we often refer to generic formals as a
+contract, we talk about the contract model for assume the best/assume the worst,
+etc.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Tuesday, February 28, 2012  8:08 AM
+
+yes, good point
+
+****************************************************************
+
+From: Erhard Ploedereder
+Sent: Tuesday, February 28, 2012  10:01 AM
+
+> That's why I think Ada programmers will continue to use the term
+> assertion to mean that which is specified with pragma Assert, and it
+> is futile for the ARG to try to push terminology that won't stick.
+
+So what is your proposal? We need some word or words to describe the group of
+pragma Assert, prcondition, postcondition, type invariant, and maybe subtype
+predicate. Repeating them all every time something is said about all of them is
+editorial suicide. "Contract" isn't it, since Assert(ions) have no contract
+idea.
+
+(By the way, I don't believe that Ada programmers will be so literal in their
+interpretations that they believe that only pragma Assert can create
+assertions.)
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Tuesday, February 28, 2012  10:14 AM
+
+>> That's why I think Ada programmers will continue to use the term
+>> assertion to mean that which is specified with pragma Assert, and it
+>> is futile for the ARG to try to push terminology that won't stick.
+>
+> So what is your proposal? We need some word or words to describe the
+> group of pragma Assert, prcondition, postcondition, type invariant,
+> and maybe subtype predicate. Repeating them all every time something
+> is said about all of them is editorial suicide.
+> "Contract" isn't it, since Assert(ions) have no contract idea.
+
+At this point I think we need to stick with "assertion expressions"
+given that we are using "Assertion_Policy" to control them all, and they all
+raise Assertion_Error on failure.
+
+****************************************************************
+
+From: Jean-Pierre Rosen
+Sent: Tuesday, February 28, 2012  10:19 AM
+
+> So what is your proposal?
+
+Assumptions?
+
+Checks? (I think it's too vague)
+
+****************************************************************
+
+From: Ben Brosgol
+Sent: Tuesday, February 28, 2012  10:37 AM
+
+...
+> At this point I think we need to stick with "assertion expressions"
+> given that we are using "Assertion_Policy" to control them all, and
+> they all raise Assertion_Error on failure.
+
+Maybe "assertion forms"?
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Tuesday, February 28, 2012  2:38 PM
+
+> (By the way, I don't believe that Ada programmers will be so literal
+> in their interpretations that they believe that only pragma Assert can
+> create assertions.)
+
+The reason I think this is that this has been the case for years.
+
+****************************************************************
+
+From: Erhard Ploedereder
+Sent: Wednesday, February 29, 2012  7:21 AM
+
+> Assumptions?
+
+Has exactly the opposite meaning in verification land, i.e. something that you
+can always assume on faith.
+
+> Checks? (I think it's too vague)
+
+Already taken by the run-time checks and, as an axiom, not to be confused with
+"the new stuff".
+
+and from Ben B.:
+> assertion forms
+
+Does not solve Robert's concern that the term is completely occupied by pragma
+Assert.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Tuesday, February 28, 2012  2:37 PM
+
+> I could live with either of the first two as long as it's spelt out
+> which.  I think that before the meeting we would have been evenly
+> split about which we were expecting.  It seems to have been a mistake
+> to have sold predicates as being similar to constraints.
+
+To me, if predicates are not similar to constraints they are broken.
+The following two should be very similar in effect
+
+    subtype R is integer range 1 .. 10;
+
+    subtype R is integer with
+      Static_Predicate => R in 1 .. 10;
+
+****************************************************************
+
+From: Ed Schonberg
+Sent: Tuesday, February 28, 2012  2:45 PM
+
+At the meeting there was an agreement in that direction (not unanimous of
+course, nothing is).  This is why Assertion_Policy has to have a different
+effect on pre/postconditions than on predicate checks. Creating values that
+violate the predicate is as bad as creating out-of- range values.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Tuesday, February 28, 2012  2:53 PM
+
+The reason I think those two cases have to be very similar (I never like to use
+the word equivalent :-)) is that I think in practice any Ada programmer would
+expect them to be similar, they sure *look* similar :-)
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Tuesday, February 28, 2012  3:01 PM
+
+They are very similar.  The one significant difference is that the first one if
+you suppress the range check, your program can go erroneous if you violate the
+constraint.  In the second one, if you set Assertion_Policy(Ignore) then some
+checks will be eliminated, but there will be no assumption that the checks would
+have passed if they had been performed.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Tuesday, February 28, 2012  3:24 PM
+
+> They are very similar.  The one significant difference is that the
+> first one if you suppress the range check, your program can go
+> erroneous if you violate the constraint.
+
+Not easily though, since generally e.g. uninitialized values don't drive you
+into erroneousness.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Tuesday, February 28, 2012  3:39 PM
+
+> They are very similar.
+
+Agreed.  If you don't turn off the checks, the only difference is which
+exception gets raised.  That counts as "very similar" in my book, especially if
+you're not going to handle these exceptions (which I expect is the usual case).
+
+If you DO turn off the checks, then you should have made sure by other means
+that the checks won't fail, so they're still quite similar.  Of course, you
+might make a mistake, and the consequences of that mistake might be different,
+but the rule for programmers is simple: Don't do that. That is, don't violate
+constraints, and don't violate predicates, and especially don't turn the checks
+off without good reason.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Tuesday, February 28, 2012  3:43 PM
+
+> and especially don't turn the checks off without good reason.
+
+Exactly, and deliberately wanting to violate the check without an exception is
+NOT a good reason :-)
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Tuesday, February 28, 2012  5:07 PM
+
+Here is the "final" version, incorporating the newer ideas about how
+Assertion_Policy should apply to subtype predicate checks, and using the term
+"enabled" more uniformly.
+[Editor's note: This is version /05.]
+
+****************************************************************
+
+From: Steve Baird
+Sent: Tuesday, February 28, 2012  6:42 PM
+
+> Here is the "final" version, ..
+
+That's optimistic.
+
+Some questions and observations:
+
+1) In general, I like the approach for defining how
+    assertion policies interact with subtype predicates.
+
+    What about cases where a subtype name is repeated with a
+    conformance check?
+
+    For example
+         pragma Assertion_Policy (Static_Predicate => Check);
+
+         subtype Foo is Integer with Static_Predicate => Foo /= 123;
+
+         package Pkg is
+           type T (D : Foo) is private;
+
+           pragma Assertion_Policy (Static_Predicate => Ignore);
+         private
+           type T (D : Foo) is ....
+         end Pkg;
+
+     For a subtype that has a specified predicate aspect
+     (either static or dynamic), perhaps we want the
+     assertion policy corresponding to that aspect to
+     participate in subtype conformance. In the above example,
+     the two uses of Foo would fail the subtype conformance
+     legality check even though they denote the same subtype.
+
+     Or perhaps we punt and just say that this case is implementation
+     dependent.
+
+     Similar issues occur for subprogram declarations (spec, stub,
+     and body), and deferred constants.
+
+2) What about conformance for 'Access attributes and related checking?
+
+     We have an access-to-foo type with one assertion policy and an
+     aliased object of type foo declared with a different assertion
+     policy in effect. Do we want to allow the Access attribute of
+     the object to yield a value of the access type?
+
+      Or two access types which would otherwise be convertible but they
+      differ with respect to applicable assertion policy. Do we want
+      to allow conversion between such access types?
+
+     Maybe allowing these things is ok, but it makes it very hard
+     to write assertions that you can count on.
+
+     The same problems occur for access-to-subprogram types.
+
+     Would we want this stricter conformance rule only if the subtype in
+     question is affected by the assertion policy? Should two uses
+     of Standard,Integer fail a conformance check because of a difference
+     in assertion policy? What about the case where we don't know
+     (e.g., an access type declaration where the designated type is
+      incomplete) or where getting this knowledge requires breaking
+      privacy?
+
+      What about overriding primitive subprograms of tagged types?
+      Is it ok if overrider and overridden differ with respect to
+      assertion policy?
+
+3) For a call with a defaulted expression which includes a
+    qualified expression, which assertion policy determines what
+    predicate checking is performed for the qualified expression?
+
+4) I think the rules for dealing with assertion policies and generics
+    are fine, but I'd still like to see an AARM note stating explicitly
+    that an assertion_policy pragma (and, for that matter, a suppress
+    pragma) which applies to a region which includes the declaration or
+    body of a generic has no effect on an instance of that
+    generic (assuming the  instance is declared outside of the region
+    affected by the pragma).
+
+    I think the consequences of the rule
+
+      If a pragma Assertion_Policy applies to a generic_instantiation,
+      then the pragma Assertion_Policy applies to the entire instance.
+
+    are a bit less obvious than some other rules and an AARM note is
+    justified.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Tuesday, February 28, 2012  8:19 PM
+
+...
+> For a subtype that has a specified predicate aspect (either static or
+> dynamic), perhaps we want the assertion policy corresponding to that
+> aspect to participate in subtype conformance. In the above example,
+> the two uses of Foo would fail the subtype conformance legality check
+> even though they denote the same subtype.
+>
+> Or perhaps we punt and just say that this case is implementation
+> dependent.
+>
+> Similar issues occur for subprogram declarations (spec, stub, and
+> body), and deferred constants.
+
+I think the initial declaration should determine whether the check is enabled.
+The state of the assertion policy at the point of the completion should not be
+relevant.
+
+> 2) What about conformance for 'Access attributes and related checking?
+
+Yuck.  First we should be sure we agree on the rules without worrying about
+Assertion_Policy.  We already decided that "static subtype matching" requires
+that predicates come from the same declaration (in 4.9.1(2/3)).  So that seems
+pretty clear.
+
+We had hoped that legality didn't depend on Assertion_Policy, but I guess I
+would be inclined to say that conflicting Assertion_Policies should cause errors
+when using 'Access.
+
+> We have an access-to-foo type with one assertion policy and an aliased
+> object of type foo declared with a different assertion policy in
+> effect. Do we want to allow the Access attribute of the object to
+> yield a value of the access type?
+>
+> Or two access types which would otherwise be convertible but they
+> differ with respect to applicable assertion policy. Do we want to
+> allow conversion between such access types?
+>
+> Maybe allowing these things is ok, but it makes it very hard to write
+> assertions that you can count on.
+>
+> The same problems occur for access-to-subprogram types.
+
+I would go with it being illegal if the predicate-check policies conflict and
+there are any subtypes with non-trivial predicates.
+
+Alternatively, for access-to-subprogram, we could try to generalize the
+assertion-policy rules for preconditions and postconditions (whatever those are)
+for calling through an access-to-subprogram.
+
+> Would we want this stricter conformance rule only if the subtype in
+> question is affected by the assertion policy?
+
+I would hope so.  That is, if the predicate is True, then conflicting assertion
+policies are not a problem.  It is only if the predicate is not True that the
+policies need to agree between the aliased object and the designated subtype of
+the access type.  Or equivalently between the designated profile and the
+subprogram that is the prefix to the 'Access.
+
+> ... Should two uses
+> of Standard,Integer fail a conformance check because of a difference
+> in assertion policy? What about the case where we don't know (e.g., an
+> access type declaration where the designated type is
+> incomplete) or where getting this knowledge requires breaking privacy?
+
+I would need to see some examples there.  I can't quite imagine how that would
+happen.
+
+> What about overriding primitive subprograms of tagged types?
+> Is it ok if overrider and overridden differ with respect to assertion
+> policy?
+
+Here I think in the same way that an overriding subprogram inherits the
+convention of the inherited subprogram, the overriding subprogram should
+probably inherit the predicate-check assertion policy state.  It is not clear
+how else it could work.
+
+> 3) For a call with a defaulted expression which includes a qualified
+> expression, which assertion policy determines what predicate checking
+> is performed for the qualified expression?
+
+I think the place where the default expression appears.
+
+> 4) I think the rules for dealing with assertion policies and generics
+> are fine, but I'd still like to see an AARM note stating explicitly
+> that an assertion_policy pragma (and, for that matter, a suppress
+> pragma) which applies to a region which includes the declaration or
+> body of a generic has no effect on an instance of that generic
+> (assuming the instance is declared outside of the region affected by
+> the pragma).
+>
+> I think the consequences of the rule
+>
+> If a pragma Assertion_Policy applies to a generic_instantiation, then
+> the pragma Assertion_Policy applies to the entire instance.
+>
+> are a bit less obvious than some other rules and an AARM note is
+> justified.
+
+Agreed.
+
+****************************************************************
+
+From: Steve Baird
+Sent: Wednesday, February 29, 2012  11:35 AM
+
+> I think the initial declaration should determine whether the check is
+> enabled.  The state of the assertion policy at the point of the
+> completion should not be relevant.
+
+That seems like a good principle.
+
+>> 2) What about conformance for 'Access attributes and related checking?
+>
+> We had hoped that legality didn't depend on Assertion_Policy, but I
+> guess I would be inclined to say that conflicting Assertion_Policies
+> should cause errors when using 'Access.
+
+Right. It is as if the same identifier can be used to denote two different
+subtypes, one with predicate checking and one not.
+
+I think we *could* allow those two subtypes to conform (i.e., it wouldn't
+compromise type-safety), but I agree with you that we probably don't want to.
+
+>> Would we want this stricter conformance rule only if the subtype in
+>> question is affected by the assertion policy?
+>
+> I would hope so.
+
+Me too, but I think we have to deal with the "maybe" case discussed below.
+
+>> ... Should two uses
+>> of Standard.Integer fail a conformance check because of a difference
+>> in assertion policy? What about the case where we don't know (e.g.,
+>> an access type declaration where the designated type is
+>> incomplete) or where getting this knowledge requires breaking
+>> privacy?
+>
+> I would need to see some examples there.  I can't quite imagine how
+> that would happen.
+
+For example, an access type where the designated type is incomplete (perhaps a
+Taft type or a type from a limited view).
+
+     pragma Asserion_Policy (Check);
+
+     procedure P (X : access Some_Incomplete_Type);
+
+     package Nested is
+        pragma Assertion_Policy (Ignore);
+
+        type Ref is access procedure (Xx : access Some_Incomplete_Type);
+
+        Ptr : Ref := P'Access; -- legal?
+
+Or, if we are concerned about privacy here (and perhaps we aren't; we could view
+assertion_policy stuff as being like repspec stuff, but it would be nicer if we
+didn't have to do that):
+
+      package Pkg is
+          type Has_A_Predicate is private;
+          type Has_no_Predicate is private;
+      private
+           type Has_A_Predicate is new Integer
+             with Static_Predicate => Has_A_Predicate /= 123;
+
+           type Has_No_Predicate is new Integer;
+      end Pkg;
+
+
+      pragma Assertion_Policy (Check);
+      use Pkg;
+      Has : aliased Has_A_Predicate;
+      Has_No : aliased Has_No_Predicate;
+
+      package Nested is
+         pragma Assert_Policy (Ignore);
+         type Has_Ref is access Has_A_Predicate;
+         type Has_No_Ref is access Has_No_Predicate;
+
+         Ptr1 : Has_Ref := Has'Access; -- we want this to be illegal ...
+         Ptr2 : Has_No_Ref := Has_No'Access; -- but what about this?
+
+
+>> What about overriding primitive subprograms of tagged types?
+>> Is it ok if overrider and overridden differ with respect to assertion
+>> policy?
+>
+> Here I think in the same way that an overriding subprogram inherits
+> the convention of the inherited subprogram, the overriding subprogram
+> should probably inherit the predicate-check assertion policy state.
+> It is not clear how else it could work.
+
+And if interface types are involved and one subprogram overrides more than one
+inherited subp and the inherited guys don't all agree? I think there are also
+much more obscure cases not involving interface types where one primitive op can
+override two, but I would have to check to be sure.
+
+>> 3) For a call with a defaulted expression which includes a qualified
+>> expression, which assertion policy determines what predicate checking
+>> is performed for the qualified expression?
+>
+> I think the place where the default expression appears.
+
+Sounds good. Ditto for all the other forms of default expressions, presumably.
+
+>> Variant records don't really have
+>> such a fall back, but we will have to be clear that even if Ignore
+>> applies where the discriminant subtype is specified, the subtype's
+>> predicate still determines whether or not a particular
+>> discriminant-dependent component exists.  It is as though there were
+>> a "when others => null;" alternative in the variant record, where the
+>> "when others" covers values that don't satisfy the predicate.
+>
+> I think this is a bad idea. I think (as in the case of case
+> statements) Constraint_Error should be raised. Let's detect a problem
+> like this ASAP instead of sweeping it under the rug and then seeing
+> mystifying behavior later.
+
+Did my "let's treat all case-ish constructs uniformly"
+argument change your mind?
+
+****************************************************************
+
+From: Steve Baird
+Sent: Wednesday, February 29, 2012  12:05 PM
+
+>> Here I think in the same way that an overriding subprogram inherits
+>> the convention of the inherited subprogram, the overriding subprogram
+>> should probably inherit the predicate-check assertion policy state.
+>> It is not clear how else it could work.
+>>
+>
+> And if interface types are involved ....
+
+Never mind. I see that 3.9.2(10/2) already has
+
+   .... if the operation overrides multiple inherited operations, then
+   they shall all have the same convention.
+
+So your proposal already covers this case.
+
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Wednesday, February 29, 2012  12:17 PM
+
+> ... Or, if we are concerned about privacy here (and perhaps we aren't;
+> we could view assertion_policy stuff as being like repspec stuff, but
+> it would be nicer if we didn't have to do that):
+
+I think conflicting assertion policies is like conflicting rep-clauses.  It has
+to see through privacy.  When a programmer starts applying micro-control with
+the assertion policy, they are now talking about the concrete representations of
+things, not just their abstract interfaces.
+
+...
+>> I think this is a bad idea. I think (as in the case of case
+>> statements) Constraint_Error should be raised. Let's detect a problem
+>> like this ASAP instead of sweeping it under the rug and then seeing
+>> mystifying behavior later.
+>
+> Did my "let's treat all case-ish constructs uniformly"
+> argument change your mind?
+
+Not sure, though probably some realistic examples might help decide.  Since
+discriminants cannot be changed after an object is created, except by
+whole-record assignment, the question is whether we check to be sure the
+discriminant is covered by the variant alternatives on object creation or on
+component selection, I suppose. Doing it on object creation is perhaps simpler,
+so I guess making an unconditional check (even if predicate checks are disabled)
+to be sure that some variant alternative covers the discriminant value seems
+reasonable. If there is a "when others" then there won't be any check anyway, so
+it would only be if the variant part did *not* have a "when others" and relied
+on full coverage of exactly those elements that satisfied the static predicate.
+
+So I guess I can go with your suggestion.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Friday, March 2, 2012  1:44 PM
+
+Steve,
+    Would you be willing to do the next "rev" on this AI?
+
+****************************************************************
+
+From: Steve Baird
+Sent: Friday, March 2, 2012  2:20 PM
+
+Sure, but only after I know what ideas we want to express.
+
+In particular, I'm wondering about the interactions with "statically matching" and incomplete types that I mentioned earlier.
+
+I'd like to avoid cases where we conservatively disallow some construct (e.g.,
+an access type conversion) because of assertion policy differences when it turns
+out that there are no predicate specifications anywhere in the neighborhood.
+Maybe we want to be more permissive and assume when dealing with an incomplete
+view of a type that the full type has no applicable predicate specifications?
+That would make predicates for designated subtypes less trustworthy, but I think
+users would be unlikely to accidentally violate a predicate via this mechanism.
+Whether it would be used deliberately (the old "designated predicate bypass
+trick") is a separate question.
+
+It would be more of a problem that tools, developers, maintainers, etc. would
+have to deal with the possibility that someone *might* use this trick, even
+nobody ever does.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Friday, March 2, 2012  2:31 PM
+
+We could disallow predicates on the first subtype of a type that is a deferred
+incomplete type.  Putting predicates on a first subtype seems pretty weird
+anyway.  The purpose of a predicate is normally to define an interesting subset,
+not to specify something that is true for all values of the type (that would be
+more appropriate for a type invariant).
+
+****************************************************************
+
+From: Bob Duff
+Sent: Friday, March 2, 2012  2:43 PM
+
+> I'd like to avoid cases where we conservatively disallow some
+> construct (e.g., an access type conversion) because of assertion
+> policy differences when it turns out that there are no predicate
+> specifications anywhere in the neighborhood.
+
+Well, I don't think we want any incompatibilities.
+
+I haven't followed much of this discussion, but if you're suggesting that pragma
+Assertion_Policy would affect the legality of a program, I look askance.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Friday, March 2, 2012  2:43 PM
+
+> We could disallow predicates on the first subtype of a type that is a
+> deferred incomplete type.  Putting predicates on a first subtype seems
+> pretty weird anyway.  The purpose of a predicate is normally to define
+> an interesting subset, not to specify something that is true for all
+> values of the type (that would be more appropriate for a type
+> invariant).
+
+I disagree, it's not weird to have a range on a first subtype
+
+    type R is new integer range 1 .. 10;
+
+so why should it be weird to have a prediate on a first subtype
+
+    type Non_Zero is new Integer with
+      Predicate => Non_Zero /= 0;
+
+to me predicates and constraints are really pretty much the same beast, it is
+just that predicates have more power. In fact it seems a bit odd to me to have
+constraints at all, given a more powerful mechanism that emcompasses ranges, but
+of course I understand the historical reasoning.
+
+On the other hand to me deferred incomplete types are a bit weird anyway, so I
+really don't mind restrictions on them.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Friday, March 2, 2012  2:52 PM
+
+>> We could disallow predicates on the first subtype of a type that is a
+>> deferred incomplete type. Putting predicates on a first subtype seems
+>> pretty weird anyway. The purpose of a predicate is normally to define
+>> an interesting subset, not to specify something that is true for all
+>> values of the type (that would be more appropriate for a type
+>> invariant).
+>
+> I disagree, it's not weird to have a range on a first subtype
+
+You are right, if the first subtype is derived from some preexisting type.  But
+I believe it would be weird to put a predicate on the first subtype of a
+non-private, non-numeric, non-derived type. And if the type is private, a type
+invariant is more appropriate.
+
+If the type is numeric or derived, then I can see the use of the predicate on
+the first subtype, since you can convert to an un-predicated version using 'Base
+if numeric, or by explicit conversion to the parent type if derived.
+
+In any case, it sounds like we agree that imposing restrictions on the use of
+predicates with deferred incomplete types would be OK.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Friday, March 2, 2012  2:54 PM
+
+> We could disallow predicates on the first subtype of a type that is a
+> deferred incomplete type.  Putting predicates on a first subtype seems
+> pretty weird anyway.
+
+I don't agree.  I think it makes perfect sense to say:
+
+    type Nonzero is new Integer with Static_Predicate => Nonzero /= 0;
+
+>...The purpose
+> of a predicate is normally to define an interesting subset,  not to
+>specify something that is true for all values of the  type...
+
+Agreed, specifying a predicate on a scalar first subtype does not say anything
+about all values of the type, because 'Base takes away the predicate, as well as
+the constraint:
+
+    X: Nonzero'Base := 0; -- no exception
+
+    type Color is (Red, Yellow, Green, None)
+        with Static_Predicate => Color /= None;
+
+    subtype Optional_Color is Color'Base; -- allows None
+
+For composites, there's no 'Base, so it applies to all objects of the type
+(modulo some loopholes):
+
+    type My_String is array (Positive range <>) of Character
+        with Dynamic_Predicate => My_String'First = 1;
+
+Perhaps we should allow 'Base on composites in Ada 2020.
+
+>... (that would be more appropriate for a type invariant).
+
+Well, type invariants only work for private-ish types.
+
+****************************************************************
+
+From: Steve Baird
+Sent: Friday, March 2, 2012  3:15 PM
+
+> We could disallow predicates on the first subtype of a type that is a
+> deferred incomplete type.
+
+This might be ok for explicit incomplete type declarations.
+
+How does this work with limited withs?
+
+Any type declaration that can be seen via a limited with has an incomplete view.
+Fortunately, limited withs don't make subtype declarations visible, so we are
+only concerned with first subtypes.
+
+> Putting predicates on
+> a first subtype seems pretty weird anyway.  The purpose of a predicate
+> is normally to define an interesting subset, not to specify something
+> that is true for all values of the type (that would be more
+> appropriate for a type invariant).
+>
+
+I disagree in the case of a derived type (upon reading Robert's message halfway
+through composing this one, I see that he made this point too and you now
+agree).
+
+Even in the case of a non-derived type, I could imagine wanting something like
+
+     type Foo (Max_Length : Natural) is
+       record
+         Data : Buffer(1 .. Max_Length);
+         Current_Length : Natural := 0;
+       end record
+       with Dynamic_Predicate Foo.Current_Length < Foo.Max_Length;
+
+and I wouldn't want to ban this in order to support mixing of assertion
+policies.
+
+Another ugly option would be to have a configuration pragma (one which has to be
+consistent across the entire partition) for specifying the assertion policy
+associated with the designated subtype of an access type when the view of that
+subtype is incomplete at the point of the access type definition. Just a
+thought. I haven't thought about DSA interactions at all - maybe there aren't
+any.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Friday, March 2, 2012  3:30 PM
+
+>      X: Nonzero'Base := 0; -- no exception
+>
+>      type Color is (Red, Yellow, Green, None)
+>          with Static_Predicate =>  Color /= None;
+>
+>      subtype Optional_Color is Color'Base; -- allows None
+>
+> For composites, there's no 'Base, so it applies to all objects of the
+> type (modulo some loopholes):
+
+Sure, but 'Base for integer types is an odd beast anyway, I virtually never saw
+it in user code.
+
+And this is really no different from
+
+   type R is range 1 .. 10;
+
+   R'Base
+   range disappeared
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Friday, March 2, 2012  4:52 PM
+
+>> We could disallow predicates on the first subtype of a type that is a
+>> deferred incomplete type.
+>
+> This might be ok for explicit incomplete type declarations.
+>
+> How does this work with limited withs?
+
+I don't see a problem with limited withs.
+Can you construct an example which has such a problem.
+
+> Any type declaration that can be seen via a limited with has an
+> incomplete view. Fortunately, limited withs don't make subtype
+> declarations visible, so we are only concerned with first subtypes.
+> ...
+
+I don't think we need to restrict predicates on types declared in the visible
+part of a package just because they might be referenced in a limited with.  I
+couldn't, but perhaps you can construct a problem that involves such a type...
+
+****************************************************************
+
+From: Steve Baird
+Sent: Friday, March 2, 2012  5:09 PM
+
+> I don't see a problem with limited withs.
+> Can you construct an example which has such a problem.
+
+I haven't tried to compile this, but this should be close.
+
+    package Pkg1 is
+      type Even is new Integer with
+        Dynamic_Predicate => Even mod 2 = 0;
+    end Pkg1;
+
+    limited with Pkg1;
+    package Checker is
+       pragma Assertion_Policy (Check);
+       type Safe_Ref is access all Pkg1.Even;
+       Safe_Ptr . Safe_Ref;
+    end Checker;
+
+    limited with Pkg1;
+    package Ignorer is
+       pragma Assertion_Policy (Ignore);
+       type Unsafe_Ref is access all Pkg1.Even;
+       Unsafe_Ptr . Unsafe_Ref := new Even'(3);
+         -- violates predicate, but that's ok
+    end Ignorer;
+
+    with Checker, Ignorer;
+    use Checker, Ignorer;
+    procedure Converter is
+        Safe_Ptr_Has_Been_Corrupted;
+    begin
+        Safe_Ptr := Safe_Ref (Unsafe_Ptr);
+        if Safe_Ptr.all not in Even then
+           raise Safe_Ptr_Has_Been_Corrupted;
+        end if;
+    end Converter;
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Friday, March 2, 2012  5:19 PM
+
+>> I don't see a problem with limited withs.
+>> Can you construct an example which has such a problem.
+>
+> I haven't tried to compile this, but this should be close.
+
+I don't see a problem here, since the compiler can certainly see that there is a
+predicate on the type "Pkg1.Even", even if it is using a limited "with" and the
+type is officially incomplete.
+
+But I suppose it would be a bigger problem if Even were defined as derived from
+some other type declared in a different package, and "Even" didn't have a
+predicate itself but it inherited one.  We could keep following the chain of
+"with" clauses I suppose just to learn whether the subtypes have predicates, but
+once you start doing name resolution you are starting to violate the spirit of
+"limited" with.
+
+At this point it looks simpler to disallow the conversion if different assertion
+policies apply to the two designated subtypes, even if we don't know for sure
+whether there is a predicate.
+
+****************************************************************
+
+From: Steve Baird
+Sent: Friday, March 2, 2012  5:24 PM
+
+> But I suppose it would be a bigger problem if Even were defined as
+> derived from some other type declared in a different package, and
+> "Even" didn't have a predicate itself but it inherited one.  We could
+> keep following the chain of "with" clauses I suppose just to learn
+> whether the subtypes have predicates, but once you start doing name
+> resolution you are starting to violate the spirit of "limited" with.
+
+There would be bigtime implementation problems if we ever introduced a language
+rule that required resolution of a name which occurs in a limited view of a
+package.
+
+The implementation model is that an implementation should be able to compile a
+limited wither after only parsing the limited withee.
 
 ****************************************************************

Questions? Ask the ACAA Technical Agent