CVS difference for ai05s/ai05-0145-2.txt
--- ai05s/ai05-0145-2.txt 2010/11/13 06:56:45 1.13
+++ ai05s/ai05-0145-2.txt 2011/02/12 08:19:56 1.14
@@ -81,7 +81,7 @@
This aspect specifies a postcondition for a callable entity and its
descendants; it shall be specified by an expression, called a
*postcondition expression*.
-
+
Name Resolution Rules
The expected type for a precondition or postcondition expression is
@@ -234,7 +234,7 @@
If the bounded error is detected, Program_Error is raised. If not detected,
execution proceeds normally, but if it is invoked within a protected action,
it might result in deadlock or a (nested) protected action.
-
+
NOTE: A precondition is checked just before the call. If another task can
change any value that the precondition expression depends on, the precondition
@@ -498,7 +498,7 @@
If the bounded error is detected, Program_Error is raised. If not detected,
execution proceeds normally, but if it is invoked within a protected action,
it might result in deadlock or a (nested) protected action.
-
+
@s9<NOTES@hr
A precondition is checked just before the call. If another task can
change any value that the precondition expression depends on, the precondition
@@ -1278,6 +1278,148 @@
****************************************************************
+From: Robert Dewar
+Sent: Wednesday, August 18, 2010 10:36 AM
+
+I have implemented an approach where internally I allow multiple Pre and Post
+aspects, splitting apart expressions in the single Pre/Post aspect allowed by
+the syntax. This allows giving more accurate messages, as shown by the following
+test:
+
+> 1. with Text_IO; use Text_IO;
+> 2. with Ada.Exceptions; use Ada.Exceptions;
+> 3. procedure prepost is
+> 4. function F (X : Integer) return Integer with
+> 5. Pre => X > 11
+> 6. and then
+> 7. X mod 2 = 1,
+> 8. Post => F'Result = X + 1
+> 9. and then
+> 10. F'Result /= 18;
+> 11.
+> 12. function F (X : Integer) return Integer is
+> 13. begin
+> 14. if X = 13 then
+> 15. return X;
+> 16. else
+> 17. return X + 1;
+> 18. end if;
+> 19. end F;
+> 20.
+> 21.
+> 22. begin
+> 23. Put_Line (F (31)'Img);
+> 24.
+> 25. begin
+> 26. Put_Line (F (13)'Img);
+> 27. exception
+> 28. when E : others =>
+> 29. Put_Line ("exception raised for F (13): "
+> 30. & Exception_Message (E));
+> 31. end;
+> 32.
+> 33. begin
+> 34. Put_Line (F (12)'Img);
+> 35. exception
+> 36. when E : others =>
+> 37. Put_Line ("exception raised for F (12): "
+> 38. & Exception_Message (E));
+> 39. end;
+> 40.
+> 41. begin
+> 42. Put_Line (F (11)'Img);
+> 43. exception
+> 44. when E : others =>
+> 45. Put_Line ("exception raised for F (11): "
+> 46. & Exception_Message (E));
+> 47. end;
+> 48.
+> 49. begin
+> 50. Put_Line (F (17)'Img);
+> 51. exception
+> 52. when E : others =>
+> 53. Put_Line ("exception raised for F (17): "
+> 54. & Exception_Message (E));
+> 55. end;
+> 56. end prepost;
+
+The output when this is run is:
+
+> 32
+> exception raised for F (13): failed postcondition from line 8
+> exception raised for F (12): failed precondition from line 7 exception
+> raised for F (11): failed precondition from line 5 exception raised
+> for F (17): failed postcondition from line 10
+
+So we can get the diagnostic clarity of separate Pre/Post aspects without
+actually allowing them explicitly, and instead requiring the use of and then.
+
+P.S. I have no idea what Randy is on about when he says that the ARG does not
+like the idea of using Pre and Post conditions for debugging. To me that in
+practice is the main use. Yes I know about input to formal tools etc, but in
+practice being able to tell which pre or post condition has failed is quite
+critical to their usability.
+
+In the case of inherited post conditions, I will make sure we point to which
+post condition failed.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Wednesday, August 18, 2010 8:38 PM
+
+...
+> P.S. I have no idea what Randy is on about when he says that the ARG
+> does not like the idea of using Pre and Post conditions for debugging.
+> To me that in practice is the main use. Yes I know about input to
+> formal tools etc, but in practice being able to tell which pre or post
+> condition has failed is quite critical to their usability.
+
+I may have done a lousy job of understanding the thinking; I didn't record much
+about it in the minutes and my reconstruction may have been lacking. Whomever's
+opinion it was (it wasn't mine I'm certain) clearly was compelling enough that
+the entire ARG went along with that thinking.
+
+I always hate it when I find myself defending an ARG decision that I don't have
+a strong opinion on. But I do believe it is part of my job to explain the
+reasoning as I understand it behind ARG decisions (whether or not I agree with
+the decision); that's necessary to avoid ping-ponging between design choices by
+considering only part of the concerns that have been previously discussed. So
+I'll continue to do that, but I'll still probably butcher the intent from
+time-to-time.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Wednesday, August 18, 2010 11:24 PM
+
+> I may have done a lousy job of understanding the thinking; I didn't
+> record much about it in the minutes and my reconstruction may have been lacking.
+> Whomever's opinion it was (it wasn't mine I'm certain) clearly was
+> compelling enough that the entire ARG went along with that thinking.
+
+Since Randy won't take responsibility for this viewpoint (fair enough if it is
+not his :-)), can someone who does subscribe to this viewpoint explain their
+position???
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Sunday, August 22, 2010 2:29 PM
+
+I don't remember the discussion.
+Using pre/post-conditions for debugging
+seems fine to me.
+
+****************************************************************
+
+From: John Barnes
+Sent: Sunday, August 22, 2010 3:26 PM
+
+Indeed. Debugging is always a bugger and anything that helps is great.
+
+****************************************************************
+
From: Florian Weimer
Sent: Saturday, September 25, 2010 2:41 PM
@@ -1311,24 +1453,25 @@
To make a distinction between the 2 cases, you should use Pre'Class in the
first case and Pre in the second case. Robert Dewar has suggested this scheme
where you cannot change in a derived operation what kind of precondition you use
-(whether Pre'Class or Pre) so that you either enforce LSP globally for a primitive
-operation.
+(whether Pre'Class or Pre) so that you either enforce LSP globally for a
+primitive operation.
Here is a summary he sent to the ARG list on 2010/09/08:
-> We keep the oring of inherited Pre'Class aspects, and if there is a
-> Pre'Class for the current subprogram it is also Or'ed in. [GNAT has a
-> nice exception message which shows all the preconditions that have
+> We keep the oring of inherited Pre'Class aspects, and if there is a
+> Pre'Class for the current subprogram it is also Or'ed in. [GNAT has a
+> nice exception message which shows all the preconditions that have
> failed if the or fails.]
->
-> We do not allow the Pre aspect if there is an explicit Pre'Class or
-> any inherited Pre'Class. This avoids the confusion that happens with
-> Or'ing Pre'Class stuff where it is expected, and Pre stuff (where it
+>
+> We do not allow the Pre aspect if there is an explicit Pre'Class or
+> any inherited Pre'Class. This avoids the confusion that happens with
+> Or'ing Pre'Class stuff where it is expected, and Pre stuff (where it
> probably is not)
->
-> For Post, we have no restrictions, Post and Post'Class can both be
-> specified and just get and'ed with any inherited Post'Class aspects.
-> The idea is that no confusion arises in this case, and it is harmless
+>
+> For Post, we have no restrictions, Post and Post'Class can both be
+> specified and just get and'ed with any inherited Post'Class aspects.
+> The idea is that no confusion arises in this case, and it is harmless
> to pile up postconditions (and may well be useful).
+
+****************************************************************
-****************************************************************
\ No newline at end of file
Questions? Ask the ACAA Technical Agent