Version 1.15 of ai05s/ai05-0146-1.txt

Unformatted version of ai05s/ai05-0146-1.txt version 1.15
Other versions for file ai05s/ai05-0146-1.txt

!standard 7.3.2 (00)          10-10-19 AI05-0146-1/08
!class amendment 09-02-15
!status Amendment 2012 10-09-02
!status WG9 Approved 10-10-28
!status ARG Approved 8-0-1 10-06-20
!status work item 09-02-15
!status received 09-02-15
!priority Medium
!difficulty Medium
!subject Type Invariants
!summary
The basic assert pragma of Ada 2005 is augmented by the specification of type invariants.
!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 the specified invariants, 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 for 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
Using the aspect_specification syntax introduced in AI05-0183/1, 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;
The invariant expression associated with a type is evaluated as a postcondition of any operation that creates, updates, or returns a value of the type.
!wording
Add new section:
13.3.3 Type Invariants
For a private type or private extension, the following language-defined aspects may be specified with an aspect_specification:
Type_Invariant
This aspect shall be specified by an expression, called an *invariant expression*. Type_Invariant may be specified on a private_type_declaration or a private_extension_declaration.
Type_Invariant'Class
This aspect shall be specified by an expression, called an *invariant expression*. Type_Invariant'Class may be specified on a private_type_declaration or a private_extension_declaration.
Name Resolution
The expected type for an invariant expression is any boolean type.
[Redundant: Within an invariant expression, the identifier of the first subtype of the associated type denotes the current instance of the type.] Within an invariant expression associated with type T, the type of the current instance is T for the Type_Invariant aspect and T'Class for the Type_Invariant'Class aspect.
Legality Rules
The Type_Invariant'Class aspect shall not be specified for an untagged type. The Type_Invariant aspect shall not be specified for an abstract type.
Static Semantics
[Redundant: If the Type_Invariant'Class aspect is specified for a tagged type T, then the invariant expression applies to all descendants of T.]
Dynamic Semantics
If one or more invariant expressions apply to a type T, and the Assertion_Policy (see 11.4.2) at the point of the partial view declaration for T is Check, then an invariant check is performed at the following places, on the specified object(s):
* After default initialization of an object of type T, on the new object;
* After conversion to type T, on the result of the conversion;
* After a call on the Read or Input stream attribute of the type T, on the object initialized by the stream attribute;
* Upon return from a call on any subprogram or entry that: - has a result of type T, or one or more IN OUT or OUT parameters of type T, - is explicitly declared within the immediate scope of type T (or is a part of an instance of a generic unit declared within the immediate scope of type T), and - is visible outside the immediate scope of type T or overrides an operation that is visible outside the immediate scope of T, on the result object of type T, and on each IN OUT or OUT actual parameter of type T.
The invariant check consists of the evaluation of each invariant expression that applies to T, on each of the objects specified above. If any of these evaluate to False, Ada.Assertions.Assertion_Error is raised at the point of the object initialization, conversion, or call. If a given call requires more than one evaluation of an invariant expression, either for multiple objects of a single type or for multiple types with invariants, the order of the evaluations is not specified, and if one of them evaluates to False, it is not specified whether the others are evaluated. Any invariant check is performed prior to copying back any by-copy IN OUT or OUT parameters. It is not specified whether any constraint checks associated with by-copy IN OUT or OUT parameters are performed before or after any invariant checks. It is not specified whether any postcondition checks are performed before or after any invariant checks.
The invariant checks performed on a call are determined by the subprogram or entry actually invoked, whether directly, as part of a dispatching call, or as part of a call through an access-to-subprogram value.
[Redundant: If the Assertion_Policy in effect at the point of a subprogram or entry declaration is Ignore, then no invariant check is performed on a call on that subprogram or entry.]
AARM Note: Invariant checks on subprogram return are not performed on objects that are accessible only through access values. It is also possible to call through an access-to-subprogram value and reach a subprogram body that has visibility on the full declaration of a type, from outside the immediate scope of the type. No invariant checks will be performed if the designated subprogram is not itself externally visible. These cases represent "holes" in the protection provided by invariant checks.
AARM Implementation Note: The implementation might want to produce a warning if a private extension has an ancestor type that is a visible extension, and an invariant expression depends on the value of one of the components from a visible extension part.
!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, conversions, and default initializations.
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) subprograms 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 adopted a rule that the invariant checks performed are determined by the subprogram invoked, whether directly or indirectly, to match the rule for pre- and postconditions.
We do not worry about non-externally visible subprograms that have their Access attribute evaluated, even though the access value might be passed out of the package and called from outside the package. Therefore there are holes in the protection provided by type invariants. Note, however, these holes can only be created by the package itself (by passing out access-to-subprogram values); a client cannot create them on their own. Thus we don't require herculean efforts to catch all possible ways a value might be updated and then become externally accessible.
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 Pre => not Is_Full(S) Post => not Is_Empty(S);
procedure Pop(S : in out Stack; I : out Item) with Pre => not Is_Empty(S) Post => not Is_Full(S);
function Top(S : in Stack) return Item with Pre => not Is_Empty(S);
function Is_Valid_Stack(S : in Stack) return Boolean;
Stack_Error : exception; private -- whatever end Stacks;
!comment AI05-0247-1 moves this to 7.3.2
!corrigendum 7.3.2(0)
Insert new clause:
For a private type or private extension, the following language-defined aspects may be specified with an aspect_specification (see 13.3.1):
Type_Invariant
This aspect shall be specified by an expression, called an invariant expression. Type_Invariant may be specified on a private_type_declaration or a private_extension_declaration.
Type_Invariant'Class
This aspect shall be specified by an expression, called an invariant expression. Type_Invariant'Class may be specified on a private_type_declaration or a private_extension_declaration.
Name Resolution Rules
The expected type for an invariant expression is any boolean type.
Within an invariant expression, the identifier of the first subtype of the associated type denotes the current instance of the type. Within an invariant expression associated with type T, the type of the current instance is T for the Type_Invariant aspect and T'Class for the Type_Invariant'Class aspect.
Legality Rules
The Type_Invariant'Class aspect shall not be specified for an untagged type. The Type_Invariant aspect shall not be specified for an abstract type.
Static Semantics
If the Type_Invariant'Class aspect is specified for a tagged type T, then the invariant expression applies to all descendants of T.
Dynamic Semantics
If one or more invariant expressions apply to a type T, and the Assertion_Policy at the point of the partial view declaration for T is Check, then an invariant check is performed at the following places, on the specified object(s):
on the result object of type T, and on each in out or out actual parameter of type T.
The invariant check consists of the evaluation of each invariant expression that applies to T, on each of the objects specified above. If any of these evaluate to False, Ada.Assertions.Assertion_Error is raised at the point of the object initialization, conversion, or call. If a given call requires more than one evaluation of an invariant expression, either for multiple objects of a single type or for multiple types with invariants, the order of the evaluations is not specified, and if one of them evaluates to False, it is not specified whether the others are evaluated. Any invariant check is performed prior to copying back any by-copy in out or out parameters. It is not specified whether any constraint checks associated with by-copy in out or out parameters are performed before or after any invariant checks. It is not specified whether any postcondition checks are performed before or after any invariant checks.
The invariant checks performed on a call are determined by the subprogram or entry actually invoked, whether directly, as part of a dispatching call, or as part of a call through an access-to-subprogram value.
If the Assertion_Policy in effect at the point of a subprogram or entry declaration is Ignore, then no invariant check is performed on a call on that subprogram or entry.
!ACATS test
An C-Test is needed to check that invariants are tested at approproiate places.
!ASIS
No change needed.
!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.

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

From: Tucker Taft
Sent: Sunday, June 6, 2010  10:35 PM

Here is an update to AI-146 on Type invariants. [This is version /04 of the AI -
Editor.] I pretty much tried to just follow the recommendations from the
minutes.

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

From: Steve Baird
Sent: Monday, June 7, 2010  1:50 PM

>  AARM Implementation Note:  The implementation might want to produce a warning
>     if a private extension has an ancestor type that is a visible extension,
>     and an invariant expression depends on the value of one of the components from
>     a visible extension part.

What is the motivation for this?

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

