Version 1.1 of ai05s/ai05-0146-1.txt
!standard 11.5 (00) 09-02-15 AI05-0146-1/01
!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
!summary
To augment the basic "assert" pragma capability of Ada 2005,
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, 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.
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.
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 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
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.
* For an Inherited_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 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.
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 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
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.
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 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 Ada 2005,
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 Invariant(Stack, Is_Valid_Stack(Stack));
Stack_Error : exception;
private
--
end Stacks;
!ACATS test
!appendix
From: Tucker Taft
Sent: Sunday, February 15, 2009 4:30 PM
Here is a resurrection of AI95-00375 on type and package invariants.
We discussed the type invariants at AdaCore. I left in the
Package_Invariant because it seemed simple and useful.
[This is version /01 of the AI - ED.]
****************************************************************
Questions? Ask the ACAA Technical Agent