Version 1.2 of ais/ai-00375.txt

Unformatted version of ais/ai-00375.txt version 1.2
Other versions for file ais/ai-00375.txt

!standard 11.5 (00)          04-02-29 AI95-00375/01
!standard 11.4.1 (10)
!class amendment 02-02-05
!status No Action (8-0-0) 04-03-07
!status work item 02-02-05
!status received 02-02-05
!priority Medium
!difficulty Medium
!subject Type and Package Invariants
!summary
To augment the basic "assert" pragma capability proposed in AI-00286, we propose pragmas for specifying invariants for packages and types.
The semantics for these pragmas are defined in terms of the Assertion_Error exception used by the Assert pragma and the Assertion_Policy configuration pragma.
!problem
A number of programming paradigms include the heavy use of invariants associated with types or modules (i.e. packages). Having a basic standardized "Assert" pragma supports this approach to some degree, but generally requires that the Assert pragmas actually be inserted inside the bodies of the associated code. It would be much more appropriate if these invariants appeared on the specification of the types and packages rather than buried in the body, as it really represents part of the contract. In particular, one wants any implementation of a given package spec to conform to all of invariants specified, in the same way one wants any 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.
!proposal
The pragmas Package_Invariant, Type_Invariant, and Classwide_Type_Invariant have the following form:
pragma Package_Invariant(package_local_name,
boolean_function_name [, [Message =>] string_expression]);
pragma Type_Invariant(first_subtype_local_name,
boolean_function_name [, [Message =>] string_expression]);
pragma Classwide_Type_Invariant(tagged_first_subtype_local_name,
boolean_function_name [, [Message =>] string_expression]);
The package_local_name for Package_Invariant must denote the immediately enclosing program unit, which must be a package. The boolean_function_name for Package_Invariant must denote a parameterless function declared within the specified package that has a Standard.Boolean result.
The first_subtype_local_name for Type_Invariant must denote a first subtype declared in the immediately enclosing region, which must be a package. The boolean_function_name for Type_Invariant must denote a function with one parameter of the type denoted by the first_subtype_local_name, and a Standard.Boolean result.
The tagged_first_subtype_local_name for Classwide_Type_Invariant must denote a tagged first subtype declared in the immediately enclosing region, which must be a package. The boolean_function_name for Classwide_Type_Invariant must denote a dispatching function with one parameter of the type denoted by the tagged_first_subtype_local_name, and a Standard.Boolean result.
If the assertion policy at the point of an invariant pragma 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 call is performed on the specified parameterless function; also, immediately after completing elaboration of the package.
* For a Type_Invariant pragma, 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 call is performed on the specified boolean function for each such [IN] OUT parameter. Similarly, after evaluation of a function call or type converstion that returns the specified type, a call is performed on the specified boolean function passing the result. Finally, after default initialization of an object of the type, a call is performed on the specified boolean function passing the default-initialized object.
* For a Classwide_Type_Invariant pragma, 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 the type, and - is visible outside the immediate scope of the type,
one call is performed on the specified boolean dispatching function for each such [IN] OUT parameter. The parameter is view-converted to the class-wide type prior to the call, ensuring that the call is a dispatching call. Similarly, after evaluation of a function call or type conversion that returns a type within the derivation class, a dispatching call is performed on the specified boolean function passing the result. Finally, after default initialization of an object of a type within the derivation class, a dispatching call is performed on the specified boolean function passing the default-initialized object.
If any of these calls return False, Ada.Assertions.Assertion_Error is raised, with the specified Message if any.
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 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.
!wording
!discussion
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 a 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 invariants are defined by referring to a boolean function. The more general boolean_expression allowed in the other assertion-like pragmas was not used because it was unlikely that the invariant could be defined in terms of visible entities, and there was no obvious way to refer to the particular instance of the type for the Type_Invariant pragma. In addition, given that the checks may be performed at the call point, space economization argues for bundling the invariant into a callable subprogram. The programmer might as well do this bundling him/herself.
Invariant checks apply to all calls on (relevant) procedures declared in the visible part of the package, even those 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.
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 do not specify any inheritance of invariant pragmas. It might make sense for a type invariant to be inherited by its descendants. However, in that case, a separate Inheritable_Type_Invariant would probably be appropriate, based on the same argument given above relating to inheritable pre/postcondition pragmas. Presumably we would allow these pragmas in generic packages, with the obvious semantics in the instance.
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.
Assertion Policy
We have used the Assertion_Policy pragma defined in AI-00286, with the same options and interpretation. It might make sense to define a separate pragma, such as Invariant_Policy, but with the 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.
!example
generic type Item is private; package Stacks is type Stack is private;
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));
function Top(S : in Stack) return Item; pragma Precondition(Top, not Is_Empty(S));
function Is_Valid_Stack(S : in Stack) return Boolean; pragma Type_Invariant(Stack, Is_Valid_Stack);
Stack_Error : exception; private -- whatever end Stacks;
!ACATS test
!appendix

****************************************************************

Questions? Ask the ACAA Technical Agent