CVS difference for ai05s/ai05-0250-1.txt
--- ai05s/ai05-0250-1.txt 2011/06/15 23:35:41 1.1
+++ ai05s/ai05-0250-1.txt 2011/06/20 04:55:19 1.2
@@ -11,19 +11,20 @@
!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.
+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
@@ -36,11 +37,15 @@
!discussion
** TBD.
+
+[Editor's note: For (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.
-[Editor's note: For (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 is subtle enough, without complicating the issue more by making it depend on
-where and how the call is made.]
+The mail from Yannick Moy suggests that this is in fact the correct solution. So
+we probably want no action on (3).]
!ACATS test
@@ -262,5 +267,251 @@
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!
****************************************************************
Questions? Ask the ACAA Technical Agent