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

--- ai05s/ai05-0145-1.txt	2009/02/17 06:01:04	1.1
+++ ai05s/ai05-0145-1.txt	2009/02/17 06:09:17	1.2
@@ -1,4 +1,4 @@
-!standard 11.5 (00)                                09-02-15  AI05-0145-1/01
+!standard 11.5 (00)                                09-02-16  AI05-0145-1/02
 !standard 11.4.1 (10)
 !class amendment 09-02-15
 !status work item 09-02-15
@@ -59,6 +59,12 @@
 subprogram specification so that the formal parameter names are
 directly visible.
 
+The names in the boolean_expression of a precondition
+or postcondition pragma are resolved not at the point
+of the pragma, but rather at the freezing point of the
+named subprogram, or at the end of the immediately
+enclosing visible part, whichever comes first.
+
 For a postcondition on a function, the attribute "Result" is defined
 on the subprogram name, yielding the value returned by the function.
 For a postcondition on a procedure, the attribute "Old"
@@ -162,6 +168,12 @@
 hence cannot catch as many bugs by itself as the combination of an 
 inherited condition and a condition specific to a particular body.  
 
+We defer resolving the names in the boolean_expression
+because it is natural for preconditions or postconditions
+to refer to other subprograms declared in the same
+scope, and requiring that there be no forward references
+unduly restricts the expressions.
+
 A possible implementation model for the pre/postcondition checks is as follows.
 Existing calls on Proc or Func are replaced with calls on "Proc_with_check"
 or "Func_with_check" if the assertion policy is "Check" at the point of the
@@ -341,4 +353,36 @@
 
 ****************************************************************
 
+From: Tucker Taft
+Sent: Sunday, February 15, 2009  4:27 PM
+
+I left out one important issue:
+
+   The names in the boolean_expression of a precondition
+   or postcondition pragma are resolved not at the point
+   of the pragma, but rather at the freezing point of the
+   named subprogram, or at the end of the immediately
+   enclosing visible part, whichever comes first.
+
+and from the discussion:
+
+   We defer resolving the names in the boolean_expression
+   because it is natural for preconditions or postconditions
+   to refer to other subprograms declared in the same
+   scope, and requiring that there be no forward references
+   unduly restricts the expressions.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Sunday, February 15, 2009  5:01 PM
+
+I haven't studied the whole proposal carefully, but as far as I can
+tell, the Precondition/Postcondition part of it corresponds pretty much
+exactly to what has been implemented in GNAT, and used fairly extensively.
 
+>> A resurrection of AI95-00375 on type invariants will appear shortly.
+
+I look forward to that, we have always got stuck on invariants :-)
+
+****************************************************************