From: Tucker Taft
Sent: Monday, June 7, 2010  2:12 PM

It was pointed out that applying an invariant to a private extension requires
some care, since it might have some visible components inherited from the
ancestor type, and if the invariant depends on one of those, the whole model
breaks down.  We are presuming that invariants are only violated while inside a
subprogram with visibility on the full type.  If code outside the package can
change the value of a component mentioned in the invariant, then checking the
invariant only on going from inside to outside the package "barrier" is useless.

Note that the "invariant" AI specifically allows the invariant to be violated
while inside the defining package.  This is in contrast with the "predicate" AI
which presumes the predicate is valid everywhere at all times, including when
inside the defining package.

Having both of these capabilities might be useful, but I don't think the terms
"invariant" and "predicate" necessarily conjure up the actual distinction, and
we might need to be more explicit in the name (e.g. "External_Invariant" or some
such thing). Better might be to somehow merge the two so that a "predicate"
applied to a private type is allowed to be violated while inside the defining
package. That would be sort of like treating the private type and the full type
as distinct subtypes, with the predicate applicable to one of them but not the
other (that's not a bad model...).

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

From: Steve Baird
Sent: Monday, June 7, 2010  2:24 PM

Got it. Thanks.

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

From: Bob Duff
Sent: Monday, June 7, 2010  4:44 PM

> Having both of these capabilities might be useful, but I don't think
> the terms "invariant" and "predicate"
> necessarily conjure up the actual distinction, ...

That's what I've been saying all along!

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

From: Randy Brukardt
Sent: Thursday, June 10, 2010  10:13 PM

Well, maybe, but it has been all muddled up. The whole idea of an invariant that
allows change is idiotic, and you've been trying to claim that these things are
the same. I suppose that's true, they're both garbage in that both allow the
underlying item to violate the "whateverwecallit" some of the time. That's a
junk model and is not really any better than sprinkling assertions around.

The subtype one was supposed to model an Ada constraint, but that falls apart
for composite types. I'm not sure what the type one is supposed be, but it sure
as heck isn't an invariant.

If we can't describe simply what these things are, we shouldn't have them.
Giving them names which don't reflect their real effects is clearly harmful.

I wanted true user-defined constraints, but Steve has convinced me that those
are impossible. That being the case, I'd rather opt for a few additional new
constraints (or nothing at all in the worst case), rather than having these
ill-defined assertions. These guys aren't very good contracts if they are
violated half the time. So I propose we reconsider the well-defined constraints
of AI-153-2, and dump these guys to the bottom of the sea. After all, the model
of constraints in Ada is well-understood, and having new kinds isn't going to
wreck any models or provide any false promises. (And it would give Robert what
he wants: enumeration set constraints, without much other baggage.)

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

From: Randy Brukardt
Sent: Thursday, June 10, 2010  10:27 PM

...
> Having both of these capabilities might be useful, but I don't think
> the terms "invariant" and "predicate"
> necessarily conjure up the actual distinction, and we might need to be
> more explicit in the name (e.g.
> "External_Invariant" or some such thing).
> Better might be to somehow merge the two so that a "predicate" applied
> to a private type is allowed to be violated while inside the defining
> package.
> That would be sort of like treating the private type and the full type
> as distinct subtypes, with the predicate applicable to one of them but
> not the other (that's not a bad model...).

That wouldn't work if a Predicate is an aspect, as aspects are the same for all
views of a type. And there is no way I'm going to stand for having an aspect
that works differently depending on whether the clause is before or after the
completion of the type -- that way lies madness (mine at least!).

I think a better thought is to realize that these two things are attempts to
solve the same problem, and we have to recognize that having both is going to be
*way* too confusing. We have to choose one or the other (or neither, as
suggested in my previous message). We have lots of failed designs, so I don't
think there is a problem adding one more to the list. I know we talked about
killing this one at the meeting in Tucker's office, but didn't have the guts. I
hope we have them in Spain...

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

From: Yannick Moy
Sent: Friday, June 11, 2010  12:26 AM

>>> Having both of these capabilities might be useful, but I don't think
>>> the terms "invariant" and "predicate"
>>> necessarily conjure up the actual distinction, ...

I quickly got used to the terminology, so it does not seem such a problem to me.

The term "invariant" clearly corresponds to properties of the private types that
should reasonably be expected by a client code of the package ("reasonably",
because we're not talking proof of programs here, and only proof can ensure
these invariants are never broken by the package which defines them, through
pointers, etc.).

The term "predicate" as well corresponds clearly to some property that a
(sub)type must respect at defined points in the program.

> Well, maybe, but it has been all muddled up. The whole idea of an
> invariant that allows change is idiotic

No! This is the well accepted definition of an invariant in the program-proof
research community. So if we are to use their legacy, we should forget about the
natural language implication that an "invariant" never changes. In proof of
programs, an invariant breaks or holds at specific points in the program. This
is perfectly fine.

There are even very interesting "history invariants" that allow capturing some
of these changes.
(http://research.microsoft.com/en-us/um/people/leino/papers/krml166.pdf)

> and you've been trying to claim that these things are the same. I
> suppose that's true, they're both garbage in that both allow the
> underlying item to violate the "whateverwecallit" some of the time.
> That's a junk model and is not really any better than sprinkling
> assertions around.

If you go this way, contracts are also just a way to sprinkle assertions around.
I think it is a very good model, very easy to understand, and very rich for both
dynamic and static verification, which already know very well how to use
assertions.

> The subtype one was supposed to model an Ada constraint, but that
> falls apart for composite types. I'm not sure what the type one is
> supposed be, but it sure as heck isn't an invariant.

Again, seeing an invariant as something that always holds is not the right way
to look at them.

> If we can't describe simply what these things are, we shouldn't have them.
> Giving them names which don't reflect their real effects is clearly harmful.

"type invariant" and "predicate subtype" don't hold for me the promise that the
invariant or predicate described will always hold. The AI clearly states when
these are checked, and that's perfectly fine with me.

> I wanted true user-defined constraints, but Steve has convinced me
> that those are impossible. That being the case, I'd rather opt for a
> few additional new constraints (or nothing at all in the worst case),
> rather than having these ill-defined assertions. These guys aren't
> very good contracts if they are violated half the time.

If you can state very precisely when they are expected to hold and when not,
then these guys are very good at expressing contracts. A contract is no more
than a very precise description of what you promise to do.

> So I propose we reconsider the
> well-defined constraints of AI-153-2, and dump these guys to the
> bottom of the sea. After all, the model of constraints in Ada is
> well-understood, and having new kinds isn't going to wreck any models
> or provide any false promises. (And it would give Robert what he
> wants: enumeration set constraints, without much other baggage.)

I think dropping type invariants and predicate subtypes because they do not
always hold would be a mistake: it would show more our lack of understanding of
invariants and predicates than a clearly motivated decision.

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

From: Randy Brukardt
Sent: Friday, June 11, 2010  2:04 AM

...
> > Well, maybe, but it has been all muddled up. The whole idea of an
> > invariant that allows change is idiotic
>
> No! This is the well accepted definition of an invariant in the
> program-proof research community. So if we are to use their legacy, we
> should forget about the natural language implication that an
> "invariant" never changes. In proof of programs, an invariant breaks
> or holds at specific points in the program. This is perfectly fine.

I doubt many Ada programmers are members of "the program-proof research
community". They will find the term misleading, even if it is technically used
correctly. (And I doubt that, for reasons noted below.)

...
> > I wanted true user-defined constraints, but Steve has convinced me
> > that those are impossible. That being the case, I'd rather opt for a
> > few additional new constraints (or nothing at all in the worst
> > case), rather than having these ill-defined assertions. These guys
> > aren't very good contracts if they are violated half the time.
>
> If you can state very precisely when they are expected to hold and
> when not, then these guys are very good at expressing contracts. A
> contract is no more than a very precise description of what you
> promise to do.

The problem here is that they can *never* be *expected* to hold. The only time
they are true is in the instant after they are checked, and that isn't
particularly useful.

Moreover, I think you may have missed the part of the AI that says that we
aren't even going to try to check invariants for calls through
access-to-subprogram values. That means that even in the places where they are
defined to be checked, they might not be if the program contains any access
calls -- something that is out of control of the package. That means that a
package author cannot even have an expectation that the invariants hold at the
boundary of the package, because all that the client has to do to defeat the
checking (usually unintentionally) is use an access-to-subprogram. And there is
no way for the package author to prevent that. Yuck.

> > So I propose we reconsider the
> > well-defined constraints of AI-153-2, and dump these guys to the
> > bottom of the sea. After all, the model of constraints in Ada is
> > well-understood, and having new kinds isn't going to wreck any
> > models or provide any false promises. (And it would give Robert what
> > he
> > wants: enumeration set constraints, without much other baggage.)
>
> I think dropping type invariants and predicate subtypes because they
> do not always hold would be a mistake: it would show more our lack of
> understanding of invariants and predicates than a clearly motivated
> decision.

I don't like the idea of adding additional checking models on subtypes if they
aren't clearly better than the one that is familiar to Ada programmers -
constraints. So far as I can tell, both invariants and predicates as proposed
are both more likely to cause trouble, especially with Ada programmers that are
used to being able to *believe* their constraints. They will never be able to
trust either of these as written (because there are a lot of holes, that is ways
to change a value so that it would fail the check, without triggering the
check), but I would expect that most programmers *would* trust these in the same
way that they trust constraints. Which will lead to a boatload of frustration,
and I suspect in many cases to abandoning the feature altogether or greatly
restricting its use (rather like many organizations do with use clauses).

There is also the problem of having two similar features with different sets of
insecurities - programmers would have trouble determining when to use one or the
other, remembering which they are using, and the like.

Finally, the real question is whether Ada needs these features at all. Ada
already has a powerful constraint system, and some targetted extensions to it
might provide the majority of the needed functionality (and the rest can be done
with preconditions and asserts). This is very different than for preconditions,
where there is little ability in Ada as it stands to do any checking on a call
(especially for interactions between parameters).

Anyway, food for thought.

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

From: Robert Dewar
Sent: Friday, June 11, 2010  7:10 AM

>> Well, maybe, but it has been all muddled up. The whole idea of an
>> invariant that allows change is idiotic
>
> No! This is the well accepted definition of an invariant in the
> program-proof research community. So if we are to use their legacy, we
> should forget about the natural language implication that an
> "invariant" never changes. In proof of programs, an invariant breaks
> or holds at specific points in the program. This is perfectly fine.

I strongly agree with Yannick on this point, basically I agree with Yannick's
entire message.

> I think dropping type invariants and predicate subtypes because they
> do not always hold would be a mistake: it would show more our lack of
> understanding of invariants and predicates than a clearly motivated decision.

yes!

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

From: Randy Brukardt
Sent: Friday, June 11, 2010  7:08 PM

> I wanted true user-defined constraints, but Steve has convinced me
> that those are impossible. That being the case, I'd rather opt for a
> few additional new constraints (or nothing at all in the worst case),
> rather than having these ill-defined assertions. These guys aren't
> very good contracts if they are violated half the time. So I propose
> we reconsider the well-defined constraints of AI-153-2, and dump these
> guys to the bottom of the sea. After all, the model of constraints in
> Ada is well-understood, and having new kinds isn't going to wreck any
> models or provide any false promises. (And it would give Robert what
> he wants: enumeration set constraints, without much other baggage.)

Right, that's what I really want, I don't see too much use in anything else,
although I don't mind the generalization. I do mind if the attempt at
generaliation fails and we lose the important feature :-)

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

From: Robert Dewar
Sent: Friday, June 11, 2010  7:11 AM

> I doubt many Ada programmers are members of "the program-proof
> research community". They will find the term misleading, even if it is
> technically used correctly. (And I doubt that, for reasons noted
> below.)

You would be surprised, remember that a major motivation of such features is
precisely to support formal techniques, and lots of Ada programmers are
interested in such approaches!

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

From: Jean-Pierre Rosen
Sent: Friday, June 11, 2010  7:21 AM

Moreover, DBC is a cornerstone of OO support in OOTiA/DO178C (and if you want to
learn more about this, you are welcome to register for my tutorial on Monday ;-)
)

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

From: Tucker Taft
Sent: Friday, June 11, 2010  8:00 AM

> ...
>>> Well, maybe, but it has been all muddled up. The whole idea of an
>>> invariant that allows change is idiotic
>> No! This is the well accepted definition of an invariant in the
>> program-proof research community. So if we are to use their legacy,
>> we should forget about the natural language implication that an
>> "invariant" never changes. In proof of programs, an invariant breaks
>> or holds at specific points in the program. This is perfectly fine.
>
> I doubt many Ada programmers are members of "the program-proof
> research community". They will find the term misleading, even if it is
> technically used correctly. (And I doubt that, for reasons noted below.)...

I think you are off base here.  Static analysis is definitely the direction the
world is heading as the complexity of doing full dynamic analysis grows
exponentially.  Static analysis is based on program-proof technology.
Preconditions and postconditions are related to program-proof technology. "Loop
invariants" are expressions that are true at a particularly point in the loop.
They are "invariant" because they are true each time the program passes through
the point where the invariant holds.

So what "invariant" means is something that is *always* true at particular
*points* in the execution. There are many interesting invariants that involve
relationships between multiple objects, or multiple components of the same
object.  These clearly can't be true at every point in the program, since you
generally can't simultaneously change multiple objects.  For example, you might
have an invariant that X.A = X.B + X.C.  Well clearly, you couldn't change any
of these and keep the invariant true.  But if the invariant is only specified to
hold at certain places, then so long as compensating changes to X.A, X.B, and
X.C are made between such places, the invariant is useful.

Subtype predicates/constraints work in part because there is an underlying type
without any predicate/ constraint.  That's why in Ada you can have a restricted
subtype like 0..10, but you can still do arithmetic where the intermediate
values are negative values, or greater than 10.  Similarly you can have an array
subtype of String(1..10) but still do slicing and concatenation that temporarily
violates the constraint.

My observation that a private type invariant, where the invariant only holds
outside the package, is similar to having two different subtype predicates, one
for outside the package, and one for inside.

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

From: Randy Brukardt
Sent: Saturday, June 12, 2010  7:16 PM

...
> I think you are off base here. ...

Fair enough. No point in arguing it, but at least you hopefully understand where
I'm coming from.

...
> Subtype predicates/constraints work in part because there is an
> underlying type without any predicate/ constraint.  That's why in Ada
> you can have a restricted subtype like 0..10, but you can still do
> arithmetic where the intermediate values are negative values, or
> greater than 10.  Similarly you can have an array subtype of
> String(1..10) but still do slicing and concatenation that temporarily
> violates the constraint.

Right.

> My observation that a private type invariant, where the invariant only
> holds outside the package, is similar to having two different subtype
> predicates, one for outside the package, and one for inside.

I suppose the model works, but I still think that is way too confusing. Ada
constraints work because you always know exactly what constraint holds at a
given point -- it is the one that belongs to the subtype of the entity, no
matter what. It doesn't depend on visibility or location or anything else. If
you start bringing visibility and location into it, even for this limited case,
it will mean that it will be very hard (and confusing) to determine what applies

I can live with the idea of type invariants, but please don't confuse the
existing constraint model to cram them into it -- they're something different. I
can live with the model of checks as outlined in the current AI, but those have
nothing whatsoever to do with constraint model of Ada.

Still, I think these aren't worth the confusion with predicates. Especially as
it is possible to use a combination of other features (including predicates) to
get the effect of these "invariants". So I still want to simplify here: choose
one or the other, and predicates are more generally useful. So...

Vote NO on 146!  :-)

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

