CVS difference for ais/ai-00288.txt

Differences between 1.1 and version 1.2
Log of other versions for file ais/ai-00288.txt

--- ais/ai-00288.txt	2002/03/13 00:48:29	1.1
+++ ais/ai-00288.txt	2003/01/03 00:01:36	1.2
@@ -543,3 +543,81 @@
 
 ****************************************************************
 
+From: Tucker Taft
+Sent: Friday, October 18, 2002,  4:00 PM
+
+When we last discussed AI-288, which introduced the concept
+of pre/post condition pragmas (and invariants), we expressed
+concern about the infinite recursion problem, if a two subprograms
+were mutually recursive when the pre/post conditions were
+taken into account.  An example used was:
+
+    function Is_Empty(S : Stack) return Boolean;
+    pragma Postcondition(Is_Empty, not (Is_Empty'Result and Is_Full(S)));
+
+    function Is_Full(S : Stack) return Boolean;
+    pragma Postcondition(Is_Full, not (Is_Full'Result and Is_Empty(S)));
+
+Apparently Eiffel suppresses pre/post conditions when evaluating
+pre/post conditions.  This seems like a kludge, and certainly
+makes implementation significantly harder, since you need
+non-checking versions, and you have to compile pre/post conditions
+using a different mode.
+
+In thinking more about this, the simplest solution seems to be
+"programmer beware."  The above example is not a very good one,
+and perhaps if there were a more convincing example I would
+be more sympathetic, but it seems easy enough for the programmer
+to watch out for these situations.
+
+In general, the functions used in pre/post conditions should
+be pure (or nearly so ;-), and should not have significant
+preconditions of their own.  Postconditions on a function
+seem like somewhat odd beasts in any case, and would probably
+be used sparingly.  They would presumably express properties
+of the returned value such as /= 0, or /= null.   Using them
+to express an identity would seem to be adequately handled
+by having the identity on only one of the functions involved,
+rather than on both.  E.g.
+
+    function "/="(Left, Right : T) return Boolean;
+    pragma Postcondition("/=", "/="'Result = not (Left = Right));
+
+There would seem no need to put the complementary identity
+on the "=" function.
+
+Similarly, one might express the effect of "<", "<=", and ">="
+in terms of ">", but then it would be odd to express the
+effect of ">" in terms of "<", because then you effectively
+have a circular definition.
+
+In any case, in my revision of AI-288 (which will also be
+split into two), I plan to propose to treat the problem of
+infinite recursion for pre/post conditions as the programmer's
+problem, rather than the implementor's problem.
+
+****************************************************************
+
+From: Robert A. Duff
+Sent: Friday, October 18, 2002,  4:31 PM
+
+>   Postconditions on a function
+> seem like somewhat odd beasts in any case, and would probably
+> be used sparingly.  They would presumably express properties
+> of the returned value such as /= 0, or /= null.
+
+Please explain why they are "odd beasts".  I agree that they normally
+"express properties of the returned value".  But why are the examples
+"/= 0, or /= null" usual?  Why not properties expressed in terms of the
+input parameters?
+
+> In any case, in my revision of AI-288 (which will also be
+> split into two), I plan to propose to treat the problem of
+> infinite recursion for pre/post conditions as the programmer's
+> problem, rather than the implementor's problem.
+
+That seem wise.  I can't think of any better way to deal with mutual
+recursion.
+
+****************************************************************
+

Questions? Ask the ACAA Technical Agent