Re: [boost] [contract] Broken postconditions on throw

Subject: Re: [boost] [contract] Broken postconditions on throw
From: Vicente J. Botet Escriba (vicente.botet_at_[hidden])
Date: 2012-08-28 13:04:51

Le 27/08/12 13:42, Andrzej Krzemienski a écrit :
> 2012/8/27 Andrzej Krzemienski <akrzemi1_at_[hidden]>
>
> I have just found that two years ago when Lorenzo introduced his 
> Contract library I was expecting just the opposite behavior (the 
> current behavior of the library): 
> https://groups.google.com/d/msg/boost-developers-archive/7fEtk3Gdgh0/Dl3lYeraMoUJ 
>
There is a point in this thread I would like to discuss.

" (7)

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?
"

I think both of you agree that providing the sequence {Pre AND 
Initializers} will be better than {Initializers AND Pre},
but we don't know yet how to implement it.

I have not seen yet the code generated by the macros, but one technique 
that maybe could be used is to add a dummy field that will be the first 
of the class.
This parameter will be generated by the CONTRACT_CLASS macro and 
initialized by the generated function evaluating the preconditions.

CONTRACT_CONSTRUCTOR(  // Declare the constructor and its contract.
     public  explicit  (ivector)  (  (size_type)  count  )
         precondition(  count  >=  0  )
         postcondition(
             size()  ==  count,
             boost::algorithm::all_of_equal(begin(),  end(),  0)
         )
         initialize(  vector_(count)  )
)  {}

dummy_type  precondition1(size_type count) {
   if  (count  >=  0  )  return dummy_type();
   else invalidate_contract();
}

ivector(size_type count)

: dummy(precondition1(count),

   vector_(count)
{

// body

// post condition  check

// class invariant check
}

Of course, this has the liability to add an extra field.

The other drawback is that initializer should be split in two parts the 
base class initializers and the field initializers.

Best,
Vicente