!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
!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 constructs for specifying invariants for types.

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.

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

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

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 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.

!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).


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 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.  

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 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 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

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, 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
       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)
        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
        with Precondition => not Is_Empty(S);

    function Is_Valid_Stack(S : in Stack) return Boolean;

    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.

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