CVS difference for ai05s/ai05-0289-1.txt

Differences between 1.1 and version 1.2
Log of other versions for file ai05s/ai05-0289-1.txt

--- ai05s/ai05-0289-1.txt	2012/02/14 06:57:11	1.1
+++ ai05s/ai05-0289-1.txt	2012/03/15 05:17:02	1.2
@@ -1,6 +1,7 @@
-!standard  7.3.2(0)                               12-02-13    AI05-0289-1/01
+!standard  7.3.2(0)                               12-03-14    AI05-0289-1/02
 !class Amendment 12-02-13
 !status Amendment 2012 12-02-13
+!status ARG Approved 7-0-3  12-02-24
 !status work item 12-02-13
 !status received 12-02-04
 !priority Low
@@ -8,9 +9,8 @@
 !subject Invariants and in-mode parameters whose value is changed
-Invariants are not checked on "in" parameters after a call. If a parameter is
-going to be modified (logically), the package should check it explicitly, or
-(better) declare the parameter as "in out".
+Invariants are checked on all parameters of the type after a call, including
+"in" parameters.
@@ -24,18 +24,22 @@
 access value.
 Should "in" parameters be checked to see if their invariants still hold
-after calls? (No.)
+after calls? (Yes.)
-Add a new note after 7.3.2(24/3):
+Modify 7.3.2(19/3):
-Invariants are not checked after a call for *in* parameters of a type. If
-the logical properties of an *in* parameter are modified by a subprogram
-(possibly via an embedded access value), the invariant may not hold on the
-object after the call. Generally, such parameters should be declared as
-*in out* parameters.
+* 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.
+Modify the last sentence of 7.3.2(21/3):
+Invariant checks, any postcondition check, and any constraint {or predicate}
+checks associated with [by-copy] in out or out parameters are performed in an
+arbitrary order.
 This issue occurs whenever the logical view of an object that is declared
@@ -75,19 +79,17 @@
 allows such parameters, and thus the necessity to use the Rosen technique has
 been substantially lessened.
-Finally, just because a parameter *could* be modified does not mean that the
-programmer *ought* to do so. Making logical modifications (those that might
-change the invariant value) to an object passed as an *in* parameter is wrong
-from a user-expectation standpoint.
-As such, there is no important reason to change which invariants are checked.
-Any problems can be avoided with proper design of the package. Moreover,
-checking all "in" parameters would greatly increase the expense of the
-checks (as "in" parameters are more than 80% of all parameters) and would
-catch many fewer errors than the other checks (as changes to "in" parameters
-ought to be rare).
+However, using "in" parameters is a time-honored technique in Ada programs,
+and changing to "in out" isn't always easy. Ada.Text_IO is a widely used
+(and copied) example.
+So, while this issue is under the control of the programmer, it's not clear-cut
+that it can always be avoided. Moreover, invariants (unlike predicates) are
+intended to be bullet-proof (that's why they're restricted to private types)
+outside of unusual circumstances. Only a fool (or your editor - draw your own
+conclusions :-) would argue that Ada.Text_IO is unusual.
-Therefore, we simply add a note to warn of this possibility.
+So we require that all parameters are checked after calls into the package.
 !corrigendum 7.3.2(0)
@@ -97,7 +99,7 @@
 !ACATS Test
