CVS difference for acs/ac-00156.txt

Differences between 1.1 and version 1.2
Log of other versions for file acs/ac-00156.txt

--- acs/ac-00156.txt	2008/01/19 05:28:15	1.1
+++ acs/ac-00156.txt	2008/01/22 06:18:46	1.2
@@ -1653,88 +1653,248 @@
 
 ****************************************************************
 
-From: Robert A. Duff
-Date: Friday, January 11, 2008  1:07 PM
+From: Cyrille Comar
+Date: Saturday, January 19, 2008  12:27 AM
 
-****************************************************************
+>> By this standard (which is a way of favoring the caller view of a
+>> contract) Classwide_Pre_Assert is not enough, you would also need a
+>> Suprogram_Access_Pre_Assert so that you know what are the preconditions
+>> for an indirect call...
+>
+> It has always seemed to me that that was necessary, because in order to
+> write correct calls, you need to know the specification of the call.
 
-From: Robert A. Duff
-Date: Friday, January 11, 2008  1:07 PM
+I was using this argument to show that favoring the caller's view of
+pre/postconditions was not necessarily the way to go but that does not
+seem sufficient so let me push the reasoning one step further: what
+about anonymous access to subprogram parameters? By your standard, they
+are necessary too, right? where do you put them? Isn't it becoming ugly?
 
-****************************************************************
+>  Indeed,
+> that seems to be the primary benefit of precondition/postcondition pragmas
+> over using Asserts inside the subprogram -- that these things are part of
+> the specification.
 
-From: Robert A. Duff
-Date: Friday, January 11, 2008  1:07 PM
+I certainly agree with this but I don't see that it is relevant to the
+point I am making.
 
-****************************************************************
+pre/postconditions form the contract between the caller and the callee
+so theoretically both views are equally important. This contract is what
+will help you catch integration errors (Data Coupling analysis in
+DO-178B terminology)
 
-From: Robert A. Duff
-Date: Friday, January 11, 2008  1:07 PM
+In practice, you often write pre/postconditions when you design reusable
+components. That is to say when you have no idea of who the caller will
+be. So you have the callee view: the precondition is what makes it safe
+to call your routine and the postcondition is what the user can expect
+as a result. So, in this view, the pre/postconditions are really
+properties of the body of your subprogram that you publish as part of
+the spec to inform users. This is a bottom-up approach...
 
-****************************************************************
+If you favor the caller view, as for access_precond and
+classwide_precond,  you basically ask the programmer to write
+pre/postconditions before he knows what will be called. You say: here is
+how I plan to use that stuff, or in the classwide case, here is what
+needs to be true in order to respect LSP, so make sure this it is so
+down the road. So, in a sense, this is more of a top-down approach...
 
-From: Robert A. Duff
-Date: Friday, January 11, 2008  1:07 PM
+In both cases, you have favored on side of the contract, so the errors
+will more likely be on the other side.
 
+I am not saying that one model is "better" than the other but I
+personally prefer the first one because it is simpler and more adapted
+to reusable components.
+
 ****************************************************************
 
-From: Robert A. Duff
-Date: Friday, January 11, 2008  1:07 PM
+From: Randy Brukardt
+Date: Saturday, January 19, 2008  12:55 AM
 
-****************************************************************
+> I was using this argument to show that favoring the caller's view of
+> pre/postconditions was not necessarily the way to go but that does not
+> seem sufficient so let me push the reasoning one step further: what
+> about anonymous access to subprogram parameters? By your standard, they
+> are necessary too, right? where do you put them? Isn't it becoming ugly?
 
-From: Robert A. Duff
-Date: Friday, January 11, 2008  1:07 PM
+I've previously said that I think these should be an integrated part of the
+syntax of a subprogram spec, so *obviously* they go in the same place they
+always do. Is that ugly in the case of anonymous access-to-subprogram? Sure,
+but anonymous access-to-subprograms are always ugly. [These syntax contracts
+probably also should include contracted exceptions, BTW.]
 
-****************************************************************
+What's really ugly is using pragmas for this purpose, especially ones with
+special visibility.
 
-From: Robert A. Duff
-Date: Friday, January 11, 2008  1:07 PM
+Indeed, I proposed user-defined constraints in large part to get some of
+this information into the Ada subprogram specification where it belongs.
 
-****************************************************************
+> >  Indeed,
+> > that seems to be the primary benefit of precondition/postcondition pragmas
+> > over using Asserts inside the subprogram -- that these things are part of
+> > the specification.
+>
+> I certainly agree with this but I don't see that it is relevant to the
+> point I am making.
+>
+> pre/postconditions form the contract between the caller and the callee
+> so theoretically both views are equally important. This contract is what
+> will help you catch integration errors (Data Coupling analysis in
+> DO-178B terminology)
 
-From: Robert A. Duff
-Date: Friday, January 11, 2008  1:07 PM
+Yes, which is why they should be an integral part of the specification; then
+they'll actually appear on both halves. Having them on just one side or the
+other is not a help.
 
-****************************************************************
+> In practice, you often write pre/postconditions when you design reusable
+> components. That is to say when you have no idea of who the caller will
+> be. So you have the callee view: the precondition is what makes it safe
+> to call your routine and the postcondition is what the user can expect
+> as a result. So, in this view, the pre/postconditions are really
+> properties of the body of your subprogram that you publish as part of
+> the spec to inform users. This is a bottom-up approach...
+>
+> If you favor the caller view, as for access_precond and
+> classwide_precond,  you basically ask the programmer to write
+> pre/postconditions before he knows what will be called. You say: here is
+> how I plan to use that stuff, or in the classwide case, here is what
+> needs to be true in order to respect LSP, so make sure this it is so
+> down the road. So, in a sense, this is more of a top-down approach...
+>
+> In both cases, you have favored on side of the contract, so the errors
+> will more likely be on the other side.
+>
+> I am not saying that one model is "better" than the other but I
+> personally prefer the first one because it is simpler and more adapted
+> to reusable components.
 
