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

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

From: Yannick Moy
Sent: Monday, August 31, 2009  11:01 AM

I am forwarding here the beginning of a conversation with Ed Schonberg about
type invariants (AI05-0146), to be continued on this list.

Yannick Moy wrote:

> I have the feeling that the following rule stated for AI 05-0146 does
> not make it easy to check a type invariant:
>
>> > 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).
>
> The proposal only requires that (in) out parameters of primitive
> operations are checked, which does not seem sufficient to me. I also
> read the thread, and you seemed to agree with the proposal:
>
>> > 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).
>
> I do not see how this prevents violating the invariant of an object of
> that type different from the (in) out parameters, e.g., through a
> pointer. I have written a small example (attached) to explain my point.
> Do you agree there is a problem here, or did I miss something?

Ed Schonberg wrote:

> I agree that the proposal is not complete, and your neat example shows
> how to poke holes in it.  I'm not sure that there is a formulation
> that is reasonably cheap to implement that would catch this example.
> Throughout the discussion there is of course a pragmatic thread: we
> cannot require implementations to do data-flow. Do you have a model
> for verification of invariants that would catch this case? Recall that
> this would have to be only for external calls, i.e. calls to Bad from
> outside of package A.  I suspect that once you introduce indirection
> like this it becomes undecidable, and you don't want to put the check
> within the procedure body, because it may be an intended internal
> violation of the invariant.

Yannick Moy wrote:

>> I agree that the proposal is not complete, and your neat example
>> shows
>> > how to poke holes in it.  I'm not sure that there is a formulation
>> > that is reasonably cheap to implement that would catch this example.
>
> I discussed it with Cyrille, and he also pointed to me that it is
> probably impractical to have an invariant that extends to "all objects
> of that type" at any given point in the program. In that case, an
> invariant is more like a shorthand for the equivalent set of pre- and
> postconditions, no more, and I think it should be emphasized in the
> wording of the problem section of the AI. In particular, the current
> wording is wrong, if we keep this notion of "never guaranteed true for
> all objects" invariant.
>
>> > Throughout the discussion there is of course a pragmatic thread: we
>> > cannot require implementations to do data-flow. Do you have a model
>> > for verification of invariants that would catch this case?
>
> Spec# ensures that the invariant
> 	obj.inv = "true" ==> obj.Inv()
> is always true, where "inv" is a hidden field of every object and "Inv"
> is the invariant of this particular object, by enforcing a detailed
> (and
> heavy) coding practice, in which an object must be "opened" explicitly
> before it is modified.
>
> JML does not ensure anything: invariants in JML are really just
> shorthands for pre- and postconditions.
>
> In our case, I think a very simple restriction would guarantee that
> the invariant is really valid for all objects of that type, outside of
> the part of the call-graph dominated by a procedure of package A
> (which may still include code outside of A): forbid modification of an
> object of that type that is not an (in) out parameter!
>
>> > Recall that this
>> > would have to be only for external calls, i.e. calls to Bad from
>> > outside of package A.  I suspect that once you introduce
>> > indirection like this it becomes undecidable, and you don't want to
>> > put the check within the procedure body, because it may be an
>> > intended internal violation of the invariant.
>
> I agree that modification through an access type makes any static
> verification of the invariant undecidable. So either we forbid it, or
> we loosen the interpretation of 'invariant' (or we have 2 different
> kinds of invariants, kind-of weak and strong invariants?)

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

From: Yannick Moy
Sent: Monday, August 31, 2009  1:51 PM

Attaching the example mentioned in the previous mail.

package A is
   type T is private;
      -- with Invariant => Ok(T);
   function Ok (This : in T) return Boolean;
   procedure Bad (This : in out T);
private
   type T is record
      J : Integer;
      Next : access T;
   end record;
end A;

package body A is
   function Ok (This : in T) return Boolean is
   begin
      return This.J >= 0;
   end Ok;
   procedure Bad (This : in out T) is
   begin
      This.Next.J := -1;
   end Bad;
end A;

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

From: Steve Baird
Sent: Monday, August 31, 2009  3:32 PM

> I agree that modification through an access type makes any static
> verification of the invariant undecidable. So either we forbid it, or
> we loosen the interpretation of 'invariant' (or we have 2 different
> kinds of invariants, kind-of weak and strong invariants?)

And access types are just one way of running into this problem, right? A routine
which updates a global variable or a subcomponent of a parameter might result in
similar problems without involving access types.

Perhaps the name "Invariant" suggests something stronger than what this
mechanism implements, but this mechanism still seems like it might save a lot of
duplicated pre- and post-conditions. If we want to keep the mechanism but change
the name, someone will have to come up with a better name than Weak_Invariant or
I_Sure_Hope_This_Is_Usually_True .

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

From: Bob Duff
Sent: Monday, August 31, 2009  5:21 PM

> In our case, I think a very simple restriction would guarantee that
> the invariant is really valid for all objects of that type, outside of
> the part of the call-graph dominated by a procedure of package A
> (which may still include code outside of A): forbid modification of an
> object of that type that is not an (in) out parameter!

Can you explain that a bit more?  I'm not sure why it works.

