CVS difference for ai05s/ai05-0146-1.txt
--- ai05s/ai05-0146-1.txt 2009/03/15 03:48:33 1.2
+++ ai05s/ai05-0146-1.txt 2009/06/08 04:01:51 1.3
@@ -1,4 +1,4 @@
-!standard 11.5 (00) 09-02-15 AI05-0146-1/01
+!standard 11.5 (00) 09-06-03 AI05-0146-1/02
!standard 11.4.1 (10)
!class amendment 09-02-15
!status work item 09-02-15
@@ -10,9 +10,9 @@
!summary
To augment the basic "assert" pragma capability of Ada 2005,
-we propose pragmas for specifying invariants for packages and types.
+we propose constructs for specifying invariants for types.
-The semantics for these pragmas are defined in terms of the
+The semantics for these constructs are defined in terms of the
Assertion_Error exception used by the Assert pragma and the
Assertion_Policy configuration pragma.
@@ -30,70 +30,103 @@
implementation of a package to conform to the constraints of the parameter
and result subtypes of the visible subprograms of the package.
-Effectively, invariants may be considered as generalized, user-definable
-constraints. They have the same power to define more accurately the
-"contract" between the user and implementor of a package, and to thereby
-catch errors in usage or implementation earlier in the development cycle.
-They also can provide valuable documentation of the intended semantics of
-an abstraction.
+Note that type invariants are not the same thing as constraints, as
+invariants apply to all values of a type, while constraints are
+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
+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
+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.
+
+Invariants can help to more accurately define the "contract" between the
+user and implementor of a package, and thereby to catch errors in usage
+or implementation earlier in the development cycle. They also can
+provide valuable documentation of the intended semantics of an
+abstraction.
-!proposal
-
-The pragmas Package_Invariant, Invariant, and Inherited_Invariant
-have the following form:
-
- pragma Package_Invariant(package_local_name,
- [Check =>] boolean_expression [, [Message =>] string_expression]);
-
- pragma Invariant(first_subtype_local_name,
- [Check =>] boolean_expression [, [Message =>] string_expression]);
-
- pragma Inherited_Invariant(tagged_first_subtype_local_name,
- [Check =>] boolean_expression [, [Message =>] string_expression]);
-The package_local_name for Package_Invariant must denote the immediately
-enclosing program unit, which must be a package.
+!proposal
-The first_subtype_local_name for Invariant must denote a first subtype
-declared in the immediately enclosing region, which must be a package.
-The first_subtype_local_name must appear at least once wthin the
-boolean_expression, and each appearance represents a "current instance"
-of the type.
-
-The tagged_first_subtype_local_name for Inherited_Invariant must denote
-a tagged first subtype declared in the immediately enclosing region,
-which must be a package. The first_subtype_local_name must appear at
-least once wthin the boolean_expression, and each appearance represents
-a "current instance" of the corresponding class-wide type.
+We propose to allow the specification of an Invariant "aspect" of a
+type, as well as an Invariant'Class aspect of a tagged type. These
+aspects are specified using a construct of the following form:
+
+
+ package Q is
+
+ type T(...) is private
+ with Invariant => Is_Valid(T);
+
+ type T2(...) is abstract tagged private
+ with Invariant'Class => Is_Valid(T2);
+
+
+ function Is_Valid(X : T) return Boolean;
+
+ function Is_Valid(X2 : T2) return Boolean is abstract;
+
+ end Q;
+
+
+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}];
+
+ aspect_mark ::= identifier['Class]
+
+ 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];
+
+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 an invariant pragma is
-"Check," then the associated check is performed at the following
+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 Package_Invariant pragma, upon return
- from a call on any procedure defined within the declarative
- region of the package that is visible outside the package,
- a check is made that the given boolean_expression evaluates to True;
- also, immediately after completing elaboration of the package.
-
-* For an Invariant pragma, upon return from a call
+* 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 boolean_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.
+ 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 an Inherited_Invariant pragma, upon return from a call
- on any procedure that
+* 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,
@@ -112,7 +145,7 @@
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.
+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
@@ -124,55 +157,59 @@
Assertion Policy
-If the assertion policy at the point of an invariant
-pragma is "Check" then the semantics are as described above.
-If the assertion policy at the point of the pragma is
-"Ignore" then the pragma has no effect.
+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.
!wording
+** TBD **
!discussion
+
+We have provided only type oriented "invariant"
+specifications. We considered but ultimately rejected the idea of
+package-oriented invariants (see section on this below).
-We have provided both type oriented and package oriented "invariant"
-pragmas. This reflects the fact that some abstractions are for abstract
-data types, while others are for abstract state machines. We only
-enforce the package-oriented invariant on return from visible procedures
-of the package. If a visible function has side-effects, the implementor
-may want to insert an explicit postcondition on the function, or an
-Assert pragma inside.
For type invariants, we apply them on [IN] OUT parameters of procedures
after the call, and on the result of functions and conversions.
-The type invariants are defined by a boolean epxression, with any
+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.
-Invariant checks apply to all calls on (relevant) procedures
-declared in the visible part of the package, even those within the package.
+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
+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 invariant pragmas equivalent to a series of
-postcondition pragmas. We considered making invariant checks apply only to
-calls from outside the package, but this appeared to complicate the
-implementation and description with little additional benefit.
+at the call point, and makes the invariants equivalent to a
+series of postconditions. We considered making invariant checks
+apply only to calls from outside the package, but this appeared to
+complicate the implementation and description with little additional
+benefit.
The invariant checks are performed as postcondition checks to ensure
-that violations are caught as soon as possible. Presumably the invariants
-could also be enforced as preconditions, but those checks would in
-general be redundant, and the failures would be harder to track 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 pragma. 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.
+that violations are caught as soon as possible. Presumably the
+invariants could also be enforced as preconditions, but those checks
+would in general be redundant, and the failures would be harder to track
+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.
Assertion Policy
@@ -182,36 +219,91 @@
same set of identifiers. This would give the programmer more
control. On the other hand, typically either the programmer wants
full debugging, or full speed. Intermediate points seem relatively
-rare.
+rare, and it seems even more unlikely that the intermediate point
+would correspond to the distinction between assertions and
+invariants.
+
+Package Invariants *not* provided
+
+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.
+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.
+
+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,
+ [Check =>] boolean_expression [, [Message =>] string_expression]);
+
+The package_local_name for pragma Invariant must denote the immediately
+enclosing program unit, which must be a package.
+
+Checks would be performed as follows:
+* For a package Invariant pragma, upon return
+ from a call on any procedure defined within the declarative
+ region of the package that is visible outside the package,
+ a check is made that the given boolean_expression evaluates to True;
+ also, immediately after completing elaboration of the package.
+
+We would propose the same name resolution deferral for package
+invariants, though there it is less critical, presuming we stick with a
+pragma. If we were to use something like the aspect specification
+syntax for a package invariant (e.g. "package P with Invariant =>
+Validate is ... end P;") then we would clearly have to defer name
+resolution.
+
+We would only enforce the package-oriented invariant on return from
+visible procedures of the package. If a visible function has
+side-effects, the implementor may want to insert an explicit
+postcondition on the function, or an Assert pragma inside.
+
!example
generic
type Item is private;
package Stacks is
- type Stack is private;
+ type Stack is private
+ with Invariant => Is_Valid_Stack(Stack);
function Is_Empty(S : in Stack) return Boolean;
function Is_Full(S : in Stack) return Boolean;
- procedure Push(S : in out Stack; I : in Item);
- pragma Precondition(Push, not Is_Full(S));
- pragma Postcondition(Push, not Is_Empty(S));
-
- procedure Pop(S : in out Stack; I : out Item);
- pragma Precondition(Pop, not Is_Empty(S));
- pragma Postcondition(Pop, not Is_Full(S));
+ procedure Push(S : in out Stack; I : in Item)
+ with Precondition => not Is_Full(S)
+ Postcondition => not Is_Empty(S);
+
+ procedure Pop(S : in out Stack; I : out Item)
+ with Precondition => not Is_Empty(S)
+ Postcondition => not Is_Full(S);
- function Top(S : in Stack) return Item;
- pragma Precondition(Top, not Is_Empty(S));
+ function Top(S : in Stack) return Item
+ with Precondition => not Is_Empty(S);
function Is_Valid_Stack(S : in Stack) return Boolean;
- pragma Invariant(Stack, Is_Valid_Stack(Stack));
Stack_Error : exception;
private
-- whatever
end Stacks;
+
!ACATS test
Questions? Ask the ACAA Technical Agent