CVS difference for ai12s/ai12-0079-1.txt

Differences between 1.4 and version 1.5
Log of other versions for file ai12s/ai12-0079-1.txt

--- ai12s/ai12-0079-1.txt	2014/10/14 00:58:20	1.4
+++ ai12s/ai12-0079-1.txt	2014/11/13 04:00:55	1.5
@@ -325,3 +325,255 @@
 
 ****************************************************************
 
+From: Bob Duff
+Sent: Tuesday, October 14, 2014  5:20 PM
+
+> Here is an AI on the Global aspect, based on SPARK and on the HILT 
+> 2014 paper on parallel language extensions for Ada.
+
+Looks good.  You make it look so simple.  So why didn't we already do this?
+I guess the Devil's in the "!wording".
+
+See below for editorial comments and some questions.
+
+> !summary
+> 
+> Annotations are provided to describe the use of global objects by subprograms.
+                                                         ^^^^^^^
+
+variables
+
+> !problem
+> 
+> Ada 2012 added many kinds of assertions to Ada in order to increase 
+> the ability of a programmer to specify contracts for types and 
+> subprograms. These contracts are defined to be checked at runtime, but 
+> are intended to be potentially checked (at least in part) statically.
+> 
+> However, without knowledge of side-effects of functions used in the 
+> aspects, a tool has to assume the worst about any user-defined 
+> functions. For example, that
+                                                        ^^^^^^^^^ subprograms
+
+> the result of a function can change even when called with the same 
+> operands. Other assumptions could cause incorrect programs to be 
+> accepted as correct, and if the assumptions were used to omit "proved"
+> aspects, to erroneous execution.
+                           ^^^^          ^^^^^^^
+
+I think you mean "suppress...checks".  If not, please explain.
+
+> Both of these results are unacceptable for a feature intended to 
+> improve the correctness of programs.
+> 
+> The worst-case assumptions pretty much prevent any analysis unless the 
+> bodies of any user-defined functions used in the aspects are 
+> available. This is bad, as it prevents analysis of programs as they 
+> are constructed. If the body is not available, no analysis is 
+> possible. Moreover, analysis depending on a body require creating 
+> pseudo body dependencies (if the body is changed, any analysis 
+> depending on the properties of that body would have to be performed 
+> again); but the language does not allow these to be "real" body
+> dependencies (any recompilation needed has to occur automatically).
+
+I agree, having to look at bodies is "bad", but those don't seem like the main
+reasons why.  To me, the main reason is the usual software engineering one: you
+want well-defined interfaces, and you want to depend ONLY on those interfaces
+(i.e. specs).  If you prove something about package body X, you want that proof
+to be valid in the presence of arbitrary changes to bodies called by X.
+
+> We need to refine the notion of SPARK's Global aspect, because SPARK 
+> does not support access types, and because SPARK relies on an 
+> elaborate mechanism for handling the abstract “state” of packages.
+
+What's your opinion about that elaborate mechanism?  I've never understood why
+it's needed, but I'm told by SPARK folks that it's super-useful.  I'd like to
+understand why, and whether we ought to add such stuff to Ada.
+
+>...The
+> refinements we are proposing are the following:
+> 
+> 1.	Allow the name of an access type A (including "access T") to
+> stand-in for the set of objects described roughly by: 
+
+"stand in" (no dash)
+
+>    (for all X convertible to A => X.all)
+
+That's the same thing as the collection of A, right?
+
+> 2.	Allow the name of a package P to stand-in for the set of objects
+> described roughly by: 
+> 
+>    (for all variables X declared in P => X)
+
+Does that include children of P?
+
+> !wording
+> 
+> ** TBD.
+
+;-)  ;-)
+
+> !discussion
+> 
+> Global annotations are critical to being able to perform any sort of 
+> modular static analysis.
+
+Yeah, that's what I meant by my "software engineering" comment above.
+
+> All of the global in, in-out, and out annotations proposed can be 
+> statically checked.
+> 
+> Note that it is possible to lie about the use of globals of 
+> subprograms and other entities that are imported. This is of course 
+> impossible to check, but thankfully is covered by B.1(38.1/2). 
+> Incorrect annotations on imported subprograms could cause a program to be
+> erroneous.
+> 
+> SPARK does not currently support identifying particular components of 
+> a global variable in the Global aspect, but for Ada we plan to allow that.
+> This is somewhat inconsistent with what can be specified for 
+> parameters, since there is no easy way to identify which components of 
+> an in-out parameter are actually updated. It is possible to specify in 
+> a postcondition that X.C = X.C'Old and X.D = X.D'Old and ... but that 
+> can be a maintenance issue as the names and numbers of subcomponents 
+> changes, and only works for types that have an appropriate "=" operator.
+> It might be useful to have another aspect that indicated which 
+> components of an in-out parameter might be updated, with all others 
+> presumably being preserved (e.g. Updated => (X.A, X.B)).
+
+Yes, I'm a fan of limited types, and I'd like to be able to say things like
+that.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Tuesday, October 14, 2014  9:37 PM
+
+...
+>> However, without knowledge of side-effects of functions used in the 
+>> aspects, a tool has to assume the worst about any user-defined 
+>> functions. For example, that
+>                                                          ^^^^^^^^^ 
+> subprograms
+>
+>> the result of a function can change even when called with the same 
+>> operands. Other assumptions could cause incorrect programs to be 
+>> accepted as correct, and if the assumptions were used to omit "proved" aspects, to erroneous execution.
+>                             ^^^^          ^^^^^^^
+>
+> I think you mean "suppress...checks".  If not, please explain.
+
+I didn't actually write the "problem" statement.  I think it might be Randy's original wording.
+
+
+>> Both of these results are unacceptable for a feature intended to 
+>> improve the correctness of programs.
+>>
+>> The worst-case assumptions pretty much prevent any analysis unless 
+>> the bodies of any user-defined functions used in the aspects are 
+>> available. This is bad, as it prevents analysis of programs as they 
+>> are constructed. If the body is not available, no analysis is 
+>> possible. Moreover, analysis depending on a body require creating 
+>> pseudo body dependencies (if the body is changed, any analysis 
+>> depending on the properties of that body would have to be performed 
+>> again); but the language does not allow these to be "real" body
+>> dependencies (any recompilation needed has to occur automatically).
+>
+> I agree, having to look at bodies is "bad", but those don't seem like 
+> the main reasons why.  To me, the main reason is the usual software 
+> engineering one: you want well-defined interfaces, and you want to 
+> depend ONLY on those interfaces (i.e. specs).  If you prove something 
+> about package body X, you want that proof to be valid in the presence 
+> of arbitrary changes to bodies called by X.
+
+Agreed.  Again, this problem statement was from an earlier version of the AI.
+It seemed adequate to capture the problem, but it could perhaps use some
+wordsmithing.
+
+>> We need to refine the notion of SPARK's Global aspect, because SPARK 
+>> does not support access types, and because SPARK relies on an 
+>> elaborate mechanism for handling the abstract “state” of packages.
+>
+> What's your opinion about that elaborate mechanism?  I've never 
+> understood why it's needed, but I'm told by SPARK folks that it's 
+> super-useful.  I'd like to understand why, and whether we ought to add 
+> such stuff to Ada.
+
+The elaborate mechanism is needed if you make heavy use of global variables.
+I have come to really hate global variables, so for me, it seems to only
+encourage an evil habit.  But when it comes to typical embedded software, I
+know that it is quite common to have a huge number of global variables
+representing the state of the environment.  These global variables are
+periodically updated as the result of sensor readings, and they are read
+whenever needed by algorithms trying to react to the environment.  I would
+hope there are better ways to structure such systems, but I think SPARK is
+trying to deal with reality as we know it, and many of these systems seem
+to represent the state using globals.
+
+>> ...The
+>> refinements we are proposing are the following:
+>>
+>> 1.	Allow the name of an access type A (including "access T") to
+>> stand-in for the set of objects described roughly by:
+>
+> "stand in" (no dash)
+
+Good point.
+
+>>     (for all X convertible to A => X.all)
+>
+> That's the same thing as the collection of A, right?
+
+Yes for a pool-specific access type, no for a general access type.
+
+>> 2.	Allow the name of a package P to stand-in for the set of objects
+>> described roughly by:
+
+"stand in" here too.
+
+>>
+>>     (for all variables X declared in P => X)
+>
+> Does that include children of P?
+
+It would presumably need to include the private children of P, but not the
+public children, as you could name them separately.
+
+>> ...
+>> It might be useful to have another aspect that indicated which 
+>> components of an in-out parameter might be updated, with all others 
+>> presumably being preserved (e.g. Updated => (X.A, X.B)).
+>
+> Yes, I'm a fan of limited types, and I'd like to be able to say things 
+> like that.
+
+If we adopt something like "Updated" then it might make sense to keep Global
+at the whole-object level, and use "Updated" to provide more precision for both
+parameters and globals.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Wednesday, November 12, 2014  9:51 PM
+
+> > Here is an AI on the Global aspect, based on SPARK and on the HILT
+> > 2014 paper on parallel language extensions for Ada.
+> 
+> Looks good.  You make it look so simple.  So why didn't we already do 
+> this?  I guess the Devil's in the "!wording".
+
+Mostly FUD, really. You and I spent a lot of hours creating AI05-0186-1,
+complete with wording. (Perhaps you've forgotten about that.) People were
+concerned that it was insufficiently mature, so it didn't end up as part of
+Ada 2012.
+
+Also, I think there was a desire to let SPARK 2014 plow this ground first
+(which only covers part of the problem, of course).
+
+Unfortunately, most of the work will have to be redone; hopefully Tucker et.
+al. will be able to use some of the wording created for AI05-0186-1 so the
+effort won't totally go to waste.
+
+****************************************************************

Questions? Ask the ACAA Technical Agent