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

Differences between 1.3 and version 1.4
Log of other versions for file ai05s/ai05-0146-1.txt

--- ai05s/ai05-0146-1.txt	2009/06/08 04:01:51	1.3
+++ ai05s/ai05-0146-1.txt	2009/10/23 06:06:31	1.4
@@ -55,39 +55,39 @@
 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;
-    
-   
+
+
 Here is a more formal syntax for the invariant specification, based
 on the more general aspect_specification syntax proposed for pre- and
 post-conditions:
 
-    aspect_specification ::= 
-       [with aspect_mark => expression {, 
+    aspect_specification ::=
+       [with aspect_mark => expression {,
              aspect_mark => expression}];
-             
+
     aspect_mark ::= identifier['Class]
-             
-    private_type_declaration ::= 
+
+    private_type_declaration ::=
        type defining_identifier [discriminant_part] is [[abstract] tagged] [limited] private
          [aspect_specification];
 
-    private_extension_declaration ::= 
+    private_extension_declaration ::=
        type defining_identifier [discriminant_part] is
          [abstract] [limited | synchronized] new ancestor_subtype_indication
          [and interface_list] with private
@@ -111,11 +111,11 @@
 
 * For a type with a specified Invariant aspect, upon return from a call
   on any procedure that
-  
+
     - has one or more [IN] OUT parameters of the specified type,
     - is defined within the immediate scope of the type, and
     - is visible outside the immediate scope of the type,
-    
+
   one evaluation is performed of the expression for each such [IN] OUT
   parameter, with final value of the parameter as the current instance.
   Similarly, after evaluation of a function call or type conversion that
@@ -125,14 +125,14 @@
   performed of the boolean_expression with the default-initialized
   object as the current instance.
 
-* For a tagged type with a specified Invariant'Class aspect, upon return 
+* For a tagged type with a specified Invariant'Class aspect, upon return
   from a call on any procedure that
-  
+
     - has one or more [IN] OUT parameters of a type within the
       derivation class of the specified type,
     - is defined within the immediate scope of such a type, and
     - is visible outside the immediate scope of the type,
-    
+
   one evaluation is performed of the boolean expression for each such
   [IN] OUT parameter. The parameter is view-converted to the class-wide
   type prior to the call, ensuring that any calls on dispatching
@@ -181,7 +181,7 @@
 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.  
+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
@@ -229,7 +229,7 @@
 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. 
+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.
@@ -237,16 +237,16 @@
 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,
@@ -365,9 +365,9 @@
 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 
+> 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
@@ -381,8 +381,8 @@
 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 
+> 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.
@@ -397,7 +397,7 @@
 
 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 
+> pre and post conditions are specific as to when they should evaluate
 > to true, but invariants cover a region (but not the whole program)
 
 ****************************************************************
@@ -406,7 +406,7 @@
 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 
+> 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
@@ -435,8 +435,8 @@
         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 
+> 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,
@@ -464,7 +464,7 @@
 From: Edmond Schonberg
 Sent: Thursday, February 26, 2009  12:50 PM
 
-> Question: In an invariant, does one refer to the "current instance"  
+> Question: In an invariant, does one refer to the "current instance"
 > in the
 > usual way, by naming the [sub]type?  As in:
 >
@@ -491,7 +491,7 @@
 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. 
+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.
@@ -510,7 +510,7 @@
 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 
+> 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
@@ -534,9 +534,9 @@
 Sent: Friday, February 27, 2009  12:58 AM
 
 > By limiting the invariant to
-> a private type, the check is limited to the visible primitive 
+> 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?
 
 ****************************************************************
@@ -544,7 +544,8 @@
 From: Edmond Schonberg
 Sent: Friday, February 27, 2009  2:57 PM
 
-No reason, written in haste. Of course visible classwide operations are included.
+No reason, written in haste. Of course visible classwide operations are
+included.
 
 ****************************************************************
 
@@ -553,6 +554,429 @@
 
 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.
 
 ****************************************************************
 

Questions? Ask the ACAA Technical Agent