> I agree that modification through an access type makes any static
> verification of the invariant undecidable. So either we forbid it, or
> we loosen the interpretation of 'invariant'...

In Eiffel, an invariant is just a short-hand for a bunch of pre- and
postconditions.  Eiffel requires checking the invariant (at run time) on both
entry and exit of each method.  The reason is basically the same as in your
example -- pointers.  It's worse in Eiffel, because pointers are more
ubiquitous.

In an Ada context, if we follow the Eiffel ideas, we would check the invariant
for an 'in' parameter on entry to a procedure.

But that's uncomfortable.  It is the responsibility (conceptually) of the
package itself to make sure the invariant is always true (for some definition of
"always" ;-)).  But preconditions are the responsibility of the caller. How is
the caller supposed to ensure an invariant?  It can't.

>... (or we have 2 different kinds
> of invariants, kind-of weak and strong invariants?)

I've thought about that a little.  I wonder if it makes sense to let the
compiler decide which are weak and strong (as opposed to letting the programmer
label them)?

It sure would be nice if at least _some_ invariants are statically provable. It
seems hopeless to prove an invariant, unless you can somehow know that checking
the invariant on exit from a subprogram (for '[in] out' params and function
results) implies that the invariant _must_ be true on entry (for 'in [out]'
params).  If you know that, you have some hope of doing an inductive proof.

Do we need 'globals' annotations, in the SPARK sense?

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

From: Randy Brukardt
Sent: Monday, August 31, 2009  8:18 PM

> > In our case, I think a very simple restriction would guarantee that
> > the invariant is really valid for all objects of that type, outside
> > of the part of the call-graph dominated by a procedure of package A
> > (which may still include code outside of A): forbid modification of
> > an object of that type that is not an (in) out parameter!
>
> Can you explain that a bit more?  I'm not sure why it works.

I don't think it does work, because the problem is modification of a logical
portion of the object that is not actually a part (in the technical sense) of
the object (that is, something that is accessed by a pointer rather than being a
(sub)component of the object).

OTOH, modifications of logical parts of "in" objects that have invariants via
pointers can be detected, and one could imagine having a warning about doing so
damaging the meaning of invariant. But it would be pretty nasty to make such
code illegal (especially as you can't tell for sure if pointer points at a
logical part of the current object, or at some other object).

...
> It sure would be nice if at least _some_ invariants are statically
> provable.
> It seems hopeless to prove an invariant, unless you can somehow know
> that checking the invariant on exit from a subprogram (for '[in] out'
> params and function results) implies that the invariant _must_ be true
> on entry (for 'in [out]' params).  If you know that, you have some
> hope of doing an inductive proof.
>
> Do we need 'globals' annotations, in the SPARK sense?

Yes, absolutely. Without them, you can't do anything much statically with
preconditions/postconditions either, because the compiler cannot know whether
there are any side-effects in the predicate functions (there shouldn't be, but
if there are, it would be evil for a compiler to *introduces* erroneousness
because it removes/changes side-effects in preconditions. Adding preconditions
ought never make the program less safe!) The same is true for invariants.

Tucker and I had discussed this in the context of some previous discussion, and
we had gotten as far as trying to sketch out the form of such annotations. But
we didn't quite agree on the details, and we agreed to put it off until later.
(I believe this was just before the Brest meeting.) I suppose "later" is rapidly
approaching...

Note that I'd been trying to solve this problem with rules about purity, but
using globals annotations for that seems to work even better, being far more
flexible. They also (appear) easy to enforce, and since they're optional, there
shouldn't be any problem with enforcing them (if you can't write an enforcable
globals annotation, then don't write one at all).

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

From: Robert C. Leif
Sent: Tuesday, September 1, 2009  9:28 AM

I have three questions:

1.  Could some of the invariants be checked at compile time and not need to be
    checked at run time?

2.  Could the units of a numerical value be part of the invariants and be
    checked as precondition and the units of returned values or out values be
    checked as a post-condition?

3.  Could item 2 be limited to compile time checking?


It should be noted that starting with Bill Whitaker some of us have been waiting
for an elegant, efficient solution in Ada to the units problem.

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

From: Yannick Moy
Sent: Tuesday, September 1, 2009  1:47 AM

>> In our case, I think a very simple restriction would guarantee that
>> the invariant is really valid for all objects of that type, outside
>> of the part of the call-graph dominated by a procedure of package A
>> (which may still include code outside of A): forbid modification of
>> an object of that type that is not an (in) out parameter!
>
> Can you explain that a bit more?  I'm not sure why it works.

There are 2 sides to this, as the comment from Randy Brukardt shows:
1) do not allow the invariant to mention anything beyond the value or the direct
   fields in the private type;
2) only allow to violate the invariant of those objects which invariant will be
   checked on subprogram exit, which are the [in] out parameters.

This is quite restrictive, as you cannot mention a value through an access type
in the invariant, even if it is through a field of the private type.

> In an Ada context, if we follow the Eiffel ideas, we would check the
> invariant for an 'in' parameter on entry to a procedure.

But we would not even be better off wrt this notion of strong invariants.