From: Robert Dewar
Sent: Saturday, June 12, 2010  7:30 PM

> I suppose the model works, but I still think that is way too
> confusing. Ada constraints work because you always know exactly what
> constraint holds at a given point -- it is the one that belongs to the
> subtype of the entity, no matter what. It doesn't depend on visibility or location or anything else.
> If you start bringing visibility and location into it, even for this
> limited case, it will mean that it will be very hard (and confusing)
> to determine what applies

As you know, I am no friend of complex stuff, but I don't understand the
possible confusion here, this model seems perfectly clear to me.

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

From: Randy Brukardt
Sent: Saturday, June 12, 2010  8:15 PM

By itself, it might be OK. But combined with constraints that hold everywhere
and predicates that logically hold everywhere, it seems beyond nasty to do
something different if the aspect happens to occur on a private type. That's
especially true as the model of aspects in Ada has previously been that the
aspects are the same for all views of a type -- changing that model seems
especially dangerous. We don't have any mechanism for changing an aspect
depending on a view.

As a separate aspect with separate semantics, I can live with (but do not like)
the semantics of type invariants. I am totally opposed to any attempt to "unify"
these with predicates, because of the damage that would do to the aspect model
and to understanding.

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

From: Bob Duff
Sent: Sunday, June 13, 2010  4:26 PM

