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 :-)
+
+****************************************************************
Questions? Ask the ACAA Technical Agent