>> ... (or we have 2 different kinds
>> of invariants, kind-of weak and strong invariants?)
>
> I've thought about that a little.  I wonder if it makes sense to let
> the compiler decide which are weak and strong (as opposed to letting
> the programmer label them)?

I guess that depends on what you allow in the invariant. In general, it would
not be feasible to decide whether an external call modifies an object by just
looking at the declarations. But if you stick to rule (1)  above, where an
invariant only mentions value or direct fields of the private type, then only
the subprograms in the current package can modify the value of the invariant.

> It sure would be nice if at least _some_ invariants are statically provable.
> It seems hopeless to prove an invariant, unless you can somehow know
> that checking the invariant on exit from a subprogram (for '[in] out'
> params and function results) implies that the invariant _must_ be true
> on entry (for 'in [out]' params).  If you know that, you have some
> hope of doing an inductive proof.

There are 2 parts in this verification:
- checking that every subprogram that could violate the strong invariant does
  ensure it holds on exit. This is hard, usually needing some interaction of a
  user with provers. Better left as dynamic checks in general.
- checking that outside of the parts of the call-graph dominated by a call which
  could violate the strong invariant, the strong invariant holds. This should be
  very easy, by restricting the kind of invariants as in rules (1) and (2)
  above.

> Do we need 'globals' annotations, in the SPARK sense?

Not for strong invariants I think, but a common description of effects would be
great for any modular analysis of Ada, yes! Except we need more that SPARK, to
describe "any field Next reachable from this parameter" and other locations on
the heap.

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

From: Yannick Moy
Sent: Tuesday, September 1, 2009  4:17 AM

> I don't think it does work, because the problem is modification of a
> logical part of the object that is not actually a part of the object
> (that is, something that is accessed by a pointer rather than being a
> (sub)component of the object).

You are right, I answered to this too when I answered to Bob. The key to strong
invariant is maintaining a kind of 'ownership' between an object and the parts
of state that are mentioned in its invariant.

> OTOH, modifications of logical parts of "in" objects that have
> invariants via pointers can be detected, and one could imagine having
> a warning about doing so damaging the meaning of invariant. But it
> would be pretty nasty to make such code illegal (especially as you
> can't tell for sure if pointer points at a logical part of the current object, or at some other object).

I am not sure if we want to go into such complexity. If the invariant is allowed
to talk about things that are pointed-to, then it is probably simpler to just
stick to weak invariants, that are only true when they were just checked.

> Tucker and I had discussed this in the context of some previous
> discussion, and we had gotten as far as trying to sketch out the form
> of such annotations. But we didn't quite agree on the details, and we
> agreed to put it off until later. (I believe this was just before the
> Brest meeting.) I suppose "later" is rapidly approaching...

Do you have a pointer to these discussions? I would be very interested in
reading your sketch of annotations.

> Note that I'd been trying to solve this problem with rules about
> purity, but using globals annotations for that seems to work even
> better, being far more flexible. They also (appear) easy to enforce,
> and since they're optional, there shouldn't be any problem with
> enforcing them (if you can't write an enforcable globals annotation, then
> don't write one at all).

Great! I'd be happy to be part of that discussion too.

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

From: Randy Brukardt
Sent: Tuesday, September 1, 2009  1:36 PM

> It should be noted that starting with Bill Whitaker some of us have
> been waiting for an elegant, efficient solution in Ada to the units
> problem.

Don't hold your breath. Lots of very smart people (including Tucker) have tried
to address the units problem, and no "elegant, efficient" solution (that is
correct as well) has been found. Solutions that work either require runtime
checks (meaning not so efficient) or generating an extremely complex set of type
definitions (efficient, but not elegant). The best solution I've seen uses a
program to generate the nest of type and operator definitions needed for an
efficient solution. Part of the problem is that the interelationships between
units are not fixed; there are lots of different combinations. So it isn't
practical to include those relationships in a programming language.

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

From: Randy Brukardt
Sent: Tuesday, September 1, 2009  1:42 PM

> > Tucker and I had discussed this in the context of some previous
> > discussion, and we had gotten as far as trying to sketch out the
> > form of such annotations. But we didn't quite agree on the details,
> > and we agreed to put it off until later. (I believe this was just
> > before the Brest meeting.) I suppose "later" is rapidly approaching...
>
> Do you have a pointer to these discussions? I would be very interested
> in reading your sketch of annotations.

It was just in private e-mail; it never got far enough along for public
consumption. I was stuck on finding a reasonable form for listing specific
objects accessed. It seems to be a some sort of list, but the resolution rules
for that list are hard to explain (any object plus keywords null and private?).

> > Note that I'd been trying to solve this problem with rules about
> > purity, but using globals annotations for that seems to work even
> > better, being far more flexible. They also (appear) easy to enforce,
> > and since they're optional, there shouldn't be any problem with
> > enforcing them (if you can't write an enforcable globals
> annotation, then don't write one at all).
>
> Great! I'd be happy to be part of that discussion too.

I'll try to make sure something is proposed well before the November meeting (it
has to be, or it can't be included in Amendment 2). Once we have an outline, we
can then throw brickbats, I mean discuss the details.

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