Re: [boost] [contract] Contract Programming Library
The documentation lists the following sequence for executing a constructor:
1. Initialize member variables via the constructor member initialization list (if such a list is specified). 2. Check preconditions (but not invariants). 3. Execute constructor body. 4. Check invariants. 5. Check postconditions.
I believe, one of the reasons for validating arguments of a constuctor is to not allow the incorrect values to initialize objest's sub-objects (members). I believe the sequence of the first two items should be inverse. Am I wrong?
The library follows Eiffel semantics for constructor which is {Default AND Pre}Body{Post AND Inv} where Default is default initialization of members (similar to C++ member initialization list). That said, it would be difficult to implement a different semantics (like the one you suggest) in C++ because of the lack of delegating constructors.
The sole fact that other language implements it this way is not sufficient an argument. I can think of the situation when "Eiffel order" may cause damage that the inverse order might have prevented: Type::Type( int & counter ) precondition{ counter < MAX; } : handle( irreversibleChange(int--) ) { ; } Suppose the constructor of Type is called, and the value of counter is MAX. This value is invalid, but by the time the precondition is checked, the irreversibleChange is executed, and the value of counter is reduced, so the assertion concludes that everything is fine. Now, the argument that it is difficult to implement is convincing; it may be that it is impossible at all. But I would call not having the {Pre->Init} order a limitation of the library. Let me be clear: one tiny limitation in the great library, because out of many attempts to provide contract programming to C++ I have seen, this is the only one that really looks good. Regards, &rzej
Hello Andrzej, On Fri, Feb 19, 2010 at 1:16 PM, Andrzej Krzemienski <akrzemi1@gmail.com> wrote:
The sole fact that other language implements it this way is not sufficient an argument. I can think of the situation when "Eiffel order" may cause damage that the inverse order might have prevented:
Type::Type( int & counter ) precondition{ counter < MAX; } : handle( irreversibleChange(int--) ) { ; }
Suppose the constructor of Type is called, and the value of counter is MAX. This value is invalid, but by the time the precondition is checked, the irreversibleChange is executed, and the value of counter is reduced, so the assertion concludes that everything is fine. Now, the argument that it is difficult to implement is convincing; it may be that it is impossible at all. But I would call not having the {Pre->Init} order a limitation of the library. Let me be clear: one tiny limitation in the great library, because out of many attempts to provide contract programming to C++ I have seen, this is the only one that really looks good.
I understand your point. Let me spend a few more words on the issue. 1) The library has a limitation in dealing with constructor initialization lists already. The one limitation currently known and _documented_ is that if a construct uses member initialization list, the constructor body definition cannot be separated from the body declaration (as long as you want to code to still compile when contract compilation is turned off completely). I have looked at this limitation and it appears to me that if delegating constructors were to be supported by C++ as proposed in [Sutter2005] then the library *could* be able to overcome the limitation (but I cannot really be sure until I try it...). 2) I think, implementing {Pre AND Default} instead of {Default AND Pre} without delegating constructors would raise very similar issues as for 1). Eiffel requirements is {Default AND Pre} but constructors in Eiffel are different from C++ so your are correct that I should not simply "copy" the Eiffel requirement if it does not make sense for C++. 3) If irreversibleChange(count--) could be performed by the constructor body (instead of the member initialization list, maybe handle is set to 0 by the initialization list...) then the preconditions will be checked before irreversibleChange(count--). However, I understand that for some code maybe the irreversibleChange(count--) call really has to happen in the member initialization list... In short, could the code be restructured to call irreversibleChange(count--) from within the body of a constructor/function/etc? However, this would be a workaround to the library limitation that {Pre AND Default} cannot be supported (limitation which should be documented). In summary, I will study {Pre AND Default} more. I will look in detail at why Eiffel does {Default AND Pre}. Also, [Crowl2006] requires: "Constructors behave much like member functions. This means that a constructor can have a precondition and a postcondition. The precondition may not reference member variables." (from [Crowl2006]) but I will also look at all older revisions of this proposal to see if member initialization list requirements are explicitly mentioned. If this {Pre AND Default} is the best requirement for C++ Contract Programming, I will document {Default AND Pre} as a library limitation (and if not, I will document why {Default AND Pre} is good). Thank you for your valuable comments. Lorenzo
participants (2)
-
Andrzej Krzemienski -
Lorenzo Caminiti