Re: [boost] [contract] diff n1962

Subject: Re: [boost] [contract] diff n1962
From: vicente.botet (vicente.botet_at_[hidden])
Date: 2010-04-11 10:58:31

----- Original Message ----- 
From: "Lorenzo Caminiti" <lorcaminiti_at_[hidden]>
To: <boost_at_[hidden]>
Sent: Sunday, April 11, 2010 4:16 PM
Subject: Re: [boost] [contract] diff n1962

Hello all,

On Thu, Apr 8, 2010 at 7:26 PM, Lorenzo Caminiti <lorcaminiti_at_[hidden]> wrote:
> Below is a summary of the differences between Boost.Contract and the
> Contract Programming C++ standard proposal n1962. I know some of the
> authors of n1962, and also of its previous revisions, are on this
> mailing list -- I hope that they can provide comments at least.

Thank you very much for all your replies. I will address your comments
and modify Boost.Contract as needed. Before that however, I have one
additional question on constructors -- for everyone and again
especially for the n1962 authors.

CONSTRUCTORS
Does n1962 require constructor preconditions to be checked before or
after the execution of the member initialization list?

>From n1962 section 4.2.2: <<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.>>.

Boost.Contract checks preconditions after the member initialization:
member-init > static-inv > pre > body > static-inv > inv > post.
However, when asked why I could not really come up with an explanation
but that it would be difficult to implement Boost.Contract
differently...

Eiffel checks "default" > pre > body > inv > post. Where "default"
essentially means that member variables are in a default state. I
think, this is similar to executing the member initialization before
checking preconditions but not quite the same because default member
values for Eiffel are essentially just Void. C++ instead can assign
more complex values in the member initialization list. Because these
values can be functions of the constructor input parameters, you can
make the argument that C++ preconditions should be checked before the
member initialization list so to validate the constructor parameters
before they are used to initialize the members.

Thank you.
Lorenzo
_______________________________________________

Hi Lorenzo,
I supose that the constructor preconditions are evaluated before the  member initialization as this initialization can rely on the preconditions been satisfied. Note also that preconditions/postconditions must to be in the declaration part, and the member initialization is on the definition part.

I understand that it is not easy for Boost.Contract to check the precondition before member initialization . To be able to do that you will need to have a first member or inherit from a 'precondition' class that do this precondition check, 

class C : C_constructor_precondition ... {

  C(T1 p1) : C_constructor_precondition(p1), ... {
    // ...
  }
};

but this seems to me a severe constraint and adds more complexity. I think that I can live with preconditions check after member initialization.

Best,
_____________________
Vicente Juan Botet Escribá
http://viboes.blogspot.com/