!standard 11.5 (00) 10-08-11 AI05-0146-1/05 !standard 11.4.1 (10) !class amendment 09-02-15 !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 To augment the basic "assert" pragma capability of Ada 2005, we propose constructs for specifying invariants for types. The semantics for these constructs are defined in terms of the Assertion_Error exception used by the Assert pragma and the Assertion_Policy configuration pragma. !problem A number of programming paradigms include the heavy use of invariants associated with types or modules (i.e. packages). Having a basic standardized "Assert" pragma supports this approach to some degree, but generally requires that the Assert pragmas actually be inserted inside the bodies of the associated code. It would be much more appropriate if these invariants appeared on the specification of the types and packages rather than buried in the body, as it really represents part of the contract. In particular, one wants any implementation of a given package spec to conform to all of invariants specified, in the same way one wants any implementation of a package to conform to the constraints of the parameter and result subtypes of the visible subprograms of the package. Note that type invariants are not the same thing as constraints, as invariants apply to all values of a type, while constraints are generally used to identify a subset of the values of a type. Invariants are only meaningful on private types, where there is a clear boundary (the enclosing package) that separates where the invariant applies (outside) and where it need not be satisfied (inside). In some ways, an invariant is more like the range of values specified when declaring a new integer type, as opposed to the constraint specified when defining an integer subtype. The specified range of an integer type can be violated (to some degree) in the middle of an arithmetic computation, but must be satisfied by the time the value is stored back into an object of the type. Invariants can help to more accurately define the "contract" between the user and implementor of a package, and thereby to catch errors in usage or implementation earlier in the development cycle. They also can provide valuable documentation of the intended semantics of an abstraction. !proposal We propose to allow the specification of an Invariant "aspect" of a type, as well as an Invariant'Class aspect of a tagged type. These aspects are specified using a construct of the following form: package Q is type T(...) is private with Invariant => Is_Valid(T); type T2(...) is abstract tagged private with Invariant'Class => Is_Valid(T2); function Is_Valid(X : T) return Boolean; function Is_Valid(X2 : T2) return Boolean is abstract; end Q; 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: Type_Invariant This aspect shall be specified by an expression, called an *invariant expression*. The expected type for the expression is any boolean type. 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*. The expected type for the expression is any boolean type. Type_Invariant'Class may be specified on a private_type_declaration or a private_extension_declaration. Name Resolution [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 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; !ACATS test !appendix From: Tucker Taft Sent: Sunday, February 15, 2009 4:30 PM Here is a resurrection of AI95-00375 on type and package invariants. We discussed the type invariants at AdaCore. I left in the Package_Invariant because it seemed simple and useful. [This is version /01 of the AI - ED.] **************************************************************** From: Bob Duff Sent: Tuesday, February 24, 2009 10:25 AM [Find the message that this is replying to in AI05-0145-1.] > type Set is interface > with > Invariant'Class => > (Is_Empty(X)) = (Count(X) = 0); I think invariants should apply to subtypes, not just types. I think they are like constraints, and at least for scalars, can be checked in the same places. **************************************************************** From: Gary Dismukes Sent: Thursday, February 26, 2009 12:09 AM Randy brought up that point at the meeting and he has an action item to make a specific proposal along those lines. **************************************************************** From: Robert Dewar Sent: Thursday, February 26, 2009 12:09 AM I agree with this, BTW, I find Tuck's syntax suggestion basically nice, and think that pre/post conditions are important enough to warrant syntax additions. I do think that postconditions in the body are useful, and so would keep the pragmas, certainly in GNAT anyway. It is true that preconditions in the body are just assertions, so they are there just for symmetry, but postconditions in the body are useful in that they come up front, which is the right position, and they block all exits (which would be tedious to do manually with assertions). I also think it is good to be able to control pre/post conditions separately from normal assertions. **************************************************************** From: Alan Burns Sent: Thursday, February 26, 2009 7:21 AM > I think invariants should apply to subtypes, not just types. > I think they are like constraints, and at least for scalars, can be > checked in the same places. I've not followed the recent discussion on invariants, but am not sure how you deal with the usual invariant that is true most of the time but not during atomic updates. Or a loop invariant that is true at the end of each iteration but not during an iteration. pre and post conditions are specific as to when they should evaluate to true, but invariants cover a region (but not the whole program) **************************************************************** From: Bob Duff Sent: Thursday, February 26, 2009 7:40 AM > I've not followed the recent discussion on invariants, but am not sure > how you deal with the usual invariant that is true most of the time > but not during atomic updates. I'm not sure, either. That issue deserves some careful thought. Perhaps scalars should be different from records? >... Or a loop invariant that is > true at the end of each iteration but not during an iteration. Isn't the loop-invariant case just a "pragma Assert" written at some point within the loop (e.g. at the end of each iteration)? I don't see any need for a new feature for loop invariants. The invariants I'm thinking of should apply to [sub]types. Maybe also to packages. > pre and post conditions are specific as to when they should evaluate > to true, but invariants cover a region (but not the whole program) **************************************************************** From: Tucker Taft Sent: Thursday, February 26, 2009 9:18 AM > I think invariants should apply to subtypes, not just types. > I think they are like constraints, and at least for scalars, can be > checked in the same places. We discussed this, and concluded that invariants and user-defined constraints are both useful, but they are not the same thing. Invariants are generally imposed on the implementation of an abstraction, and translate into *postconditions* on all operations that return values to the "outside" world. Constraints are often used as *preconditions* on values being passed *in* to a subprogram, and generally are required to be satisfied at all points, whereas invariants are often false in the middle of a primitive operation. So we concluded, I believe, that invariants are associated with an abstraction, and hence a type, or perhaps a package, while constraints define a subset of the values of a type, and hence are appropriately associated with a subtype. **************************************************************** From: Bob Duff Sent: Thursday, February 26, 2009 7:57 AM Question: In an invariant, does one refer to the "current instance" in the usual way, by naming the [sub]type? As in: type My_Int is range 0..1_000_000; subtype My_Even_Int is My_Int with Invariant => (My_Even_Int mod 2) = 0; > I've not followed the recent discussion on invariants, but am not sure > how you deal with the usual invariant that is true most of the time > but not during atomic updates. For scalars, one can use 'Base as always. E.g. if you have X: in out My_Int, and you want to temporarily set it to a negative number, you do something like: Temp : My_Int'Base := X; Temp := Temp - 10; -- might be negative Temp := abs Temp; X := Temp; -- OK, Temp is now nonnegative Similarly, My_Even_Int'Base would be a subtype that is NOT restricted to even numbers. Not sure how this can work for records. By the way, I think the "in" operator should take invariants into account. E.g.: if Blah in My_Even_Int then ... would be True iff Blah is an even number in the 0..1_000_000 range. **************************************************************** From: Edmond Schonberg Sent: Thursday, February 26, 2009 12:50 PM > Question: In an invariant, does one refer to the "current instance" > in the > usual way, by naming the [sub]type? As in: > > type My_Int is range 0..1_000_000; > > subtype My_Even_Int is My_Int with > Invariant => (My_Even_Int mod 2) = 0; Invariants are intended for private types only. Otherwise the invariant may have to be verified on assignment or any operation that would visibly modify a value of the type outside of the defining package. This is impractical and not particularly useful (we have constraints for this, and invariants are NOT constraints). By limiting the invariant to a private type, the check is limited to the visible primitive operations of the type (what happens otherwise in the body stays in the body). **************************************************************** From: Stephen Michell Sent: Thursday, February 26, 2009 1:04 PM In general, I like Tucker's proposal. On the issue of invariance, Alan is completely correct. Invariance for, say, the relationship between components or between state variables in a class only allies when they are no threads executing subprograms that may change that state. You can make invariance work for every execution step, but in general that is going to require auxillary variables and a lot of very hard work. We need to develop syntax to express when invariance applies, or possibly when it does not apply, such as loop invariants only apply at the exit condition and state invariants only apply at the precondition and postcondition points of every subprogram that can see the state. As part of this effort, we need a syntax for auxillary variables, declaration, assignment and formal relationships. **************************************************************** From: Randy Brukardt Sent: Thursday, February 26, 2009 1:49 PM > I think invariants should apply to subtypes, not just types. > I think they are like constraints, and at least for scalars, can be > checked in the same places. We talked about that at my insistence. We decided that invariants and constraints are different things that solve different problems. (Which is what I have been saying all along.) Invariants apply to all values of a type, and can be inherited. Constraints apply to particular views (not necessarily an object). Constraints are checked at the points that language currently defines (subtype conversion); invariants are checked only when crossing the boundary of the defining package. I was tasked in writing up a proposal for user-defined constraints (resurrecting my old proposal on that topic, but now using syntax and legality rules). If we can have only one of these, I think user-defined constraints are far more useful. But I can see uses for both. **************************************************************** From: Jean-Pierre Rosen Sent: Friday, February 27, 2009 12:58 AM > By limiting the invariant to > a private type, the check is limited to the visible primitive > operations of the type (what happens otherwise in the body stays in the body). I understand limited to visible operations, but why primitives? **************************************************************** From: Edmond Schonberg Sent: Friday, February 27, 2009 2:57 PM No reason, written in haste. Of course visible classwide operations are included. **************************************************************** From: Jean-Pierre Rosen Sent: Saturday, February 28, 2009 5:11 AM Actually, I was thinking of operations that are not primitive because they are declared, f.e., in a subpackage. **************************************************************** From: Yannick Moy Sent: Monday, August 31, 2009 11:01 AM I am forwarding here the beginning of a conversation with Ed Schonberg about type invariants (AI05-0146), to be continued on this list. Yannick Moy wrote: > I have the feeling that the following rule stated for AI 05-0146 does > not make it easy to check a type invariant: > >> > Invariants are only meaningful on private types, where there is a >> > clear boundary (the enclosing package) that separates where the >> > invariant applies (outside) and where it need not be satisfied (inside). > > The proposal only requires that (in) out parameters of primitive > operations are checked, which does not seem sufficient to me. I also > read the thread, and you seemed to agree with the proposal: > >> > Invariants are intended for private types only. Otherwise the >> > invariant may have to be verified on assignment or any operation >> > that would visibly modify a value of the type outside of the >> > defining package. This is impractical and not particularly useful >> > (we have constraints for this, and invariants are NOT constraints). >> > By limiting the invariant to a private type, the check is limited >> > to the visible primitive operations of the type (what happens otherwise in the body stays in the body). > > I do not see how this prevents violating the invariant of an object of > that type different from the (in) out parameters, e.g., through a > pointer. I have written a small example (attached) to explain my point. > Do you agree there is a problem here, or did I miss something? Ed Schonberg wrote: > I agree that the proposal is not complete, and your neat example shows > how to poke holes in it. I'm not sure that there is a formulation > that is reasonably cheap to implement that would catch this example. > Throughout the discussion there is of course a pragmatic thread: we > cannot require implementations to do data-flow. Do you have a model > for verification of invariants that would catch this case? Recall that > this would have to be only for external calls, i.e. calls to Bad from > outside of package A. I suspect that once you introduce indirection > like this it becomes undecidable, and you don't want to put the check > within the procedure body, because it may be an intended internal > violation of the invariant. Yannick Moy wrote: >> I agree that the proposal is not complete, and your neat example >> shows >> > how to poke holes in it. I'm not sure that there is a formulation >> > that is reasonably cheap to implement that would catch this example. > > I discussed it with Cyrille, and he also pointed to me that it is > probably impractical to have an invariant that extends to "all objects > of that type" at any given point in the program. In that case, an > invariant is more like a shorthand for the equivalent set of pre- and > postconditions, no more, and I think it should be emphasized in the > wording of the problem section of the AI. In particular, the current > wording is wrong, if we keep this notion of "never guaranteed true for > all objects" invariant. > >> > Throughout the discussion there is of course a pragmatic thread: we >> > cannot require implementations to do data-flow. Do you have a model >> > for verification of invariants that would catch this case? > > Spec# ensures that the invariant > obj.inv = "true" ==> obj.Inv() > is always true, where "inv" is a hidden field of every object and "Inv" > is the invariant of this particular object, by enforcing a detailed > (and > heavy) coding practice, in which an object must be "opened" explicitly > before it is modified. > > JML does not ensure anything: invariants in JML are really just > shorthands for pre- and postconditions. > > In our case, I think a very simple restriction would guarantee that > the invariant is really valid for all objects of that type, outside of > the part of the call-graph dominated by a procedure of package A > (which may still include code outside of A): forbid modification of an > object of that type that is not an (in) out parameter! > >> > Recall that this >> > would have to be only for external calls, i.e. calls to Bad from >> > outside of package A. I suspect that once you introduce >> > indirection like this it becomes undecidable, and you don't want to >> > put the check within the procedure body, because it may be an >> > intended internal violation of the invariant. > > I agree that modification through an access type makes any static > verification of the invariant undecidable. So either we forbid it, or > we loosen the interpretation of 'invariant' (or we have 2 different > kinds of invariants, kind-of weak and strong invariants?) **************************************************************** From: Yannick Moy Sent: Monday, August 31, 2009 1:51 PM Attaching the example mentioned in the previous mail. package A is type T is private; -- with Invariant => Ok(T); function Ok (This : in T) return Boolean; procedure Bad (This : in out T); private type T is record J : Integer; Next : access T; end record; end A; package body A is function Ok (This : in T) return Boolean is begin return This.J >= 0; end Ok; procedure Bad (This : in out T) is begin This.Next.J := -1; end Bad; end A; **************************************************************** From: Steve Baird Sent: Monday, August 31, 2009 3:32 PM > I agree that modification through an access type makes any static > verification of the invariant undecidable. So either we forbid it, or > we loosen the interpretation of 'invariant' (or we have 2 different > kinds of invariants, kind-of weak and strong invariants?) And access types are just one way of running into this problem, right? A routine which updates a global variable or a subcomponent of a parameter might result in similar problems without involving access types. Perhaps the name "Invariant" suggests something stronger than what this mechanism implements, but this mechanism still seems like it might save a lot of duplicated pre- and post-conditions. If we want to keep the mechanism but change the name, someone will have to come up with a better name than Weak_Invariant or I_Sure_Hope_This_Is_Usually_True . **************************************************************** From: Bob Duff Sent: Monday, August 31, 2009 5:21 PM > In our case, I think a very simple restriction would guarantee that > the invariant is really valid for all objects of that type, outside of > the part of the call-graph dominated by a procedure of package A > (which may still include code outside of A): forbid modification of an > object of that type that is not an (in) out parameter! Can you explain that a bit more? I'm not sure why it works. > I agree that modification through an access type makes any static > verification of the invariant undecidable. So either we forbid it, or > we loosen the interpretation of 'invariant'... In Eiffel, an invariant is just a short-hand for a bunch of pre- and postconditions. Eiffel requires checking the invariant (at run time) on both entry and exit of each method. The reason is basically the same as in your example -- pointers. It's worse in Eiffel, because pointers are more ubiquitous. In an Ada context, if we follow the Eiffel ideas, we would check the invariant for an 'in' parameter on entry to a procedure. But that's uncomfortable. It is the responsibility (conceptually) of the package itself to make sure the invariant is always true (for some definition of "always" ;-)). But preconditions are the responsibility of the caller. How is the caller supposed to ensure an invariant? It can't. >... (or we have 2 different kinds > of invariants, kind-of weak and strong invariants?) I've thought about that a little. I wonder if it makes sense to let the compiler decide which are weak and strong (as opposed to letting the programmer label them)? It sure would be nice if at least _some_ invariants are statically provable. It seems hopeless to prove an invariant, unless you can somehow know that checking the invariant on exit from a subprogram (for '[in] out' params and function results) implies that the invariant _must_ be true on entry (for 'in [out]' params). If you know that, you have some hope of doing an inductive proof. Do we need 'globals' annotations, in the SPARK sense? **************************************************************** From: Randy Brukardt Sent: Monday, August 31, 2009 8:18 PM > > In our case, I think a very simple restriction would guarantee that > > the invariant is really valid for all objects of that type, outside > > of the part of the call-graph dominated by a procedure of package A > > (which may still include code outside of A): forbid modification of > > an object of that type that is not an (in) out parameter! > > Can you explain that a bit more? I'm not sure why it works. I don't think it does work, because the problem is modification of a logical portion of the object that is not actually a part (in the technical sense) of the object (that is, something that is accessed by a pointer rather than being a (sub)component of the object). OTOH, modifications of logical parts of "in" objects that have invariants via pointers can be detected, and one could imagine having a warning about doing so damaging the meaning of invariant. But it would be pretty nasty to make such code illegal (especially as you can't tell for sure if pointer points at a logical part of the current object, or at some other object). ... > It sure would be nice if at least _some_ invariants are statically > provable. > It seems hopeless to prove an invariant, unless you can somehow know > that checking the invariant on exit from a subprogram (for '[in] out' > params and function results) implies that the invariant _must_ be true > on entry (for 'in [out]' params). If you know that, you have some > hope of doing an inductive proof. > > Do we need 'globals' annotations, in the SPARK sense? Yes, absolutely. Without them, you can't do anything much statically with preconditions/postconditions either, because the compiler cannot know whether there are any side-effects in the predicate functions (there shouldn't be, but if there are, it would be evil for a compiler to *introduces* erroneousness because it removes/changes side-effects in preconditions. Adding preconditions ought never make the program less safe!) The same is true for invariants. Tucker and I had discussed this in the context of some previous discussion, and we had gotten as far as trying to sketch out the form of such annotations. But we didn't quite agree on the details, and we agreed to put it off until later. (I believe this was just before the Brest meeting.) I suppose "later" is rapidly approaching... Note that I'd been trying to solve this problem with rules about purity, but using globals annotations for that seems to work even better, being far more flexible. They also (appear) easy to enforce, and since they're optional, there shouldn't be any problem with enforcing them (if you can't write an enforcable globals annotation, then don't write one at all). **************************************************************** From: Robert C. Leif Sent: Tuesday, September 1, 2009 9:28 AM I have three questions: 1. Could some of the invariants be checked at compile time and not need to be checked at run time? 2. Could the units of a numerical value be part of the invariants and be checked as precondition and the units of returned values or out values be checked as a post-condition? 3. Could item 2 be limited to compile time checking? It should be noted that starting with Bill Whitaker some of us have been waiting for an elegant, efficient solution in Ada to the units problem. **************************************************************** From: Yannick Moy Sent: Tuesday, September 1, 2009 1:47 AM >> In our case, I think a very simple restriction would guarantee that >> the invariant is really valid for all objects of that type, outside >> of the part of the call-graph dominated by a procedure of package A >> (which may still include code outside of A): forbid modification of >> an object of that type that is not an (in) out parameter! > > Can you explain that a bit more? I'm not sure why it works. There are 2 sides to this, as the comment from Randy Brukardt shows: 1) do not allow the invariant to mention anything beyond the value or the direct fields in the private type; 2) only allow to violate the invariant of those objects which invariant will be checked on subprogram exit, which are the [in] out parameters. This is quite restrictive, as you cannot mention a value through an access type in the invariant, even if it is through a field of the private type. > In an Ada context, if we follow the Eiffel ideas, we would check the > invariant for an 'in' parameter on entry to a procedure. But we would not even be better off wrt this notion of strong invariants. >> ... (or we have 2 different kinds >> of invariants, kind-of weak and strong invariants?) > > I've thought about that a little. I wonder if it makes sense to let > the compiler decide which are weak and strong (as opposed to letting > the programmer label them)? I guess that depends on what you allow in the invariant. In general, it would not be feasible to decide whether an external call modifies an object by just looking at the declarations. But if you stick to rule (1) above, where an invariant only mentions value or direct fields of the private type, then only the subprograms in the current package can modify the value of the invariant. > It sure would be nice if at least _some_ invariants are statically provable. > It seems hopeless to prove an invariant, unless you can somehow know > that checking the invariant on exit from a subprogram (for '[in] out' > params and function results) implies that the invariant _must_ be true > on entry (for 'in [out]' params). If you know that, you have some > hope of doing an inductive proof. There are 2 parts in this verification: - checking that every subprogram that could violate the strong invariant does ensure it holds on exit. This is hard, usually needing some interaction of a user with provers. Better left as dynamic checks in general. - checking that outside of the parts of the call-graph dominated by a call which could violate the strong invariant, the strong invariant holds. This should be very easy, by restricting the kind of invariants as in rules (1) and (2) above. > Do we need 'globals' annotations, in the SPARK sense? Not for strong invariants I think, but a common description of effects would be great for any modular analysis of Ada, yes! Except we need more that SPARK, to describe "any field Next reachable from this parameter" and other locations on the heap. **************************************************************** From: Yannick Moy Sent: Tuesday, September 1, 2009 4:17 AM > I don't think it does work, because the problem is modification of a > logical part of the object that is not actually a part of the object > (that is, something that is accessed by a pointer rather than being a > (sub)component of the object). You are right, I answered to this too when I answered to Bob. The key to strong invariant is maintaining a kind of 'ownership' between an object and the parts of state that are mentioned in its invariant. > OTOH, modifications of logical parts of "in" objects that have > invariants via pointers can be detected, and one could imagine having > a warning about doing so damaging the meaning of invariant. But it > would be pretty nasty to make such code illegal (especially as you > can't tell for sure if pointer points at a logical part of the current object, or at some other object). I am not sure if we want to go into such complexity. If the invariant is allowed to talk about things that are pointed-to, then it is probably simpler to just stick to weak invariants, that are only true when they were just checked. > Tucker and I had discussed this in the context of some previous > discussion, and we had gotten as far as trying to sketch out the form > of such annotations. But we didn't quite agree on the details, and we > agreed to put it off until later. (I believe this was just before the > Brest meeting.) I suppose "later" is rapidly approaching... Do you have a pointer to these discussions? I would be very interested in reading your sketch of annotations. > Note that I'd been trying to solve this problem with rules about > purity, but using globals annotations for that seems to work even > better, being far more flexible. They also (appear) easy to enforce, > and since they're optional, there shouldn't be any problem with > enforcing them (if you can't write an enforcable globals annotation, then > don't write one at all). Great! I'd be happy to be part of that discussion too. **************************************************************** From: Randy Brukardt Sent: Tuesday, September 1, 2009 1:36 PM > It should be noted that starting with Bill Whitaker some of us have > been waiting for an elegant, efficient solution in Ada to the units > problem. Don't hold your breath. Lots of very smart people (including Tucker) have tried to address the units problem, and no "elegant, efficient" solution (that is correct as well) has been found. Solutions that work either require runtime checks (meaning not so efficient) or generating an extremely complex set of type definitions (efficient, but not elegant). The best solution I've seen uses a program to generate the nest of type and operator definitions needed for an efficient solution. Part of the problem is that the interelationships between units are not fixed; there are lots of different combinations. So it isn't practical to include those relationships in a programming language. **************************************************************** From: Randy Brukardt Sent: Tuesday, September 1, 2009 1:42 PM > > Tucker and I had discussed this in the context of some previous > > discussion, and we had gotten as far as trying to sketch out the > > form of such annotations. But we didn't quite agree on the details, > > and we agreed to put it off until later. (I believe this was just > > before the Brest meeting.) I suppose "later" is rapidly approaching... > > Do you have a pointer to these discussions? I would be very interested > in reading your sketch of annotations. It was just in private e-mail; it never got far enough along for public consumption. I was stuck on finding a reasonable form for listing specific objects accessed. It seems to be a some sort of list, but the resolution rules for that list are hard to explain (any object plus keywords null and private?). > > Note that I'd been trying to solve this problem with rules about > > purity, but using globals annotations for that seems to work even > > better, being far more flexible. They also (appear) easy to enforce, > > and since they're optional, there shouldn't be any problem with > > enforcing them (if you can't write an enforcable globals > annotation, then don't write one at all). > > Great! I'd be happy to be part of that discussion too. I'll try to make sure something is proposed well before the November meeting (it has to be, or it can't be included in Amendment 2). Once we have an outline, we can then throw brickbats, I mean discuss the details. **************************************************************** 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. ****************************************************************