> Here is an update to AI-146 on Type invariants.

Looks good.  See comments, below.

One general comment, and this AI, and related ones.
I think it might be a good idea to say something in the AARM about our intent
with respect to static analysis.

Many "static analysis / proof of (so-called) correctness" folks sneer at the
idea of run-time checks having anything to do with proofs.  And all these AI's
do is add some run-time checks.

Points to be made:

    - We expect these run-time checks to feed into tools (could be
      part of the compiler, could be separate tools) that do
      static analysis.

    - It's beyond the scope of the Ada language to define such
      stuff, so we don't say much about it.

    - We freely admit that these features have loopholes.

    - Some tools may want to close the loopholes (e.g.
      make sure you don't refer to globals in an invariant).

    - Some tools may want to produce conditional proofs (e.g.
      we don't know X, but we know that IF there are no
      access types and so on that use the loopholes, then X).

I strongly believe that "static" vs. "dynamic" is not a property of some sort of
assertion facility, but is a property of the tool doing the analysis.

> !problem

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

I think this is a poor analogy.  I suggest you delete it from the AI.
The intermediate results being out of bounds doesn't match the crossing of the
public/private boundary that these invariants talk about.

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

Seems to me that the key point is that invariants apply to ALL subp's, including
the ones invented tomorrow, including the ones in derived (tagged) types, etc.
That's something that just can't be expressed using pragma Assert, or
pre/postconditions, or even comments.

> !wording

>   If one or more invariant expressions apply to a type T, and the Assertion_Policy
>   at the point of the partial view declaration for T is Check, then an
>   invariant check is performed at the following places, on the specified object(s):

>   * After default initialization of an object of type T, on the new
> object;

This essentially forces every type with invariants to have a sensible default
value (or have unknown discrims).  I'm not sure that's wise. Note that we
decided differently for predicates.  Maybe you should copy that rule.

Also, given the existence of loopholes that Randy likes to pound his shoe on the
table about, I think 'in' and 'in out' params ought to be checked on the way in.

>   * After conversion to type T, on the result of the conversion;
>
>   * Upon return from a call on any subprogram or entry that:
>       - has a result of type T, or one or more IN OUT or OUT
>         parameters of type T,
>       - is explicitly declared within the immediate scope of type T
>         (or is a part of an instance of a generic unit declared within
>         the immediate scope of type T), and
>       - is visible outside the immediate scope of type T or overrides
>         an operation that is visible outside the immediate scope of T,
>     on the result object of type T, and on each IN OUT or OUT
>     actual parameter of type T.
>
>   The invariant check consists of the evaluation of each invariant
>   expression that applies to T, on each of the objects specified above.
>   If any of these evaluate to False, Ada.Assertions.Assertion_Error is
>   raised at the point of the object initialization, conversion, or call.

I think "at the point ..." could be removed, without losing any info.

>   If a given call requires more than one evaluation of an invariant

"call" --> "evaluation", or something less specific (because type conv can do
multiple ones; so can default init).

>   expression, either for multiple objects of a single type or for
>   multiple types with invariants, ...

or for multiple invariants that apply to a single object of a single type

>...the order of the evaluations is not
>   specified, and if one of them evaluates to False, it is not specified
>   whether the others are evaluated. Any invariant check is performed
>   prior to copying back any by-copy IN OUT or OUT parameters.  It is not
>   specified whether any constraint checks associated with by-copy IN OUT
>   or OUT parameters are performed before or after any invariant checks.
>   It is not specified whether any postcondition checks are performed
>   before or after any invariant checks.

I wonder if the above could be simplified by saying that an invariant defines a
bunch of postconditions?

>   The invariant checks performed on a call are determined by the subprogram
>   or entry actually invoked, whether directly, as part of a dispatching call, or
>   as part of a call through an access-to-subprogram value.
>
>   [Redundant: If the Assertion_Policy in effect at the point of a
>   subprogram or entry declaration is Ignore, then no invariant check is
>   performed on a call on that subprogram or entry.]

This seems to contradict the prior rule about where the policy applies.
(I don't care too much what the exact rule is.)

> !discussion

> Invariant checks apply to all calls on (relevant) subprograms 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.

I agree with this rule, but it might be worth noting that it is different from
(and simpler than) the Eiffel rule.

My rationale is:

    - implementation of the Eiffel rule is way over complicated

    - the need for it is rare (a semi-educated guess)

    - the workaround is easy (declare another subprogram in the
      body to skip the inv check, and call that from the exported one).

I don't know if you want to say all that here, but if the ARG agrees with my
rationale...

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

I don't buy it.  If an invariant fails on the way 'in', that's a strong clue
that some client is driving one of their trucks through a loophole. That makes
it EASIER to track down, whereas if we only check on the way out, we will be
fooled into thinking it's THIS package's fault.

Eiffel checks on the way 'in', after admitting that there are loopholes.
Note that the loopholes in Eiffel are worse, because (almost) everything's a
pointer, so it's easy for a class to accidentally hand out pointers to parts of
itself.  That loophole exists in Ada, but should be rarer.

Anyway, if I lose this part of the argument, it's no big deal.  I will advocate
that GNAT turn on such checks via '-gnata'.

> We have adopted a rule that the invariant checks performed are
> determined by the subprogram invoked, whether directly or indirectly,
> to match the rule for pre- and postconditions.

Note to Randy: I think you missed this part, given one of your other messages.

> Note that we do not worry about subprograms that have their Access
> attribute evaluated, even though they might be called from outside the package.
> We recognize there are holes in the protection provided by type
> invariants, so we don't require herculean efforts to catch all
> possible ways a value might be updated and then become externally accessible.
>
> 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.

Right.  The useful "intermediate point" is that part of your program is more
trusted (via testing, or whatever), and some other part is less trusted. We DO
support that distinction (I think).

> !appendix
> ...

Best not to include the !appendix in emails.  ;-)

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

From: Bob Duff
Sent: Sunday, June 13, 2010  3:09 PM

I think the following message constitutes unhelpful hyperbole.
(I say that admitting that I am sometimes guilty of hyperbole myself!  ;-))

Both type invariants and subtype predicates have some loopholes.  That doesn't
mean they are "idiotic", "garbage", "junk model", "clearly harmful", "violated
half the time".  That's all just nonsense.  These things are clearly useful.

Note that constraints have loopholes, too.  That's unfortunate, but they're
still better than nothing.

> Well, maybe, but it has been all muddled up. The whole idea of an
> invariant that allows change is idiotic, and you've been trying to
> claim that these things are the same. I suppose that's true, they're
> both garbage in that both allow the underlying item to violate the
> "whateverwecallit" some of the time. That's a junk model and is not
> really any better than sprinkling assertions around.
>
> The subtype one was supposed to model an Ada constraint, but that
> falls apart for composite types. I'm not sure what the type one is
> supposed be, but it sure as heck isn't an invariant.
>
> If we can't describe simply what these things are, we shouldn't have them.
> Giving them names which don't reflect their real effects is clearly harmful.
>
> I wanted true user-defined constraints, but Steve has convinced me
> that those are impossible. That being the case, I'd rather opt for a
> few additional new constraints (or nothing at all in the worst case),
> rather than having these ill-defined assertions. These guys aren't
> very good contracts if they are violated half the time. So I propose
> we reconsider the well-defined constraints of AI-153-2, and dump these
> guys to the bottom of the sea. After all, the model of constraints in
> Ada is well-understood, and having new kinds isn't going to wreck any
> models or provide any false promises. (And it would give Robert what
> he wants: enumeration set constraints, without much other baggage.)