-From: Robert A. Duff
-Date: Friday, January 11, 2008  1:07 PM
+We absolutely have to support both. The language shouldn't be favoring one
+kind of development over another. Indeed, I've developed components both
+ways.
+
+Besides that, there isn't much value to a new language feature for the
+bottom-up approach. Pragma Assert works just fine. It's the top-down
+approach where the benefits really begin to show.
 
 ****************************************************************
 
 From: Robert A. Duff
-Date: Friday, January 11, 2008  1:07 PM
+Date: Saturday, January 19, 2008  7:57 AM
 
-****************************************************************
+> In practice, you often write pre/postconditions when you design reusable
+> components. That is to say when you have no idea of who the caller will be.
 
-From: Robert A. Duff
-Date: Friday, January 11, 2008  1:07 PM
+In this case, the contract is not negotiated between equal parties.  It's more
+like a license you get with shrink-wrapped software -- clients have to take it
+or leave it (more or less).
+
+;-)
 
 ****************************************************************
 
 From: Robert A. Duff
-Date: Friday, January 11, 2008  1:07 PM
+Date: Saturday, January 19, 2008  8:02 AM
 
-****************************************************************
+...
+> Besides that, there isn't much value to a new language feature for the
+> bottom-up approach. Pragma Assert works just fine. It's the top-down
+> approach where the benefits really begin to show.
 
-From: Robert A. Duff
-Date: Friday, January 11, 2008  1:07 PM
+I don't agree that pragma Assert works just fine.  There are advantages to
+putting the precondition on the spec -- more likely that static proofs can
+work, for example.
 
 ****************************************************************
 
-From: Robert A. Duff
-Date: Friday, January 11, 2008  1:07 PM
+From: Arnaud Charlet
+Date: Saturday, January 19, 2008  8:06 AM
 
-****************************************************************
+> I don't agree that pragma Assert works just fine.  There are advantages to
+> putting the precondition on the spec -- more likely that static proofs can
+> work, for example.
 
-From: Robert A. Duff
-Date: Friday, January 11, 2008  1:07 PM
+Plus the fact that some users want to be able to enable/disable preconditions
+without disabling/enabling all other assertions (or postconditions).
+
+It also gives more freedom to the compiler, to decide whether it makes more
+sense to generate the precondition check at the caller or callee side.
+It also makes sure that the user doesn't put the pre-condition at the wrong
+place.
 
 ****************************************************************
 
-From: Robert A. Duff
-Date: Friday, January 11, 2008  1:07 PM
+From: Randy Brukardt
+Date: Saturday, January 19, 2008  9:09 PM
 
+> > Besides that, there isn't much value to a new language feature for the
+> > bottom-up approach. Pragma Assert works just fine. It's the top-down
+> > approach where the benefits really begin to show.
+>
+> I don't agree that pragma Assert works just fine.  There are advantages to
+> putting the precondition on the spec -- more likely that static proofs can
+> work, for example.
+
+You can't usefully do anything at the call site with his bottom-up approach,
+because you don't know the preconditions in general (dispatching,
+access-to-subprogram, etc.). Moreover, with his approach, the preconditions
+are going to be in a constant state of flux, so they can't be depended on
+and shouldn't appear to be part of the specification.
+
+But this is a straw man: I don't agree with limiting preconditions to the
+bottom-up case, so I do think they should be in intregral part of the
+specification of *all* subprogram profiles. (And that needs syntax, not
+pragmas, because overloading and anonymous types cause serious problems for
+pragmas).
+
 ****************************************************************
 
+From: Robert Dewar
+Date: Monday, January 21, 2008  10:24 PM
+
+> I've previously said that I think these should be an integrated part of the
+> syntax of a subprogram spec, so *obviously* they go in the same place they
+> always do. Is that ugly in the case of anonymous access-to-subprogram? Sure,
+> but anonymous access-to-subprograms are always ugly. [These syntax contracts
+> probably also should include contracted exceptions, BTW.]
+
+I agree that in the long run some syntax extension might be appropriate.
+
+> What's really ugly is using pragmas for this purpose, especially ones with
+> special visibility.
+
+Doesn't seem so ugly in practice, though it might be nicer if the
+pragmas could go inside the formal part (WHY OH WHY are pragmas
+forbidden inside a formal part?) Anyway, we don't feel like
+inventing new syntax, or waiting for the ARG to do so to get
+this feature off the ground (it is now fully implemented in
+our current build).
+
+Certainly it's easy enough to implement, at least it was for us,
+since we already have these expressions that have to be analyzed
+once for visibility and again for code generation (e.g. default
+expressions), and we already have the mechanism for making formals
+visible in the body, so the code in GNAT to analyze these pragmas
+looks like:
+
+                --  Analyze the pragma appearing in spec
+
+                Install_Formals (S);
+                Push_Scope (S);
+
+                Analyze_Per_Use_Expression
+                  (Get_Pragma_Arg (Arg1), Standard_Boolean);
+
+                if Arg_Count = 2 then
+                   Analyze_Per_Use_Expression
+                     (Get_Pragma_Arg (Arg2), Standard_String);
+                end if;
+
+                End_Scope;
+
+P.S. Per_Use_Expression is an ugly name, I am going to think of a better
+one now that this is used for
+
+   default expressions
+   per use stuff (e.g. pragmas in tasks)
+   preconditions and postconditions
+
+****************************************************************

Questions? Ask the ACAA Technical Agent