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

--- ai05s/ai05-0145-2.txt	2010/10/19 00:38:38	1.11
+++ ai05s/ai05-0145-2.txt	2010/10/26 05:39:47	1.12
@@ -1275,4 +1275,59 @@
 (At first I was thinking that the level had something to do with the point of
 calls, but that was confused.  Accessibility is often that way...)
 
+****************************************************************
+
+From: Florian Weimer
+Sent: Saturday, September 25, 2010  2:41 PM
+
+To me, the decision to use disjunction for multiple preconditions seems rather
+strange.  I have never seen this approach before, and I expect that most
+programmers will assume that the preconditions are "and"ed together.
+
+****************************************************************
+
+From: Yannick Moy
+Sent: Monday, September 27, 2010  4:46 AM
+
+Note that you cannot define more than one precondition directly on a subprogram.
+Thus, to have more than one condition here you must conjoin them:
+
+procedure F with Pre => Cond_1 and then Cond_2 and then ...;
+
+Hence, the case where you have multiple preconditions corresponds to inherited
+preconditions on a primitive operation. Here, you must be careful that the
+subprogram could be called as a result of a dispatching operation.
+
+In order to respect the Liskov Subtitutability Principle (LSP), you would want
+the precondition on the derived operation to be weaker than the precondition
+on the inherited operation. This calls for or'ing the explicit precondition
+on the derived operation with the ones it inherits.
+
+But you may as well not want to enforce the LSP, in which case you don't want
+such or'ing of preconditions, and you'd rather use only the direct precondition
+on the derived operation.
+
+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.
+
+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 
+> 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 
+> 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 
+> to pile up postconditions (and may well be useful).
+
 ****************************************************************