The ides that "sprinkling assertions around" (by hand) is just as good is
nonsense.  Both predicates and subtype invariants apply in ALL of certain
well-defined places.  To do that by hand is error prone.  (Think about the
inheritance of Invariant'Class, for example.  Or just think about adding a
procedure to a package -- "invariant" applies to all the procedures, including
the ones invented tomorrow.)

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

From: Bob Duff
Sent: Sunday, June 13, 2010  3:09 PM

> So I still want to
> simplify here: choose one or the other, and predicates are more
> generally useful. So...

Well, at least you and I agree that predicates are more generally useful than
invariants, so if we can't have both...

> Vote NO on 146!  :-)

But I wouldn't go that far (unless these things are too hard to implement.
That's really my main concern about Ada 2012 -- that it be feasible to
implement).

> As a separate aspect with separate semantics, I can live with (but do
> not
> like) the semantics of type invariants. I am totally opposed to any
> attempt to "unify" these with predicates, because of the damage that
> would do to the aspect model and to understanding.

OK, I give up on trying to unify predicates and invariants.  I still think
they're pretty similar, conceptually, with some minor details that are
different.  But I won't push that view on the Ada lanugage by trying to unify
them!

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

From: Bob Duff
Sent: Sunday, June 13, 2010  3:11 PM

> > ...enumeration set
> > constraints, without much other baggage.)
>
> Right, that's what I really want, I don't see too much use in anything
> else, although I don't mind the generalization. I do mind if the
> attempt at generaliation fails and we lose the important feature :-)

Robert,

Don't you see the use of having:

    subtype Access_Type_Entity_Id is Entity_Id
        with Predicate => Ekind (Access_Type_Entity_Id in ...);

    function Get_Designated_Type (E : Access_Type_Entity_Id) return ...;

    ... -- 100 other subprograms that operate on
        -- Access_Type_Entity_Ids, or return them,
        -- and 1000 local variables of this subtype.

?

The point is, you're often not dealing DIRECTLY with enumeration values, but
with records discriminated by those, or (in the case of Entity_Id), a table that
contains enums somewhere therein, or ....

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

From: Randy Brukardt
Sent: Sunday, June 13, 2010  6:58 PM

> I think the following message constitutes unhelpful hyperbole.
> (I say that admitting that I am sometimes guilty of hyperbole myself!
> ;-))
>
> Both type invariants and subtype predicates have some loopholes.  That
> doesn't mean they are "idiotic", "garbage", "junk model", "clearly
> harmful", "violated half the time".
> That's all just nonsense.  These things are clearly useful.

I disagree, especially in the case of "type invariants". The terminology (IMHO,
not shared by most) promises much more than they actually deliver. In that case,
I think that they will be far more confusing than helpful. In a vacuum (without
the existing Ada concepts, and especially without subtype predicates), I
wouldn't argue that they could be useful. But Ada is not a vacuum!

My biggest concern is really with the terminology, which according to the rest
of the group has been hijacked to mean something far from "invariant". I'm not
going to argue about how others are using (or misusing) the terminology, but I
cannot abide by it myself. If that is "hyperbole", so be it.

> Note that constraints have loopholes, too.  That's unfortunate, but
> they're still better than nothing.

Only in erroneous programs, for which no reasoning is possible. If there are any
others, we need to fix them!

...
> The ides that "sprinkling assertions around" (by hand) is just as good
> is nonsense.  Both predicates and subtype invariants apply in ALL of
> certain well-defined places.  To do that by hand is error prone.
> (Think about the inheritance of Invariant'Class, for example.  Or just
> think about adding a procedure to a package -- "invariant" applies to
> all the procedures, including the ones invented tomorrow.)

I really do not understand why you and others keep calling this "sprinkling".
Generally, there is only a very small number of places where these checks go,
and they are ones where most Ada programmers are going to explicitly write
checks no matter what "contracts" exist. For preconditions, there is only *one*
place where the checks go; that's usually true for postconditions as well
(although you have to take care when there are multiple exit points). For
subtype predicates, we are just talking about additional checks on parameters --
which is the first thing that you would normally write in an subprogram. (I
don't think subtype predicates will be very useful in other contexts, in this
sense they are like null exclusions.)

So only type invariants have any sort of "sprinkling" effect. And given that
hardly anyone will understand them well enough to use them correctly, I'm not
sure that is really harmful.

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

From: Bob Duff
Sent: Sunday, June 13, 2010  9:11 PM

> I disagree, ...

I know.  ;-)

>...especially in the case of "type invariants". The terminology  (IMHO,
>not shared by most) promises much more than they actually deliver. In
>that case, I think that they will be far more confusing than helpful.
>In a  vacuum (without the existing Ada concepts, and especially without
>subtype  predicates), I wouldn't argue that they could be useful. But
>Ada is not a  vacuum!
>
> My biggest concern is really with the terminology, which according to
> the rest of the group has been hijacked to mean something far from "invariant".

And I think ``far from "invariant"'' is hyperbole.  Invariants (and predicates)
are ALMOST ALWAYS true.  Yes, acc-to-subp and other stuff can cause trouble, but
that doesn't amount to "far from".  If you violate an invariant, it is HIGHLY
LIKELY that you'll get an exception pretty soon after.

> I'm not going to argue about how others are using (or misusing) the
> terminology, but I cannot abide by it myself. If that is "hyperbole",
> so be it.
>
> > Note that constraints have loopholes, too.  That's unfortunate, but
> > they're still better than nothing.
>
> Only in erroneous programs, for which no reasoning is possible. If
> there are any others, we need to fix them!

No, not only in erroneous programs.  Example:

    procedure P(X : Natural) is
    begin
        Put_Line(Natural'Image(X));
    end P;

The above can print "-1".  All it takes is an uninit var:

    Uninit : Natural;

    P(Uninit);

It's a programming error, but it's not erroneous.

The fact that the language does not require this programming error to be
detected is NOT a good argument against having constraints.

You're trying to use an analogous (bogus, IMHO) argument against invariants.
It's true that if you hand out (to clients) pointers to components of your
private type, those clients can "sneakily" violate the invariant by assigning
via such pointers.  The current situation is that the invariant is expressed as
a comment, and there's zero chance that such "sneaking" will be detected by run
time checks. With variants, on the other hand, there's a pretty good (not 100%)
chance that the sneaking will be caught.

In other words, I'm asking you to consider these features as compared to what we
have without them (mainly, comments), rather than comparing them to some ideal
features that we don't know how to design in the context of Ada.

> ...
> > The ides that "sprinkling assertions around" (by hand) is just as
> > good is nonsense.  Both predicates and subtype invariants apply in
> > ALL of certain well-defined places.  To do that by hand is error
> > prone.  (Think about the inheritance of Invariant'Class, for
> > example.  Or just think about adding a procedure to a package --
> > "invariant" applies to all the procedures, including the ones
> > invented tomorrow.)
>
> I really do not understand why you and others keep calling this
> "sprinkling".

I was specifically talking about invariants and predicates.
Those features are placed once, one the relevant [sub]type decl.
To do it by hand, you have to "sprinkle" on every call, return, and (for
predicates) a lot of places like assignments and initializations.  That sounds
like hundreds or thousands of places, to me.

>... Generally, there is only a very small number of places where  these
>checks go, and they are ones where most Ada programmers are going to
>explicitly write checks no matter what "contracts" exist. For
>preconditions,  there is only *one* place where the checks go; that's
>usually true for  postconditions as well (although you have to take
>care when there are  multiple exit points). For subtype predicates, we
>are just talking about  additional checks on parameters -- which is the
>first thing that you would  normally write in an subprogram. (I don't
>think subtype predicates will be  very useful in other contexts, in
>this sense they are like null exclusions.)

No, predicates are not like null exclusions in that regard.

The reason null exclusions are primarily useful on parameters and function
results is a because of a design mistake in Ada 83: for access types, there is
no distinction between "uninitialized" and "null".  For ex., that means you
can't declare a not-null local variable, and initialize it later.  Constraints
and predicates are different: you CAN declare a local variable with a
constraint, and initialize it later.  Similarly, null exclusions don't work very
well for components, but constraints and predicate do.

Anyway, even if we're talking only about parameters and function results, that's
still a lot of sprinkling.

Here's one data point: I just did some searching, and found over 4000 parameters
and results of type Node_Id in the GNAT sources.  My search method
underestimates -- it could easily be twice that.  And I'm sure that well over
99% of those will not operate properly on ALL Node_Ids -- they're retricted to
Node_Id's for statements, or for just assignment statements, or some other
predicate.

Adding local variables of type Node_Id into the mix, I'd guess we're talking
about tens of thousands of "sprinkles".  Approx. 100 subtype predicates could do
all that sprinkling automatically.

> So only type invariants have any sort of "sprinkling" effect. And
> given that hardly anyone will understand them well enough to use them
> correctly, I'm not sure that is really harmful.

"Hardly anyone"?  Bah.  I'm sure I could teach average-competence Ada
programmers to use invariants and predicates properly.  (Don't try to get me to
teach average-competence Ada programmers to use coextensions properly! Or even
tasking, for that matter.)

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

From: Robert Dewar
Sent: Sunday, June 13, 2010  9:17 PM

I entirely agree with Bob here, I was about to write my own message, and then
read Bob's and it said everything I wanted to say.

I don't understand (or sympathize) with Randy's position at all here, it seeems
to be based on a very personal and peculiar idea of what the term invariant
means in this context.

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

From: Tucker Taft
Sent: Tuesday, June 14, 2010  2:11 PM

...
> I strongly believe that "static" vs. "dynamic" is not a property of
> some sort of assertion facility, but is a property of the tool doing
> the analysis.

I basically agree with this.  Also just as an observation, the fact that pragma
Asserts started showing up in Ada code (and Java and C, for that matter) was a
big help to static analysis, even if their semantics were defined dynamically in
the language definition.  The reason pragma Assert didn't make it into Ada 95
was largely because of claims that:

   1) Folks not using static analysis have no use
      for them
   2) Folks using static analysis need something much
      for sophisticated.

