CVS difference for ai05s/ai05-0146-1.txt
--- ai05s/ai05-0146-1.txt 2009/11/03 06:03:06 1.5
+++ ai05s/ai05-0146-1.txt 2010/06/11 03:29:51 1.6
@@ -1,11 +1,11 @@
-!standard 11.5 (00) 09-11-02 AI05-0146-1/03
+!standard 11.5 (00) 10-06-06 AI05-0146-1/04
!standard 11.4.1 (10)
!class amendment 09-02-15
!status work item 09-02-15
!status received 09-02-15
!priority Medium
!difficulty Medium
-!subject Type and Package Invariants
+!subject Type Invariants
!summary
@@ -77,18 +77,6 @@
!wording
-Modify 7.3(2 and 3/2):
-
- private_type_declaration ::=
- type defining_identifier [discriminant_part] is [[abstract] tagged] [limited] private
- [aspect_specification];
-
- private_extension_declaration ::=
- type defining_identifier [discriminant_part] is
- [abstract] [limited | synchronized] new ancestor_subtype_indication
- [and interface_list] with private
- [aspect_specification];
-
Add new section:
13.3.3 Type Invariants
@@ -97,9 +85,9 @@
using an aspect_specification for the aspect Invariant and, if tagged,
for the aspect Invariant'Class. The associated expression is called
an *invariant expression*.
-
+
Name Resolution
-
+
The expected type for an invariant expression is the predefined type
Boolean. [Redundant: Within an invariant expression, the identifier of
the first subtype of the associated type denotes the current instance
@@ -108,38 +96,37 @@
T'Class for the Invariant'Class aspect.
Legality Rules
-
+
[Redundant: The Invariant'Class aspect shall not be specified for an
untagged type.] The Invariant aspect shall not be specified for an
abstract type.
-
+
Static Semantics
-
+
[Redundant: If the Invariant'Class aspect is specified for a tagged type T,
then the invariant expression applies to all descendants of T.]
-
+
Dynamic Semantics
-
+
If one or more invariant expressions apply to a type T, and the Assertion_Policy
at the point of the partial view declaration for T is Check, then an
invariant check is performed at the following places, on the specified object(s):
* After default initialization of an object of type T, on the new object;
-
+
* After conversion to type T, on the result of the conversion;
-
- * Upon return from a call on any subprogram or entry that:
-
- - has a result of type T, or one or more IN OUT or OUT
+
+ * Upon return from a call on any subprogram or entry that:
+ - has a result of type T, or one or more IN OUT or OUT
parameters of type T,
- - is explicitly declared within the immediate scope of type T, and
- - is visible outside the immediate scope of type T, overrides
+ - is explicitly declared within the immediate scope of type T
+ (or is a part of an instance of a generic unit declared within
+ the immediate scope of type T), and
+ - is visible outside the immediate scope of type T or overrides
an operation that is visible outside the immediate scope of T,
- or has its Access attribute evaluated;
-
- on the result object of type T, and on each IN OUT or OUT
+ on the result object of type T, and on each IN OUT or OUT
actual parameter of type T.
-
+
The invariant check consists of the evaluation of each invariant
expression that applies to T, on each of the objects specified above.
If any of these evaluate to False, Ada.Assertions.Assertion_Error is
@@ -154,15 +141,30 @@
or OUT parameters are performed before or after any invariant checks.
It is not specified whether any postcondition checks are performed
before or after any invariant checks.
-
+
The invariant checks performed on a call are determined by the subprogram
or entry actually invoked, whether directly, as part of a dispatching call, or
as part of a call through an access-to-subprogram value.
-
+
[Redundant: If the Assertion_Policy in effect at the point of a
subprogram or entry declaration is Ignore, then no invariant check is
performed on a call on that subprogram or entry.]
+ AARM Note: Invariant checks on subprogram return are not performed on
+ objects that are accessible only through access values. It is also
+ possible to call through an access-to-subprogram value and reach a
+ subprogram body that has visibility on the full declaration
+ of a type, from outside the immediate scope of the type. No invariant
+ checks will be performed if the designated subprogram is not itself
+ externally visible. These cases represent "holes" in the protection
+ provided by invariant checks.
+
+ AARM Implementation Note: The implementation might want to produce a warning
+ if a private extension has an ancestor type that is a visible extension,
+ and an invariant expression depends on the value of one of the components from
+ a visible extension part.
+
+
!discussion
We have provided only type oriented "invariant"
@@ -178,7 +180,7 @@
to the "current instance," which is the value being checked against the
invariant. We considered allowing only the name of a boolean function,
but the more general boolean_expression was felt to be useful at least
-in same cases.
+in same cases.
For type invariants, name resolution on the boolean expression is not
performed until reaching the end of the visible part of the enclosing
@@ -203,9 +205,13 @@
We have adopted a rule that the invariant checks performed are determined
by the subprogram invoked, whether directly or indirectly, to match
-the rule for pre- and postconditions. Note that we assume that any
-subprogram that has its Access attribute evaluated might be called from
-outside the package.
+the rule for pre- and postconditions.
+
+Note that we do not worry about subprograms that have their Access attribute
+evaluated, even though they might be called from outside the package.
+We recognize there are holes in the protection provided by type invariants,
+so we don't require herculean efforts to catch all possible ways a value
+might be updated and then become externally accessible.
Assertion Policy
@@ -225,7 +231,7 @@
that some abstractions are for abstract data types, where type-oriented
invariants make sense, while others are for abstract state machines,
where a package-oriented invariant would make sense. Here is the part of
-the original proposal associated with them, for historical reference.
+the original proposal associated with them, for historical reference.
We decided there was not a particularly good syntax for specifying them,
and they didn't seem to add sufficient benefit over simply using
postconditions.
@@ -233,16 +239,16 @@
This was the general form of a package invariant:
package P is
-
+
pragma Invariant(P, Validate);
...
-
+
function Validate return Boolean;
-
+
end P;
-
+
Here is a more formal syntax for the pragma:
pragma Invariant(package_local_name,
@@ -974,6 +980,131 @@
I'll try to make sure something is proposed well before the November meeting (it
has to be, or it can't be included in Amendment 2). Once we have an outline, we
can then throw brickbats, I mean discuss the details.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Sunday, June 6, 2010 10:35 PM
+
+Here is an update to AI-146 on Type invariants. [This is version /04 of the AI -
+Editor.] I pretty much tried to just follow the recommendations from the
+minutes.
+
+****************************************************************
+
+From: Steve Baird
+Sent: Monday, June 7, 2010 1:50 PM
+
+> AARM Implementation Note: The implementation might want to produce a warning
+> if a private extension has an ancestor type that is a visible extension,
+> and an invariant expression depends on the value of one of the components from
+> a visible extension part.
+
+What is the motivation for this?
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Monday, June 7, 2010 2:12 PM
+
+It was pointed out that applying an invariant to a private extension requires
+some care, since it might have some visible components inherited from the
+ancestor type, and if the invariant depends on one of those, the whole model
+breaks down. We are presuming that invariants are only violated while inside a
+subprogram with visibility on the full type. If code outside the package can
+change the value of a component mentioned in the invariant, then checking the
+invariant only on going from inside to outside the package "barrier" is useless.
+
+Note that the "invariant" AI specifically allows the invariant to be violated
+while inside the defining package. This is in contrast with the "predicate" AI
+which presumes the predicate is valid everywhere at all times, including when
+inside the defining package.
+
+Having both of these capabilities might be useful, but I don't think the terms
+"invariant" and "predicate" necessarily conjure up the actual distinction, and
+we might need to be more explicit in the name (e.g. "External_Invariant" or some
+such thing). Better might be to somehow merge the two so that a "predicate"
+applied to a private type is allowed to be violated while inside the defining
+package. That would be sort of like treating the private type and the full type
+as distinct subtypes, with the predicate applicable to one of them but not the
+other (that's not a bad model...).
+
+****************************************************************
+
+From: Steve Baird
+Sent: Monday, June 7, 2010 2:24 PM
+
+Got it. Thanks.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Monday, June 7, 2010 4:44 PM
+
+> Having both of these capabilities might be useful, but I don't think
+> the terms "invariant" and "predicate"
+> necessarily conjure up the actual distinction, ...
+
+That's what I've been saying all along!
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Monday, June 7, 2010 10:13 PM
+
+Well, maybe, but it has been all muddled up. The whole idea of an invariant that
+allows change is idiotic, and you've been trying to claim that these things are
+the same. I suppose that's true, they're both garbage in that both allow the
+underlying item to violate the "whateverwecallit" some of the time. That's a
+junk model and is not really any better than sprinkling assertions around.
+
+The subtype one was supposed to model an Ada constraint, but that falls apart
+for composite types. I'm not sure what the type one is supposed be, but it sure
+as heck isn't an invariant.
+
+If we can't describe simply what these things are, we shouldn't have them.
+Giving them names which don't reflect their real effects is clearly harmful.
+
+I wanted true user-defined constraints, but Steve has convinced me that those
+are impossible. That being the case, I'd rather opt for a few additional new
+constraints (or nothing at all in the worst case), rather than having these
+ill-defined assertions. These guys aren't very good contracts if they are
+violated half the time. So I propose we reconsider the well-defined constraints
+of AI-153-2, and dump these guys to the bottom of the sea. After all, the model
+of constraints in Ada is well-understood, and having new kinds isn't going to
+wreck any models or provide any false promises. (And it would give Robert what
+he wants: enumeration set constraints, without much other baggage.)
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Monday, June 7, 2010 10:27 PM
+
+...
+> Having both of these capabilities might be useful, but I don't think
+> the terms "invariant" and "predicate"
+> necessarily conjure up the actual distinction, and we might need to be
+> more explicit in the name (e.g.
+> "External_Invariant" or some such thing).
+> Better might be to somehow merge the two so that a "predicate" applied
+> to a private type is allowed to be violated while inside the defining
+> package.
+> That would be sort of like treating the private type and the full type
+> as distinct subtypes, with the predicate applicable to one of them but
+> not the other (that's not a bad model...).
+
+That wouldn't work if a Predicate is an aspect, as aspects are the same for all
+views of a type. And there is no way I'm going to stand for having an aspect
+that works differently depending on whether the clause is before or after the
+completion of the type -- that way lies madness (mine at least!).
+
+I think a better thought is to realize that these two things are attempts to
+solve the same problem, and we have to recognize that having both is going to be
+*way* too confusing. We have to choose one or the other (or neither, as
+suggested in my previous message). We have lots of failed designs, so I don't
+think there is a problem adding one more to the list. I know we talked about
+killing this one at the meeting in Tucker's office, but didn't have the guts. I
+hope we have them in Spain...
****************************************************************
Questions? Ask the ACAA Technical Agent