!standard 7.3.2(0) 11-09-27 AI05-0250-1/03 !standard 3.9.2(20.2/2) !class Amendment 11-06-15 !status Amendment 2012 11-07-27 !status ARG Approved 10-0-1 11-06-26 !status work item 11-06-15 !status received 11-06-15 !priority Low !difficulty Easy !subject Thoughts on type invariants !summary Specific Invariants can be hidden (given on the full declaration of a private type). The places at which invariant checks are performed are clarified. !question 1) It would be useful to have the option of specifying the Invariant aspect with the full declaration of the type instead of only at the declaration of the partial view of the type. It's bizarre to have to make the invariant visible to all clients; if often only relevant to the implementation of the type. 2) It would be useful if some mechanism existed for statically enforcing a requirement that an invariant expression must not have side effects or, more generally, must be "well behaved" (definition details TBD, but this might include prohibitions on reading variables and/or on propagating exceptions). 3) It would be useful if the language made a distinction between "internal" calls (where the caller is already inside the implementation of the type in question) and "external" calls. No runtime invariant checking should be performed for an "internal" call. !proposal (See wording.) !wording Modify 3.9.4(20.4/3): otherwise, the action is the same as the action for the corresponding operation of the parent type or progenitor type from which the operation was inherited {except that additional invariant checks (see 7.3.2) and class-wide postcondition checks (see 6.1.1) may apply)}. If there is more than one such corresponding operation, the action is that for the operation that is not a null procedure, if any; otherwise, the action is that of an arbitrary one of the operations. In 7.3.2(2/3), replace Type_Invariant may be specified on a private_type_declaration or a private_extension_declaration. with Type_Invariant may be specified on a private_type_declaration, on a private_extension_declaration, or on a full_type_declaration that declares the completion of a private type or private extension. Add an AARM Note after 7.3.2(3/3): Reason: A class-wide type invariant cannot be hidden in the private part, as the creator of an extension needs to know about it in order to conform to it in any new or overriding operations. On the other hand, a specific type invariant is not inherited, so that no operation outside of the original package needs to conform to it; thus there is no need for it to be visible. Add before 7.3.2(7/3): [Redundant: If the Type_Invariant aspect is specified for a type T, then the invariant expression applies to T.] Replace 7.3.2(9-16/3) by * After successful default initialization of an object of type T, the check is performed on the new object; * After successful conversion to type T, the check is performed on the result of the conversion; * After assigning to a view conversion, outside the immediate scope of T, that converts from T or one or more record extensions (and no private extensions) of T to an ancestor of type T, a check is performed on the part of the object that is of type T; similarly, for passing a view conversion as an OUT or IN OUT parameter outside the immediate scope of T, this check is performed upon successful return; * After a successful call on the Read or Input stream attribute of the type T, the check is performed on the object initialized by the stream attribute; * Upon successful return from a call on any subprogram or entry that: - is explicitly declared within the immediate scope of type T (or by an instance of a generic unit, and the generic is 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, and - has a result with a part of type T, or one or more IN OUT or OUT parameters with a part of type T, or an access to variable parameter whose designated type has a part of type T. the check is performed on each such part of type T. Modify 7.3.2(17/3): 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, 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 {are performed in an arbitrary order}[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. {Invariant checks, any postcondition check, and any constraint checks associated with by-copy in out or out parameters are performed in an arbitrary order.} [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.] Replace 7.3.2(18/3) by: 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. Add after 7.3.2(19/3): Note: A call of a primitive subprogram of type NT that is inherited from type T needs to satisfy the specific invariants of both the types NT and T. A call of a primitive subprogram of type NT that is overridden for type NT needs to satisfy only the specific invariants of type NT. !discussion Item (1) is addressed in the wording proposal above. For item (2), it seems premature to define such restrictions. Implementations can define their own; and we'll revisit this next time. For item (3), the language *does* make such a distinction, but it makes it between subprograms, not calls. Subprograms declared in the visible part are external, others are internal. This also seems right: A called subprogram doesn't know who is its caller, so if it is externally callable, it needs to ensure the invariant is true on return. This seems right, so no change is needed now. The change to 7.3.2(17/3) is to use the "arbitrary order" wording used by the rest of the standard. The remaining changes are to clarify when checks are and are not performed, and to fix holes caused by view conversions. !corrigendum 3.9.2(20.2/2) @drepl Force a conflict; the real text is found in the conflict file. @dby Nothing interesting. !corrigendum 7.3.2(0) @dinsc Force a conflict; the real text is found in the conflict file. !ACATS test Create ACATS C-Tests to ensure that the invariant checks are made in all of the defined cases. !ASIS No ASIS impact (beyond the original AI). !appendix From: Steve Baird Sent: Wednesday, June 15, 2011 4:24 PM An AdaCore customer has identified three issues with Ada 2012's type invariants. I'm passing these along so that the ARG can decide for each whether a) some action is needed for Ada 2012; or b) some action is needed, but not for Ada 2012; or c) no action is needed. ==== 1) It would be useful to have the option of specifying the Invariant aspect with the full declaration of the type instead of only at the declaration of the partial view of the type. If what the user really wants is package Pkg is type Stack is private; private type Stack is record Max, Current : Index := 0; ...; end record with Invariant => Stack.Current <= Stack.Max; end Pkg; , it is annoying to have to write package Pkg is type Stack is private with Invariant => Is_Valid (T); function Is_Valid (X : Stack) return Boolean; private type Stack is record Max, Current : Index:= 0; ...; end record; function Is_Valid (X : T) return Boolean is (X.Current <= X.Max); end Pkg; , thereby adding an unwanted visible operation (Is_Valid) to the interface. If a user chooses to think of the invariant as an implementation detail, not part of the public interface (and not part of a contract which clients need to be aware of), then that user doesn't want to see any mention of the invariant in the visible part. Introducing the Is_Valid function (albeit a function whose completion is an expression_function) may also have interactions with issue #2 (below). ==== 2) It would be useful if some mechanism existed for statically enforcing a requirement that an invariant expression must not have side effects or, more generally, must be "well behaved" (definition details TBD, but this might include prohibitions on reading variables and/or on propagating exceptions). A new language-defined restriction which only allows "well behaved" invariant expressions could address this issue. Concern was also expressed about the particular case of an invariant expression whose evaluation leads to infinite recursion because the expression itself contains some construct whose evaluation requires evaluation of the invariant expression (e.g., due to a type conversion or to a call to a function with an out-mode parameter). Hopefully the as-yet-uninvented restriction would catch this case. ==== 3) It would be useful if the language made a distinction between "internal" calls (where the caller is already inside the implementation of the type in question) and "external" calls. No runtime invariant checking should be performed for an "internal" call. The concern here is correctness, not performance. Inside the implementation, it is perfectly reasonable to (temporarily) violate a type's invariant. An invariant check performed while "the hood is up" can be a problem. One (partial) workaround is to implement each exported operation Foo as a rename of a non-exported Foo_Implementation subprogram. "Internal" callers who want to call Foo then call Foo_Implementation instead. Or the private type in question could be implemented as a derived type with invariant-breaking operations performed using the non-exported parent type and then only converting to the exported type when the invariant has been restored. Either of these approaches is cumbersome. ===== My own opinions: #1 I can see the argument for this. I would not be opposed to allowing the Invariant spec to be supplied as part of either the private type declaration (as it is today) or the completion. #2 Defining a new restriction for folks who want more restrictions on invariant expressions seems reasonable, but lots of details TBD. #3 The AI currently says 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. There are good reasons for this rule and I think messing with it would lead to problems. **************************************************************** From: Randy Brukardt Sent: Wednesday, June 15, 2011 5:00 PM ... > #2 Defining a new restriction for folks who want > more restrictions on invariant expressions > seems reasonable, but lots of details TBD. Such a restriction makes perfect sense, and should apply to all contracts (that is, preconditions, postconditions, and subtype predicates) but in the past when I've proposed such things I've not gotten any traction. I suspect that this is an area where an implementer needs to take the lead (I definitely will do something on this like in Janus/Ada should I ever get to implementing contracts, but obviously something AdaCore does will have a lot more impact). **************************************************************** From: Edmond Schonberg Sent: Wednesday, June 15, 2011 5:10 PM > ... >> #2 Defining a new restriction for folks who want >> more restrictions on invariant expressions >> seems reasonable, but lots of details TBD. > > Such a restriction makes perfect sense, and should apply to all > contracts (that is, preconditions, postconditions, and subtype > predicates) but in the past when I've proposed such things I've not > gotten any traction. I suspect that this is an area where an > implementer needs to take the lead (I definitely will do something on > this like in Janus/Ada should I ever get to implementing contracts, > but obviously something AdaCore does will have a lot more impact). There have been several user suggestions along those lines, so we will definitely introduce such a restriction. Implementation seems straightforward if the definition is tight enough. Should there be a pragma (sorry, an aspect) that asserts that the body of a function satisfies this restriction? They seem to go together. **************************************************************** From: Randy Brukardt Sent: Wednesday, June 15, 2011 6:17 PM > > ... > >> #2 Defining a new restriction for folks who want > >> more restrictions on invariant expressions > >> seems reasonable, but lots of details TBD. > > > > Such a restriction makes perfect sense, and should apply to all > > contracts (that is, preconditions, postconditions, and subtype > > predicates) but in the past when I've proposed such things I've not > > gotten any traction. I suspect that this is an area where an > > implementer needs to take the lead (I definitely will do something > > on this like in Janus/Ada should I ever get to implementing > > contracts, but obviously something AdaCore does will have a lot more impact). > > There have been several user suggestions along those lines, so we > will definitely introduce such a restriction. > Implementation seems straightforward if the definition is tight > enough. Should there be a pragma (sorry, an aspect) that asserts that > the body of a function satisfies this restriction? They seem to go > together. Yes, I think that is required in order to support separate compilation (and dispatching, in class-wide contracts). The question of course is whether this enforces restrictions on the body, and what those restrictions are in that case. This was one of the purposes of the global in/global out annotations, after all: a restriction on the global in/global out allowed in functions called from contract expressions would be easy to specify and enforce. But of course that depends on the full global in/global out mechanisms. Something more limited in scope would be easier to define, inplement, and most likely use. In any case, something to talk about at the meeting. Probably best as a post-Ada 2012 feature, but something that we can scope out anytime as implementations can add their own aspects and restrictions (so there is no pressing rush). **************************************************************** From: Randy Brukardt Sent: Wednesday, June 15, 2011 6:21 PM ... > #3 The AI currently says > 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. > > There are good reasons for this rule and I think messing with > it would lead to problems. Right. Keep in mind that AI05-0247-1 modifies these rules slightly, to ensure that inherited routines enforce all of the invariants (including ones the original body does not know about). In any case, I'll make a skeleton AI to hold this mail so we have something to discuss at the meeting next week. **************************************************************** From: Tucker Taft Sent: Wednesday, June 15, 2011 8:37 PM It certainly makes perfect sense to make the Invariant private, since it is really something to support the implementation, not the client. As far as restrictions, that seems not worth standardizing at this point, and I would expect good compilers to provide warnings without any effort on the part of the user if the invariant has side-effects or other weirdness. Distinguishing internal from external calls seems to be more trouble than it is worth. The called subprogram doesn't know who is its caller, so if it is externally callable, it pretty much needs to ensure the invariant is true on return. Inlining can be a way of dealing with this without any extra language support, for the unusual case where it is needed. **************************************************************** From: Robert Dewar Sent: Thursday, June 16, 2011 4:39 AM ... > As far as restrictions, that seems not worth standardizing at this > point, and I would expect good compilers to provide warnings without > any effort on the part of the user if the invariant has side-effects > or other weirdness. I agree, let implementations respond to actual usage and suggestions and needs of users, standardize next time around if appropriate. **************************************************************** From: Yannick Moy Sent: Thursday, June 16, 2011 2:42 AM > 3) It would be useful if the language made a distinction between > "internal" calls (where the caller is already inside the > implementation of the type in question) and "external" calls. No > runtime invariant checking should be performed for an "internal" call. Indeed, this is what the customer initially suggested, based on his experience with Eiffel and C++: - In Eiffel, it is the syntactic difference between a qualified call "a.f(...)" and an unqualified call "f(...)" (called from a method on the implicit "Current") that decides whether the invariant is checked or not. It is not checked at all on unqualified calls. It is checked on both entry and exit from qualified calls. - For C++, the customer developed their own implementation of C++ macros which implement almost fully the rules of design by contract: - during evaluation of assertions, the function is executed without evaluation of the associated assertions (valid for all assertions) - during an internal call, the invariant is not assessed. The distinction between internal and external calls is implemented with a simple imbrication counter in the implicit attributes of all objects: if the imbrication counter is > 1 during a call, the invariant is not evaluated. But in the conversation that follows, I explained that the distinction between internal and external *calls* is not appropriate. Rather, we should distinguish internal and external *subprograms*. What I mean is the following. Suppose you want to verify formally code that respects the policy of Eiffel. So every routine over type T can be called either in a context in which the invariant of T holds, in which case it must reestablish the invariant at the end, or in a context in which the invariant of T does not hold. This means that every routine has really *two* different contracts... well, not really. Some routines will be called only in a context in which the invariant holds, and they may rely on this, so that they do not execute properly if called in a context in which the invariant does not hold. So in the end you don't know really whether a routine should work only in a context in which the invariant holds, or always. If you perform runtime checking, that's not a problem, because the dynamic environment tells you in which case you are. But if you aim at formal verification, you are left with no other choice than ask the user to provide this information. Since we aim at both with Ada 2012, I much prefer a rule which states exactly which routines expect to be called in a context in which the invariant holds. We agreed that such a rule is to check invariants only on public operations of a type, not on private subprograms (either declared in private part or in body). So that's this rule that I would like the ARG to consider. On 16/06/2011 03:36, Tucker Taft wrote: > Distinguishing internal from external calls seems to be more trouble > than it is worth. The called subprogram doesn't know who is its > caller, so if it is externally callable, it pretty much needs to > ensure the invariant is true on return. Inlining can be a way of > dealing with this without any extra language support, for the unusual > case where it is needed. As explained above, this issue is rather external vs. internal *subprograms*. Without this distinction, the customer says invariants are "unusable" in his context. Note that this customer uses pre- and postconditions (pragmas) extensively (AdaCore developed these for them). My experience is that languages that do not have a distinction of this kind lead to unusable invariants: - in Spec# (C#), it is the user responsibility to "open" and "close" objects, with the invariant being checked on entry/exit of a call only when the caller object is "closed". Very heavy. - in JML (Java), the invariant is required to hold on entry/exit of every call. As a result, invariants are almost not used; people prefer using pre- and postconditions. What would be the problem with this (simple) rule enforcing invariant only on external subprograms? **************************************************************** From: Yannick Moy Sent: Thursday, June 16, 2011 8:34 AM > As explained above, this issue is rather external vs. internal *subprograms*. Our customer pointed us today to the following sentence in B. Meyer's book "Object-Oriented Software Construction 2nd edition", p 366 under "Who must preserve the invariant?": "As a consequence, the obligation to maintain the invariant applies only to the body of features that are exported either generally or selectively; a secret feature - one that is available to no client - is not affected by the invariant." So Eiffel already has this policy of checking the invariant only on external *subprograms*, plus it has the internal/external *call* difference. I believe Ada could implement only the first one, and it would be enough to satisfy the needs expressed so far. Ideally, a renaming-as-body of a private operation into a public one would add the verification of the invariant if necessary: spec: type T is ... with Invariant => Inv(T); procedure External (X : out T); -- Inv(X) checked on exit body: procedure Internal (X : out T); -- no invariant checking procedure External (X : out T) renames Internal; -- adds Inv(X) checking which would give an easy way to use an operation both externally (with invariant checked) and internally (no check). **************************************************************** From: Randy Brukardt Sent: Thursday, June 16, 2011 12:08 PM ... > What would be the problem with this (simple) rule enforcing invariant > only on external subprograms? There is no problem -- it is ALREADY the rule for Type_Invariants in Ada 2012. Specifically, 7.3.2(12-5/3) [the number is from the working draft of the Standard, not sure what it was in Draft 11] says about when an invariant is checked: 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, Note that the last part requires the routine to be one that is visible to clients; it excludes private operations unless they are overriding some visible inherited routine. So the rule you are suggesting is in fact the rule Ada 2012 requires. If your description of the problem is correct, then we need to do nothing. (Whether GNAT properly implements these rules is another question, but irrelevant to the ARG.) **************************************************************** From: Tucker Taft Sent: Thursday, June 16, 2011 4:34 PM > ... What would be the problem with this (simple) rule enforcing > invariant only on external subprograms? As Randy pointed out, this is exactly what Ada 2012 does. **************************************************************** From: Randy Brukardt Sent: Thursday, June 16, 2011 6:54 PM But thanks for confirming that we have it right already. It's one less thing to worry about. :-) **************************************************************** From: Randy Brukardt Sent: Thursday, June 16, 2011 7:05 PM ... > As far as restrictions, that seems not worth standardizing at this > point, and I would expect good compilers to provide warnings without > any effort on the part of the user if the invariant has side-effects > or other weirdness. Well, I surely agree that it is too late for any such restrictions in Ada 2012. But I don't think it is practical to produce warnings for "bad" contract expressions; you could only catch some low-hanging fruit and I have to wonder if such warnings would actually be harmful (by giving a false sense of security). But such warnings aren't possible if the "bad" things occur within called functions; expression functions help a bit, but can provide no help for class-wide contracts as the calls are all dispatching. And as Bob has repeatedly noted, banning all functions other than expression functions and predefined operators really isn't practical (especially in the class-wide cases). We really need some sort of function categorization aspect (or global in/global out aspects), and that would work with the warnings and/or restrictions to fully cover the needs. I do expect AdaCore to end up taking the lead on this, because they clearly have customer requests for this functionality and they will need to convince the entire ARG of what is needed (as I have). That's both good and bad (good because something will actually get done here, bad because the result is likely to be whatever is easiest for GNAT rather than technically best), but I don't think it can be helped. **************************************************************** From: Yannick Moy Sent: Friday, June 17, 2011 2:01 AM >>> ... What would be the problem with this (simple) rule enforcing >>> invariant only on external subprograms? > >> As Randy pointed out, this is exactly what Ada 2012 does. > > But thanks for confirming that we have it right already. It's one less > thing to worry about. :-) thanks for the good news that I'll transmit with pleasure to our customer! **************************************************************** From: Steve Baird Sent: Monday, June 20, 2011 2:32 PM >> It would be useful to have the option of specifying the Invariant >> aspect with the full declaration of the type instead of only at the >> declaration of the partial view of the type. > It certainly makes perfect sense to make the Invariant private, since > it is really something to support the implementation, not the client. There seems to be general support for this idea. Just so that we have a concrete proposal to discuss (whether in Edinburgh or later), here is a proposed wording change. ==== !wording In 7.3.2(2/3), replace Type_Invariant may be specified on a private_type_declaration or a private_extension_declaration. with Type_Invariant may be specified on a private_type_declaration, on a private_extension_declaration, or on a full_type_declaration which declares the completion of a private type or private extension. In 7.3.2(3/3), replace Type_Invariant'Class may be specified on a private_type_declaration or a private_extension_declaration. with Type_Invariant'Class may be specified on a private_type_declaration, on a private_extension_declaration, or on a full_type_declaration which declares the completion of a private type or private extension. **************************************************************** From: Erhard Ploedereder Sent: Saturday, June 25, 2011 3:35 AM This is how I understand the most recently proposed principles: Within the full view of a type, its class-invariants are not checked. Reason: As plain assigments to visible components could violate the invariants without any checking preventing it, it makes no sense to check invariants, if said changes are effected by calls on some subprograms. Within a partial view of the declared type of a variable, all (redundant: dispatching or non-dispatching) calls on primitive operations of this type with the variable as controlling/first argument check all class-invariants of the actual type of the object denoted by the variable. (In addition, any non-class invariant is checked - presumably the one that matches the view for the call.) Reason: It should be guaranteed that despite potential up-casts (i.e., view conversions) and even in the presence of statically bound calls, the invariants of the object cannot be violated by the completed call. ------------------------- Other questions (which may or may not be answered already by the RM: Are invariants and post-conditions checked when the call completes with an exception? Presumably not, but where does it say that? Why aren't invariants checked upon entry as well? They are supposed to hold there, too. For types that have visible components this would make a lot of sense. For fully private types, they are guaranteed by the last call. How do class-wide operations play here? **************************************************************** From: Erhard Ploedereder Sent: Saturday, June 25, 2011 6:44 AM This is how I understand the most recently proposed principles ( further amended to make them work reasonably): Within the full view of a type, its class-invariants are not checked. Reason: As plain assigments to visible components could violate the invariants without any checking preventing it, it makes no sense to check invariants, if said changes are effected by calls on some subprograms instead. (Possible variation, if deemed easier to implement or safer: the class-invariants of the static view of the subprogram are checked.) Within a partial view of a type, all (redundant: dispatching or non-dispatching) calls on subprograms whose body has a full view of this type and has an actual parameter of the type check all class-invariants of the actual type of the object denoted by the parameter. Multiple such parameters cause multiple such checks. (In addition, any non-class invariant is checked - presumably the one that comes with the body of the subprogram, whichever it might be.) Reason: It should be guaranteed that despite potential up-casts and even in the presence of statically bound calls, the invariants of the type of the !object! cannot be violated by the completed call. ------------------------- Other questions (which may or may not be answered already by the RM: Are invariants and post-conditions checked when the call completes with an exception? Presumably not, but where does it say that? Why aren't invariants checked upon entry as well? They are supposed to hold there, too. For types that have visible components this would make a lot of sense. For fully private types, they are guaranteed by the last call and hence could be optimized away. When can the checks be optimized away? (even in the presence of unchecked_* stuff?) (How do class-wide operations play? They are included in the above, as are any other subprograms that have visibility to the type's details.) **************************************************************** From: Tucker Taft Sent: Saturday, June 25, 2011 10:26 AM Replace the 7.3.2(10-16/3) with: Static Semantics [Redundant: If the Type_Invariant aspect is specified for a type T, then the invariant expression applies to T.] [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 successful default initialization of an object of type T, the check is performed on the new object; * After successful conversion to type T, the check is performed on the result of the conversion; * After assigning to a view conversion, outside the immediate scope of T, that converts from T or one or more record extensions (and no private extensions) of T to an ancestor of type T, a check is performed on the part of the object that is of type T; similarly, for passing a view conversion as an OUT or IN OUT parameter outside the immediate scope of T, this check is performed upon successful return; * After a successful call on the Read or Input stream attribute of the type T, the check is performed on the object initialized by the stream attribute; * Upon successful return from a call on any subprogram or entry that: - 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, - has a result with a part of type T, or one or more IN OUT or OUT parameters with a part of type T, or an access to variable parameter whose designated type has a part of type T. the check is performed on each such part of type T. **************************************************************** From: Randy Brukardt Sent: Sunday, June 26, 2011 4:25 AM Modify 3.9.2(20.4): otherwise, the action is the same as the action for the corresponding operation of the parent type or progenitor type from which the operation was inherited {except that additional invariant checks (see 7.3.2) and class-wide postcondition checks (see 6.1.1) may apply}. If there is more than one such corresponding operation, the action is that for the operation that is not a null procedure, if any; otherwise, the action is that of an arbitrary one of the operations. Delete 7.3.2(18/3). **************************************************************** From: Erhard Ploedereder Sent: Sunday, June 26, 2011 4:51 AM Proposed Wording: Note: A call on a primitive subprogram of type NT that is inherited from type T will need to satisfy the specific invariants of both the types NT and T. A call on a primitive subprogram of type NT that is redefined for type NT will need to satisfy only the specific invariants of the type NT. **************************************************************** From: Yannick Moy Sent: Monday, June 27, 2011 1:54 AM > Other questions (which may or may not be answered already by the RM: > > Are invariants and post-conditions checked when the call completes > with an exception? Presumably not, but where does it say that? I guess that's the meaning of "successful return" in: * Upon successful return from a call on any subprogram or entry that: [...] > Why aren't invariants checked upon entry as well? They are supposed to > hold there, too. For types that have visible components this would > make a lot of sense. For fully private types, they are guaranteed by > the last call. AI says: > 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 would add as an important benefit that invariant is not checked at all on calls to functions taking only IN parameters. This is crucial to be able to have calls to (public) functions or expression functions in invariants. Otherwise you'd get an infinite loop. **************************************************************** From: Yannick Moy Sent: Monday, June 27, 2011 2:02 AM The AI wording you sent does not contain the proposed amendment sent by Steve on 2011/06/20, to allow invariants being defined on full_type_declaration for a private type. (with the possibility of direct component access in the invariant) Does that mean this amendment was not adopted? BTW, the example in !proposal should mention Type_Invariant, not Invariant. **************************************************************** From: Randy Brukardt Sent: Thursday, June 30, 2011 2:33 PM ... > The AI wording you sent does not contain the proposed amendment sent > by Steve on 2011/06/20, to allow invariants being defined on > full_type_declaration for a private type. > (with the possibility of direct component access in the invariant) > > Does that mean this amendment was not adopted? No, it means that Tuck started with an obsolete AI rather than the current wording of the Standard as amended by the first day of the meeting. It will be the editor's job (that is, me) to merge all of the various decisions into a single whole. In this case, there was some concern about whether Type_Invariant'Class should be required to be visible (because it affects child types), while there is no reason for specific Type_Invariants to be visible. Deciding that was deferred, and I'm not sure that we ever actually decided that (I didn't see a decision in a quick scan of my notes). We ought to do that. ;-) **************************************************************** From: Randy Brukardt Sent: Wednesday, July 27, 2011 9:36 PM Actually, after reading my notes carefully, what happened is that we immediately decided to adopt Steve's wording of June 20th (changing "which" to "that") for Type_Invariant only (not Type_Invariant'Class, since descendants need to know about it in order to write operations correctly). That happened in the first 30 minutes of the meeting. We then spent the entire remainder of the 3 day meeting changing type invariants (doing other things in between discussions), not concluding until there was 30 minutes left in the meeting. By then, we'd totally forgotten about the initial decision. I'm going to presume that we still intend this change (I can't think of any reason why not), so anyone that disagrees should speak up. P.S. I didn't actually explain the change: In 7.3.2(2/3), replace Type_Invariant may be specified on a private_type_declaration or a private_extension_declaration. with Type_Invariant may be specified on a private_type_declaration, on a private_extension_declaration, or on a full_type_declaration that declares the completion of a private type or private extension. **************************************************************** From: Bob Duff Sent: Friday, July 1, 2011 8:17 AM > !standard 7.3.2 (00) 10-10-19 AI05-0146-1/08 This AI is inconsistent about the name of the aspect -- Invariant versus Type_Invariant. IMHO it should be Invariant, because "Type_" is just noise -- you can see from the syntax that it applies to the type it's attached to. If we had package invariants, they should be called Invariant, too, not Package_Invariant. **************************************************************** From: Randy Brukardt Sent: Friday, July 1, 2011 6:54 PM > > !standard 7.3.2 (00) > 10-10-19 AI05-0146-1/08 > > This AI is inconsistent about the name of the aspect -- Invariant > versus Type_Invariant. No, it's not. The !wording consistently uses Type_Invariant. The examples are just plain wrong, and all that means is that someone forgot to update them. Big deal. In any case, this AI is not going to be changed, because it is already WG 9 approved. AI05-0250-1 will include the changes we approved at the meeting. > IMHO it should be > Invariant, because "Type_" is just noise -- you can see from the > syntax that it applies to the type it's attached to. Huh? We use exactly the same syntax for subtype predicates. They don't apply to the type, only the subtype. The whole point of saying "Type_Invariant" is to make it clear that this is type-related, as opposed to predicates, which are subtype-related. These use the same syntax and are allowed on some of the same declarations (and conceivably could be used at the same time on a declaration). Recall that the name of the predicates was "Subtype_Predicate" before we split them into static and dynamic versions -- these really should be Static_Subtype_Predicate and Dynamic_Subtype_Predicate, but those are too long. There was a lot of confusion about the difference between these two, and we wanted to make it crystal clear which was which. That need has not gone away (even if the ARG itself is more comfortable with the distinction). In any case, we just spent 1/3 of the recent meeting talking about "type invariants", and that would have been the perfect time to raise this issue. I have to assume you really don't feel that strongly about it or you would have had to say something! It's now effectively too late, in that with the holidays and summer vacations, it will be impossible to have a discussion with everyone involved. (And e-mail discussions tend to be dominated by a handful of people.) And quite frankly, naming discussions are interminable and a bad use of my (and everyone else's) limited time. (30 messages = 1 hour of my time on average.) > If we had package invariants, they should be called Invariant, too, > not Package_Invariant. Perhaps, but there is no possibility of confusion there (there isn't any such thing as a subpackage). And in any case, we don't have package invariants and are unlikely to ever have them (the semantic problems aren't suddenly going to disappear at some point in the next 5 years), so what they might be called seems irrelevant. **************************************************************** From: Bob Duff Sent: Friday, July 1, 2011 5:54 AM >...(30 messages = 1 > hour of my time on average.) That's an interesting statistic. I get about 300 emails per day, mostly on report@adacore.com. (That's week days; I think it's less than 100 on weekend days.) So if I spent 1 hour per 30, I'd spend 10 hours a day doing nothing but reading and filing email. Yikes! **************************************************************** From: John Barnes Sent: Saturday, July 2, 2011 9:50 AM And the Rat says Type_Invariant, so that's that. **************************************************************** From: Bob Duff Sent: Saturday, July 2, 2011 11:30 AM Hmm, this could save Randy and the rest of us a lot of trouble. Let's just go by what's in the Rat, and forget about this silly RM document. ****************************************************************