(1) is demonstrably false, at least based on my experience.
(2) is also demonstrably false in my experience,
     but in Ada 2012 we are also addressing the issue
     of sophistication, by at least considering the
     addition of conditional expressions and quantified
     expressions.

...
>> 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, ...
>
> I think this is a poor analogy.  I suggest you delete it from the AI.
> The intermediate results being out of bounds doesn't match the
> crossing of the public/private boundary that these invariants talk
> about.

Fair enough.  I will drop it or try to find a better analogy.

...
> Seems to me that the key point is that invariants apply to ALL subp's,
> including the ones invented tomorrow, including the ones in derived
> (tagged) types, etc.  That's something that just can't be expressed
> using pragma Assert, or pre/postconditions, or even comments.

Subtype predicates also work on subp's invented tomorrow.
But as far as the "contract" for a private type, I think the "type invariant" is
more directly relevant.

If we always say "subtype predicate" and "type invariant"
(or even "private type invariant") in our discussion, hopefully we can do a
better job of keeping these things apart. They really *aren't* the same thing,
though I think we could describe the semantics of "private type invariants" in
terms of "subtype predicates."  (It would clearly not be possible to describe
the semantics of subtype predicates in terms of type invariants!)

Whether we want to eliminate type invariants and make a subtype predicate, when
applied to a partial view, have the special property of applying to *only* the
partial view "subtype" along the lines specified for "private type invariants,"
I could go either way.  Alternatively, we could keep the "Invariant =>" (or
"Type_Invariant =>") syntax, but describe its semantics in terms of "Predicate
=>" (or "Subtype_Predicate =>"), and do the checks at the same points as we do
for subtype predicates, that might be a way of reducing the amount of "bulk" in
the manual.

>>   If one or more invariant expressions apply to a type T, and the Assertion_Policy
>>   at the point of the partial view declaration for T is Check, then an
>>   invariant check is performed at the following places, on the specified object(s):
>
>>   * After default initialization of an object of type T, on the new
>> object;
>
> This essentially forces every type with invariants to have a sensible
> default value (or have unknown discrims).  I'm not sure that's wise.
> Note that we decided differently for predicates.  Maybe you should
> copy that rule.

I don't agree.  A private type invariant depends on having a well-defined
default-initialized state, unless of course the programmer has eliminated the
possibility of having default-initialized objects, by declaring the partial view
with "(<>)" unknown discriminants.

> Also, given the existence of loopholes that Randy likes to pound his
> shoe on the table about, I think 'in' and 'in out' params ought to be
> checked on the way in.

This doesn't seem logically necessary, but in the interests of being able to
define the semantics of private-type invariants in terms of subtype predicates,
I could see the advantage.  Adding them to all operations with "in" parameters
is clearly a dramatic increase in the number of checks required. Here is a case
where I might make it implementation defined, or perhaps some separate assertion
policy, which controls such things.  Perhaps we need at this point to add at
least one more language-defined policy, which would be "Minimal_Checks" vs.
"Full_Checks" or something like that.

...
>>   The invariant check consists of the evaluation of each invariant
>>   expression that applies to T, on each of the objects specified above.
>>   If any of these evaluate to False, Ada.Assertions.Assertion_Error is
>>   raised at the point of the object initialization, conversion, or call.
>
> I think "at the point ..." could be removed, without losing any info.

It is important for a "call" to know exactly where the exception is raised.  For
the other two I agree this is redundant.  We actually go on to say more about
the "call" so perhaps there is no need to say "at the point" in this sentence,
if we believe it is covered later for calls.


>>   If a given call requires more than one evaluation of an invariant
>
> "call" --> "evaluation", or something less specific (because type conv
> can do multiple ones; so can default init).

How can type conversion require multiple ones?

...
>> ...the order of the evaluations is not
>>   specified, and if one of them evaluates to False, it is not specified
>>   whether the others are evaluated. Any invariant check is performed
>>   prior to copying back any by-copy IN OUT or OUT parameters.  It is not
>>   specified whether any constraint checks associated with by-copy IN OUT
>>   or OUT parameters are performed before or after any invariant checks.
>>   It is not specified whether any postcondition checks are performed
>>   before or after any invariant checks.
>
> I wonder if the above could be simplified by saying that an invariant
> defines a bunch of postconditions?

Everyone loves equivalences! ;-)  It is also dangerous when writing an AI to
depend on the semantics of some other AI.  But if we believe preconditions and
postconditions are a slam dunk, then describing some of these as
preconditions/postconditions would seem to save on wording "bulk."

>>   The invariant checks performed on a call are determined by the subprogram
>>   or entry actually invoked, whether directly, as part of a dispatching call, or
>>   as part of a call through an access-to-subprogram value.
>>
>>   [Redundant: If the Assertion_Policy in effect at the point of a
>>   subprogram or entry declaration is Ignore, then no invariant check is
>>   performed on a call on that subprogram or entry.]
>
> This seems to contradict the prior rule about where the policy applies.
> (I don't care too much what the exact rule is.)

Can you elaborate on this contradiction?

...
>> 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.
>
> I don't buy it.  If an invariant fails on the way 'in', that's a
> strong clue that some client is driving one of their trucks through a loophole.
> That makes it EASIER to track down, whereas if we only check on the
> way out, we will be fooled into thinking it's THIS package's fault.

As suggested above, I am beginning to think we might need an additional checking
policy, perhaps just to get a "some-but-not-all" policy identifier into the
standard, even if the implementation defines some of the details of such an
intermediate policy. Yes of course implementations can define as many policies
as they want, but it would be nice to have a portable identifier for an
"intermediate" level of checking, so you could move source code across Ada
compilers without having to always change policy identifiers.

...
>> 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.
>
> Right.  The useful "intermediate point" is that part of your program
> is more trusted (via testing, or whatever), and some other part is less trusted.
> We DO support that distinction (I think).

Now I am contradicting myself, thinking that there is a useful intermediate
point.  The biggest difference would be eliminating the check on "in"
parameters, given that there are *many* more calls with an "in" parameter than
with in-out or out.  Also, checks on "out"/"in-out" parameters are easier to
eliminate when included "inside" the body.  Checks on "in" parameters are
essentially impossible to eliminate if the code is inside the body.

>> !appendix
>> ...
>
> Best not to include the !appendix in emails.  ;-)

