Re: [boost] [contract] Contract Programming Library

Subject: Re: [boost] [contract] Contract Programming Library
From: Lorenzo Caminiti (lorcaminiti_at_[hidden])
Date: 2010-02-19 20:09:51

Hello Andrzej,

On Fri, Feb 19, 2010 at 1:16 PM, Andrzej Krzemienski <akrzemi1_at_[hidden]> 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