!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
    --  whatever
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.]

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

From: Bob Duff
Sent: Tuesday, February 24, 2009  10:25 AM

[Find the message that this is replying to in AI05-0145-1.]

>      type Set is interface
>        with
>          Invariant'Class =>
>            (Is_Empty(X)) = (Count(X) = 0);

I think invariants should apply to subtypes, not just types.
I think they are like constraints, and at least for scalars, can be checked in
the same places.

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

From: Gary Dismukes
Sent: Thursday, February 26, 2009  12:09 AM

Randy brought up that point at the meeting and he has an action item to make a
specific proposal along those lines.

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

From: Robert Dewar
Sent: Thursday, February 26, 2009  12:09 AM

I agree with this, BTW, I find Tuck's syntax suggestion basically nice, and
think that pre/post conditions are important enough to warrant syntax additions.

I do think that postconditions in the body are useful, and so would keep the
pragmas, certainly in GNAT anyway. It is true that preconditions in the body
are just assertions, so they are there just for symmetry, but postconditions
in the body are useful in that they come up front, which is the right position,
and they block all exits (which would be tedious to do manually with assertions).
I also think it is good to be able to control pre/post conditions separately
from normal assertions.

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

From: Alan Burns
Sent: Thursday, February 26, 2009  7:21 AM

> I think invariants should apply to subtypes, not just types.
> I think they are like constraints, and at least for scalars, can be 
> checked in the same places.
   
I've not followed the recent discussion on invariants, but am not sure how
you deal with the usual invariant that is true most of the time but not
during atomic updates.  Or a loop invariant that is true at the end of each
iteration but not during an iteration.

pre and post conditions are specific as to when they should evaluate to true,
but invariants cover a region (but not the whole program)

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

From: Bob Duff
Sent: Thursday, February 26, 2009  7:40 AM

> I've not followed the recent discussion on invariants, but am not sure 
> how you deal with the usual invariant that is true most of the time 
> but not during atomic updates.

I'm not sure, either.  That issue deserves some careful thought.
Perhaps scalars should be different from records?

>...  Or a loop invariant that is
> true at the end of each iteration but not during an iteration.

Isn't the loop-invariant case just a "pragma Assert" written at some point
within the loop (e.g. at the end of each iteration)?  I don't see any need for
a new feature for loop invariants.

The invariants I'm thinking of should apply to [sub]types.  Maybe also to packages.

> pre and post conditions are specific as to when they should evaluate 
> to true, but invariants cover a region (but not the whole program)

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

From: Tucker Taft
Sent: Thursday, February 26, 2009  9:18 AM

> I think invariants should apply to subtypes, not just types.
> I think they are like constraints, and at least for scalars, can be 
> checked in the same places.

We discussed this, and concluded that invariants and user-defined constraints
are both useful, but they are not the same thing.  Invariants are generally
imposed on the implementation of an abstraction, and translate into
*postconditions* on all operations that return values to the "outside" world.
Constraints are often used as *preconditions* on values being passed *in* to
a subprogram, and generally are required to be satisfied at all points, whereas
invariants are often false in the middle of a primitive operation.

So we concluded, I believe, that invariants are associated with an abstraction,
and hence a type, or perhaps a package, while constraints define a subset of
the values of a type, and hence are appropriately associated with a subtype.

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

From: Bob Duff
Sent: Thursday, February 26, 2009  7:57 AM

Question: In an invariant, does one refer to the "current instance" in the
usual way, by naming the [sub]type?  As in:

    type My_Int is range 0..1_000_000;

    subtype My_Even_Int is My_Int with
        Invariant => (My_Even_Int mod 2) = 0;


> I've not followed the recent discussion on invariants, but am not sure 
> how you deal with the usual invariant that is true most of the time 
> but not during atomic updates.

For scalars, one can use 'Base as always.  E.g. if you have X: in out My_Int,
and you want to temporarily set it to a negative number, you do something like:

    Temp : My_Int'Base := X;
    Temp := Temp - 10; -- might be negative
    Temp := abs Temp;
    X := Temp; -- OK, Temp is now nonnegative

Similarly, My_Even_Int'Base would be a subtype that is NOT restricted to even
numbers.

Not sure how this can work for records.

By the way, I think the "in" operator should take invariants into account.
E.g.:

    if Blah in My_Even_Int then ...

would be True iff Blah is an even number in the 0..1_000_000 range.

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

From: Edmond Schonberg
Sent: Thursday, February 26, 2009  12:50 PM

> Question: In an invariant, does one refer to the "current instance"  
> in the
> usual way, by naming the [sub]type?  As in:
>
>    type My_Int is range 0..1_000_000;
>
>    subtype My_Even_Int is My_Int with
>        Invariant => (My_Even_Int mod 2) = 0;

Invariants are intended for private types only.  Otherwise the invariant
may have to be verified on assignment or any operation that would visibly
modify a value of the type outside of the defining package. This is
impractical and not particularly useful (we have constraints for this, and
invariants are NOT constraints).  By limiting the invariant to a private
type, the check is limited to the visible primitive operations of the type
(what happens otherwise in the body stays in the body).

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

From: Stephen Michell
Sent: Thursday, February 26, 2009  1:04 PM

In general, I like Tucker's proposal.

On the issue of invariance, Alan is completely correct. Invariance for,
say,  the relationship between components or between state variables in a
class only allies when they are no threads executing subprograms that may
change that state. 

You can make invariance work for every execution step, but in general that
is going to require auxillary variables and a lot of very hard work.

We need to develop syntax to express when invariance applies, or possibly
when it does not apply, such as loop invariants only apply at the exit
condition and state invariants only apply at the precondition and
postcondition points of every subprogram that can see the state.

As part of this effort, we need a syntax for auxillary variables, declaration,
assignment and formal relationships.

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

From: Randy Brukardt
Sent: Thursday, February 26, 2009  1:49 PM

> I think invariants should apply to subtypes, not just types.
> I think they are like constraints, and at least for scalars, can be 
> checked in the same places.

We talked about that at my insistence. We decided that invariants and
constraints are different things that solve different problems. (Which
is what I have been saying all along.) Invariants apply to all values of
a type, and can be inherited. Constraints apply to particular views (not
necessarily an object). Constraints are checked at the points that language
currently defines (subtype conversion); invariants are checked only when
crossing the boundary of the defining package.

I was tasked in writing up a proposal for user-defined constraints
(resurrecting my old proposal on that topic, but now using syntax and
legality rules).

If we can have only one of these, I think user-defined constraints are far
more useful. But I can see uses for both.

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

From: Jean-Pierre Rosen
Sent: Friday, February 27, 2009  12:58 AM

> By limiting the invariant to
> a private type, the check is limited to the visible primitive 
> operations of the type  (what happens otherwise in the body stays in the body).
 
I understand limited to visible operations, but why primitives?

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

From: Edmond Schonberg
Sent: Friday, February 27, 2009  2:57 PM

No reason, written in haste. Of course visible classwide operations are included.

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

From: Jean-Pierre Rosen
Sent: Saturday, February 28, 2009  5:11 AM

Actually, I was thinking of operations that are not primitive because they are
declared, f.e., in a subpackage.

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