Agreed.  Sorry about that.

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

From: Robert A Duff
Sent: Monday, June 14, 2010  10:03 PM

> > Seems to me that the key point is that invariants apply to ALL
> > subp's, including the ones invented tomorrow, including the ones in
> > derived
> > (tagged) types, etc.  That's something that just can't be expressed
> > using pragma Assert, or pre/postconditions, or even comments.
>
> Subtype predicates also work on subp's invented tomorrow.

Yes.  Are you saying the above "Invariants can help..."
is intended to contrast invariants with predicates?
I didn't get that.  Still don't, really.

> But as far as the "contract" for a private type, I think the "type
> invariant" is more directly relevant.

More than what?

> If we always say "subtype predicate" and "type invariant"
> (or even "private type invariant") in our discussion, hopefully we can
> do a better job of keeping these things apart.
> They really *aren't* the same thing, ...

Well, they have something in common, and some differences, and if we try to emphasize the commonality, Randy will snap.  ;-) So I"ve pretty much given up on that.

>...though I think
> we could describe the semantics of "private type invariants"
> in terms of "subtype predicates."

Probably, but I'm not sure it helps, and anyway, Randy will snap.

>...(It would clearly not
> be possible to describe the semantics of subtype predicates  in terms
>of type invariants!)

Agreed.

> Whether we want to eliminate type invariants and make a subtype
> predicate, when applied to a partial view, have the special property
> of applying to *only* the partial view "subtype" along the lines
> specified for "private type invariants,"

At this point, I think that would be unwise.

> I could go either way.  Alternatively, we could keep the "Invariant
> =>" (or "Type_Invariant =>") syntax, but describe its semantics in
> terms of "Predicate =>"
> (or "Subtype_Predicate =>"), and do the checks at the same points as
> we do for subtype predicates, that might be a way of reducing the
> amount of "bulk"
> in the manual.

Hmm...  Maybe.

I'm inclined to keep invariants and predicates (OK, type invariants and subtype
predicates) separate, even though they have much in common.

> >> !wording
...
> I don't agree.  A private type invariant depends on having a
> well-defined default-initialized state, unless of course the
> programmer has eliminated the possibility of having
> default-initialized objects, by declaring the partial view with "(<>)"
> unknown discriminants.

Well, I can live with your view, but I'm not sure it's best.
Currently, SOME private types (with invariants expressed as comments) allow:

    X : Priv_Type;
    ...
    (later)
    X := Blah (...);

It's a language flaw that you can't tell from the private type decl whether it
has a meaningful default, and I'm not sure what to do about that.

> > Also, given the existence of loopholes that Randy likes to pound his
> > shoe on the table about, I think 'in' and 'in out' params ought to
> > be checked on the way in.
>
> This doesn't seem logically necessary, but in the interests of being
> able to define the semantics of private-type invariants in terms of
> subtype predicates, I could see the advantage.

I'm thinking purely from a practical point of view -- it's useful to catch
"sneaky" violations of the invariant that happen outside the package. I mean,
catch them as soon as you enter the package.

>...Adding them to all  operations with "in" parameters is clearly a
>dramatic increase in the number of checks required.
> Here is a case where I might make it implementation  defined, or
>perhaps some separate assertion policy,  which controls such things.
>Perhaps we need at this  point to add at least one more
>language-defined policy,  which would be "Minimal_Checks" vs.
>"Full_Checks"
> or something like that.

Not impl-def, please.  I could live with another policy.
I could also live with not checking 'in's -- then an impl can do it, with an
impl-def policy.  Or I could live with checking 'in's, and an impl can have the
other impl-def policy.  But if the policy in use is language defined, we
shouldn't be too loose.

...
> >>   The invariant check consists of the evaluation of each invariant
> >>   expression that applies to T, on each of the objects specified above.
> >>   If any of these evaluate to False, Ada.Assertions.Assertion_Error is
> >>   raised at the point of the object initialization, conversion, or call.
> >
> > I think "at the point ..." could be removed, without losing any info.
>
> It is important for a "call" to know exactly where the exception is
> raised.  For the other two I agree this is redundant.  We actually go
> on to say more about the "call" so perhaps there is no need to say "at
> the point"
> in this sentence, if we believe it is covered later for calls.

I think it's sufficiently covered by "Upon return..." above.

> >>   If a given call requires more than one evaluation of an invariant
> >
> > "call" --> "evaluation", or something less specific (because type
> > conv can do multiple ones; so can default init).
>
> How can type conversion require multiple ones?

What I said below, "or for...".

> >>   expression, either for multiple objects of a single type or for
> >>   multiple types with invariants, ...
> >
> > or for multiple invariants that apply to a single object of a single
> > type

Here.  A type T has its own invariant, plus other invariants from class-wide
things.  You didn't say these all get 'anded', you said they are multiple
invariants.  So T(X) involves checking all those.

This is just a minor wording issue.

...
> > This seems to contradict the prior rule about where the policy applies.
> > (I don't care too much what the exact rule is.)
>
> Can you elaborate on this contradiction?

I thought before you said the policy that matters is the one that applies to the
type decl.  But here you're saing it's the one that applies to some subprogram.

...
> > I don't buy it.  If an invariant fails on the way 'in', that's a
> > strong clue that some client is driving one of their trucks through a loophole.
> > That makes it EASIER to track down, whereas if we only check on the
> > way out, we will be fooled into thinking it's THIS package's fault.
>
> As suggested above, I am beginning to think we might need an
> additional checking policy, perhaps just to get a "some-but-not-all"
> policy identifier into the standard, even if the implementation
> defines some of the details of such an intermediate policy.
> Yes of course implementations can define as many policies as they
> want, but it would be nice to have a portable identifier for an
> "intermediate" level of checking, so you could move source code across
> Ada compilers without having to always change policy identifiers.

OK, I suppose.

We don't want TOO many policies.  Seems like the important ones are the
extremes.

...
> > Right.  The useful "intermediate point" is that part of your program
> > is more trusted (via testing, or whatever), and some other part is less trusted.
> > We DO support that distinction (I think).
>
> Now I am contradicting myself, thinking that there is a useful
> intermediate point.  The biggest difference would be eliminating the
> check on "in" parameters, given that there are *many* more calls with
> an "in" parameter than with in-out or out.  Also, checks on
> "out"/"in-out" parameters are easier to eliminate when included
> "inside" the body.  Checks on "in" parameters are essentially
> impossible to eliminate if the code is inside the body.

True.

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

From: Tucker Taft
Sent: Friday, June 25, 2010  6:01 PM

We agreed to change the name of the aspects to be "Type_Invariant" and
"Subtype_Predicate".
We abandoned any attempt to explain the
semantics of Type_Invariant in terms of
Subtype_Predicate, as it didn't seem to
help anyone (except perhaps me ;-).

More specific comments below.

...
> Yes.  Are you saying the above "Invariants can help..."
> is intended to contrast invariants with predicates?
> I didn't get that.  Still don't, really.

No, I meant no contrast.  Both Type_Invariants and Subtype_Predicates apply to
subprograms invented tomorrow.

>> But as far as the "contract" for a private type, I think the "type
>> invariant" is more directly relevant.
>
> More than what?

A Type_Invariant makes sense for a private type, and helps to express the
contract between the implementor and the client of the type. A Subtype_Predicate
doesn't have as much to do with a contract between the implementor and the
client of the *type*, but rather is used to create distinctions between
different (named) subsets of values of the same type, and allow a subprogram to
indicate which of the various named subsets it expects as a parameter.

>> If we always say "subtype predicate" and "type invariant"
>> (or even "private type invariant") in our discussion, hopefully we
>> can do a better job of keeping these things apart.
>> They really *aren't* the same thing, ...
>
> Well, they have something in common, and some differences, and if we
> try to emphasize the commonality, Randy will snap.  ;-) So I"ve pretty
> much given up on that.

So have I.

