CVS difference for ai05s/ai05-0146-1.txt
--- ai05s/ai05-0146-1.txt 2009/10/23 06:06:31 1.4
+++ ai05s/ai05-0146-1.txt 2009/11/03 06:03:06 1.5
@@ -1,4 +1,4 @@
-!standard 11.5 (00) 09-06-03 AI05-0146-1/02
+!standard 11.5 (00) 09-11-02 AI05-0146-1/03
!standard 11.4.1 (10)
!class amendment 09-02-15
!status work item 09-02-15
@@ -35,10 +35,10 @@
generally used to identify a subset of the values of a type. Invariants
are only meaningful on private types, where there is a clear boundary
(the enclosing package) that separates where the invariant applies
-(outside) and where it need not be satisfied (inside). In some ways, an
+(outside) and where it need not be satisfied (inside). In some ways, an
invariant is more like the range of values specified when declaring a
new integer type, as opposed to the constraint specified when defining
-an integer subtype. The specified range of an integer type can be
+an integer subtype. The specified range of an integer type can be
violated (to some degree) in the middle of an arithmetic computation,
but must be satisfied by the time the value is stored back into an
object of the type.
@@ -72,99 +72,96 @@
end Q;
+The invariant expression associated with a type is evaluated as a postcondition
+of any operation that creates, updates, or returns a value of the type.
-Here is a more formal syntax for the invariant specification, based
-on the more general aspect_specification syntax proposed for pre- and
-post-conditions:
-
- aspect_specification ::=
- [with aspect_mark => expression {,
- aspect_mark => expression}];
+!wording
- aspect_mark ::= identifier['Class]
+Modify 7.3(2 and 3/2):
- private_type_declaration ::=
+ private_type_declaration ::=
type defining_identifier [discriminant_part] is [[abstract] tagged] [limited] private
[aspect_specification];
- private_extension_declaration ::=
+ private_extension_declaration ::=
type defining_identifier [discriminant_part] is
[abstract] [limited | synchronized] new ancestor_subtype_indication
[and interface_list] with private
[aspect_specification];
-
-The aspect_marks used for invariants on types are Invariant and, if the
-type is tagged, Invariant'Class. The identifier of the type must appear
-at least once within the boolean_expression, and each appearance
-represents a "current instance" of the type, or of the corresponding
-class-wide type in the case of the aspect Invariant'Class.
-
-Name resolution on the expression (which must be of a boolean type) that
-specifies an invariant for a type is performed at the end
-of the visible part of the enclosing package, allowing it to refer to
-subprograms or other entities declared in the visible part, but
-following the specification of the invariant.
-
-If the assertion policy at the point of a specification of an invariant
-is "Check," then the associated check is performed at the following
-places:
-
-* For a type with a specified Invariant aspect, upon return from a call
- on any procedure that
-
- - has one or more [IN] OUT parameters of the specified type,
- - is defined within the immediate scope of the type, and
- - is visible outside the immediate scope of the type,
-
- one evaluation is performed of the expression for each such [IN] OUT
- parameter, with final value of the parameter as the current instance.
- Similarly, after evaluation of a function call or type conversion that
- returns the specified type, an evaluation is performed of the boolean
- expression with the result as the current instance. Finally, after
- default initialization of an object of the type, an evaluation is
- performed of the boolean_expression with the default-initialized
- object as the current instance.
-
-* For a tagged type with a specified Invariant'Class aspect, upon return
- from a call on any procedure that
-
- - has one or more [IN] OUT parameters of a type within the
- derivation class of the specified type,
- - is defined within the immediate scope of such a type, and
- - is visible outside the immediate scope of the type,
-
- one evaluation is performed of the boolean expression for each such
- [IN] OUT parameter. The parameter is view-converted to the class-wide
- type prior to the call, ensuring that any calls on dispatching
- operations are dispatching calls. Similarly, after evaluation of a
- function call or type conversion that returns a type within the
- derivation class, an evaluation is performed on the boolean_expression
- with the result as the current instance. Finally, after default
- initialization of an object of a type within the derivation class, an
- evaluation is performed of the boolean_expression with the
- default-initialized object as the current instance.
-
-If any of these evaluations produce False, Ada.Assertions.Assertion_Error is
-raised, with the specified Message if any, in the case of the Invariant pragma.
-
-The invariant checks are performed prior to copying back
-any by-copy [IN] OUT parameters. However, it is not specified
-whether any constraint checks associated with the copying back are
-performed before or after the invariant checks. If there are any
-postconditions associated with the procedure, it is not specified
-whether these checks are performed before, after, or interleaved with
-the invariant checks.
-Assertion Policy
-
-If the assertion policy at the point of an invariant specification is
-"Check" then the semantics are as described above. If the assertion
-policy at the point of the specification is "Ignore" then the
-specification has no effect.
+Add new section:
-!wording
+ 13.3.3 Type Invariants
-** TBD **
+ An invariant for a private type or private extension may be specified
+ 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
+ of the type.] Within an invariant expression associated with type T,
+ the type of the current instance is T for the Invariant aspect and
+ 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
+ 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
+ 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
+ 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
+ raised at the point of the object initialization, conversion, or call.
+ If a given call requires more than one evaluation of an invariant
+ expression, either for multiple objects of a single type or for
+ multiple types with invariants, the order of the evaluations is not
+ specified, and if one of them evaluates to False, it is not specified
+ whether the others are evaluated. Any invariant check is performed
+ prior to copying back any by-copy IN OUT or OUT parameters. It is not
+ specified whether any constraint checks associated with by-copy IN OUT
+ 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.]
!discussion
@@ -172,23 +169,23 @@
specifications. We considered but ultimately rejected the idea of
package-oriented invariants (see section on this below).
-
For type invariants, we apply them on [IN] OUT parameters of procedures
-after the call, and on the result of functions and conversions.
+after the call, and on the result of functions, conversions, and default
+initializations.
The type invariants are defined by a boolean expression, with any
appearance of the type name within the expression treated as a reference
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
package, which is clearly necessary given the placement of the
aspect specification on the declaration of the partial view.
-Invariant checks apply to all calls on (relevant) procedures declared in
+Invariant checks apply to all calls on (relevant) subprograms declared in
the visible part of the package, even for calls from within the package.
This allows the checks to be performed inside the procedures rather than
at the call point, and makes the invariants equivalent to a
@@ -204,12 +201,11 @@
down since the call that actually created the problem would be harder to
identify.
-We have not specified whether the invariants apply to any inherited
-primitive subprograms that are implicitly declared within the package
-containing the type. We have not specified whether invariants apply to
-dynamically-bound calls, which might reach subprograms that are not
-declared in the visible part of the package. Clearly these issues need
-to be resolved.
+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.
Assertion Policy
@@ -225,11 +221,11 @@
Package Invariants *not* provided
-We considered providing package invariants. This reflected the fact
+We considered providing package invariants. This reflected the fact
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.
@@ -237,16 +233,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,
@@ -287,15 +283,15 @@
function Is_Full(S : in Stack) return Boolean;
procedure Push(S : in out Stack; I : in Item)
- with Precondition => not Is_Full(S)
- Postcondition => not Is_Empty(S);
+ with Pre => not Is_Full(S)
+ Post => not Is_Empty(S);
procedure Pop(S : in out Stack; I : out Item)
- with Precondition => not Is_Empty(S)
- Postcondition => not Is_Full(S);
+ with Pre => not Is_Empty(S)
+ Post => not Is_Full(S);
function Top(S : in Stack) return Item
- with Precondition => not Is_Empty(S);
+ with Pre => not Is_Empty(S);
function Is_Valid_Stack(S : in Stack) return Boolean;
@@ -303,6 +299,7 @@
private
-- whatever
end Stacks;
+
!ACATS test
Questions? Ask the ACAA Technical Agent