-Create an ACATS C-Test to test this subprogram.
+Create an ACATS C-Test to test that invariant checks are applied to "in" parameters.
@@ -845,5 +847,135 @@
 (for more details about our strategy for mixing tests and proofs, see the paper
 we just published at ERTS2: -
+From: Randy Brukardt
+Sent: Monday, March 14, 2012  9:31 PM
+The last bit of 7.3.2(21/3) says:
+Invariant checks, any postcondition check, and any constraint checks associated
+with by-copy in out or out parameters are performed in an arbitrary order.
+Great, but what about predicate checks associated with by-copy in out and out
+parameters? They're not constraint checks, or any of the other kinds of checks either.
+Invariant checks, any postcondition check, and any constraint {or predicate} checks
+associated with by-copy in out or out parameters are performed in an arbitrary order.
+P.S. Happy PI day!
+From: Randy Brukardt
+Sent: Monday, March 14, 2012  10:20 PM
+After sending the last message, I though of a slightly more important bug:
+3.2.4 also defines predicate checks on by-reference in out or out parameters.
+Probably that sentence of 7.3.2(21/3) ought to include them as well:
+   Invariant checks, any postcondition check, and any constraint {or predicate}
+   checks associated with [by-copy] in out or out parameters are performed
+   in an arbitrary order.
+But that set me to wondering: we changed the rules for invariants so that
+they're checked for all parameters on the way out, regardless of mode. Should we
+have done something similar for predicates as well?
+That is, the current rules for predicates check by-copy in out and out
+parameters by the "normal" subtype conversion check, and by-reference in out and
+out parameters by a special rule.
+But we're now checking all parameters for invariants; perhaps we need to do that
+for parameters?
+We surely don't need to do that for by-copy parameters; the original objects
+will never be modified and thus any changes will be lost.
+[Aside: Humm: I wonder if invariants also should except by-copy in parameters
+somehow? These can't be changed by any means, and rechecking them is just wasted
+time. I suppose it depends on the invariant; the parameter is an index, it might
+point into a global table, which could have changed. But then the by-copy
+objects could have changed, too. Barf.]
+But a by-reference object could have been changed (especially if it has embedded
+I personally would say that such checks should not be performed; a predicate
+should be about the value of the object and not about the value of anything
+else. But then again, I'd say the same about an invariant and I lost that
+argument. So I don't think that anything *I* think on this one is likely to be
+That being the case, I think we need to make these checks on *all* parameters on
+the way out, just like we decided to do for invariants. That's probably not a
+real problem for static predicates (they can't depend on anything global, their
+types are always by-copy, so there would never be any need to perform those
+checks again). But it would be fairly rare that a dynamic predicate could be
+removed (it could only be removed if it didn't contain any references outside of
+the object, which means no dereferences, no globals, and (in most compilers,
+anyway) no regular function calls). (This is just like the situation with
+invariants, which almost never can be eliminated for "in" parameters; only in
+similar cases as outlined above.)
+So, I suggest that we modify the second sentence of 3.2.4(22/3) as follows:
+   After normal completion and leaving of a subprogram, for each [in out or out]
+   parameter [that is passed by reference]{other than an in out or out parameter
+   passed by copy}, the predicate of the subtype of the actual is evaluated, and
+   a check is made that the predicate is True.
+And extend the existing AARM note:
+   Static_Predicate checks can be removed even in the presence of potentially
+   invalid values, just as constraint checks can be removed. {In particular, it
+   is never necessary to perform a Static_Predicate check on an in parameter of
+   a by-copy type after a call, as neither the parameter value nor the result of
+   the predicate expression can change from when it was evaluated before the
+   call. In contrast, a Dynamic_Predicate check of an in parameter of a by-copy
+   type can only be eliminated if the compiler can prove that the value of the
+   predicate expression cannot depend on any global values (or it can prove that
+   those values haven't changed).}
+This is a fairly big change (it will force more users to turn off predicate
+checks, because there will be many more checks on parameters), so I think we'll
+need to vote.
+Just as I was about to hit "send" on this, I realized that the situation is not
+quite as similar with invariants as I previously thought. An invariant evaluates
+the *same* check in both directions. The predicate checks described about are on
+the subtype of the *formal* on the way into a call, and on the subtype of the
+*actual* on the way out.
+But the point is the same - if an "in" parameter is modified "under-the-covers",
+the check may need to be retried. OTOH, there are many holes in the
+Dynamic_Predicate model in any case, and we're not going to try to plug those.
+That's the point of 3.2.4(27/3). So the need to plug this hole is much less than
+the need to plug the hole for invariants. (There are other holes in invariants,
+which can only be exploited with the help of the abstraction creator; I would
+have thought that "in" parameters were also in that category, but somehow I lost
+that one. Again, I don't think that too much of what I think is relevant here.)
+So now I'm just 100% confused. There seem to be three possibilities; please vote
+for one and explain if you want:
+         ________  Leave 3.2.4(22/3) unmodified. (We're not going to try to make
+		   Dynamic_Predicates "work"; it's impossible.)
+         ________  Recheck a by-reference parameter of any mode after a call;
+		   don't check by-copy parameters. (The by-copy parameter is
+		   unmodified, and if a Dynamic_Predicate changes value by other
+		   reason, we're not trying to keep it working. OTOH, it's
+		   possible to modify an "in" parameter via the Rosen technique,
+		   so rechecking makes sense.)
+         ________  Recheck everything after a call as described above. (The
+		   fewer holes the better.)

Questions? Ask the ACAA Technical Agent