>
>> ...though I think
>> we could describe the semantics of "private type invariants"
>> in terms of "subtype predicates."
>
> Probably, but I'm not sure it helps, and anyway, Randy will snap.

I have given up on that.

...
>> Whether we want to eliminate type invariants and make a subtype
>> predicate, when applied to a partial view, have the special property
>> of applying to *only* the partial view "subtype" along the lines
>> specified for "private type invariants,"
>
> At this point, I think that would be unwise.

Yes, we have proceeded treating them as distinct features, one applies to
partial views, and one applies to any old named subtype.

>> I could go either way.  Alternatively, we could keep the "Invariant
>> =>" (or "Type_Invariant =>") syntax, but describe its semantics in
>> terms of "Predicate =>"
>> (or "Subtype_Predicate =>"), and do the checks at the same points as
>> we do for subtype predicates, that might be a way of reducing the
>> amount of "bulk"
>> in the manual.
>
> Hmm...  Maybe.

This approach didn't attract any interest.

...
> Well, I can live with your view, but I'm not sure it's best.
> Currently, SOME private types (with invariants expressed as comments)
> allow:
>
>     X : Priv_Type;
>     ...
>     (later)
>     X := Blah (...);
>
> It's a language flaw that you can't tell from the private type decl
> whether it has a meaningful default, and I'm not sure what to do about
> that.

That seems pretty error prone, to have a private type whose initial state is
undefined, but doesn't have unknown discriminants and so any use of the type
before a full-object assignment is potentially meaningless.  Doesn't sounds like
a very safe "abstraction."

...

I'll have to respond to other parts at a later time...

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

From: Bob Duff
Sent: Saturday, June 26, 2010  9:16 AM

Note that my message you are replying to was sent about a week ago -- it
apparently got stuck in arg@ada-auth.org for a while.

> We agreed to change the name of the aspects to be "Type_Invariant" and
> "Subtype_Predicate".

In order to uphold Ada's reputation for useless verbosity? Sigh.

I am strongly opposed to making either of these features harder to use,
including by making the names longer. I can't think of any example where the
extra "Type_" or "Subtype_" would enhance readability.  I guess the ARG was
talking along the lines of "people could be confused between these two
rather-similar features" (which is true!), and came up with an ineffectual
non-solution.

I'm happy to call them "type invariants" and "subtype predicates" in the RM, but
to require all programs to echo that all over the place seems ridiculous.

I hope we keep "Pre" and "Post, rather than "Precondition"
and "Postcondition" (or "Require" and "Ensure").
Or should it be "Subprogram_Precondition"?
Oops, that's not right, it has to be
"Callable_Entity_Precondition", to allow for entries.

> We abandoned any attempt to explain the semantics of Type_Invariant in
> terms of Subtype_Predicate, as it didn't seem to help anyone (except
> perhaps me ;-).

I don't think your viewpoint is wrong -- I just don't think it's for this
language, at this time.

[...snipping various points of agreement]

> > Well, I can live with your view, but I'm not sure it's best.
> > Currently, SOME private types (with invariants expressed as
> > comments) allow:
> >
> >     X : Priv_Type;
> >     ...
> >     (later)
> >     X := Blah (...);
> >
> > It's a language flaw that you can't tell from the private type decl
> > whether it has a meaningful default, and I'm not sure what to do
> > about that.
>
> That seems pretty error prone, to have a private type whose initial
> state is undefined, but doesn't have unknown discriminants and so any
> use of the type before a full-object assignment is potentially
> meaningless.  Doesn't sounds like a very safe "abstraction."

You're right, it's error prone and unsafe.  But that has nothing to do with type
invariants (and only a little to do with private types).

You need to think about unintended consequences.  If you make airplanes safer,
and that costs some money, so ticket prices go up, that's a good thing, right?
It saves lives!  No, it's wrong -- it will cause more people to drive cars more
often, so the number of unnecessary deaths and injuries will go up.

Suppose I need/want to do the above thing (see "(later)" above), You are
proposing that I'm not allowed to do that if I use an invariant.  So I have two
choices:

    1. Express my invariant in a comment, the old-fashioned way.
       That's even less safe.

    2. Provide a useless init on X.  Again, less safe.

    3. Provide a bogus default value for Priv_Type.  (The extreme
       of this strategy is Jave, where EVERY variable gets a
       possibly-bogus initial value.  I know you don't like that
       rule -- so why require it for the new types-with-invariants
       feature.)

We can live with these problems, but if you think they make the language
net-safer, you're wrong, IMHO.

Note that 2 and 3 introduce inefficiency, as well as unsafety.
2 and 3 also probably defeat useful compiler warnings, which currently
(partially) address the problems you're worried about.

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

From: Bob Duff
Sent: Saturday, June 26, 2010  9:16 AM

> >     X : Priv_Type;
> >     ...
> >     (later)
> >     X := Blah (...);

Actually, thinking about this a little more, it seems even worse than what I
said before.  In particular, for private types whose full type is scalar.
Here's some code that comes from CodePeer's arbitrary-range arithmetic package,
somewhat simplified:

    package Bignums is
        type Big_Int is private; -- no default initial value
        ...
    private
        type Big_Int is range ...;
    end Bignums;

Big_Int is an index into some sort of table (I'm oversimplifying!).

You're saying (I think) that if Big_Int has an invariant, then:

    X : Big_Int;
    ...
    X := To_Big_Int (1);

It is implementation dependent whether or not this raises Assertion_Failure.  X
is initialized to some arbitrary stack junk, so the invariant will fail if that
junk happens to represent a "bad" value.

That seems like a totally unacceptable non-portability.

Without an invariant, the above is completely correct and portable.  Surely we
don't want "adding an invariant" to sprinkle arbitrary and impl-dep exceptions
all over the place!

We could make it illegal for any type with an invariant to lack some sort of
default (thus forbidding scalars), but that seems like overkill, and doesn't
even fully solve the problem.  I could live with it, though -- it's far better
than applying invariants to arbitrary stack junk!

Note that when I wrote the Big_Int code some years ago, I tried to use a default
value, which in full-checking mode would raise an exception on use of an
uninitialized Big_Int. This turned out to cause an intolerable amount of cruft
inside the package.  It might not seem like a big deal to wrap the thing in a
record, with a default for the component, but it meant every operation has to
grab the components out, and then rewrap using an aggregate. That hugely damaged
the readability of the code, so I gave up.  We're talking about thousands of
lines of code in the package (including children).

I suggest you do an experiment:

        type Big_Int(<>) is private;
                    ^^^^
and see how many errors you get in clients.  (I don't know how to build
CodePeer, and I don't want to learn how, so I'm not going to do the experiment.)

Note that I advocate checking invariants on 'in' parameters (on the way in).  I
think the above discussion is another argument in favor of that view (if you are
now convinced that checking invariants on uninit vars is a bad idea).

Summary: My first choice is as I said before -- check invariants on object decls
if the type has some default init, or the object is explicitly initialized,
otherwise don't check.  My second choice is to forbid invariants on a type that
has no default init and no (<>) discrim.  The third choice (which seems
unaccepable) is to check on all object decls.

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

From: Tucker Taft
Sent: Monday, June 28, 2010  9:09 AM

Another possibility might be to allow
the specification of a default initial
value for a scalar type, and disallow
a type_invariant unless such a default
is specified, for a private type completed by a scalar type.  That would provide
the most safety, I would think.

[This idea eventually led to the proposal in AI05-0228-1. See that
AI for more e-mail on this topic. - Editor.]

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

From: Bob Duff
Sent: Monday, July 5, 2010  2:18 PM

> Another possibility might be to allow
> the specification of a default initial value for a scalar type, and
> disallow a type_invariant unless such a default is specified, for a
> private type completed by a scalar type.  That would provide the most
> safety, I would think.

I could live with that.  I'm not entirely convinced that it adds a whole lot of
safety, but it's certainly preferable to my "third (unacceptable) choice" below.

If we do that, we should allow a default for access types, for uniformity,
right?

I suppose if you say:

    subtype T is Integer range 1..10 := 11;

a compiler should warn if an object uses that default (and NOT on the default
itself, which is deliberately intended to prevent uninit objects).

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


Questions? Ask the ACAA Technical Agent