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

Subject: Re: [boost] [contract] Broken postconditions on throw
From: Lorenzo Caminiti (lorcaminiti_at_[hidden])
Date: 2012-08-28 13:57:28

On Tue, Aug 28, 2012 at 10:04 AM, Vicente J. Botet Escriba
<vicente.botet_at_[hidden]> wrote:
> 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.

Where do the docs say the above? That's incorrect...

In the Contract Programming Overview section, the docs say:

http://contractpp.svn.sourceforge.net/viewvc/contractpp/releases/contractpp_0_4_1/doc/html/contract__/contract_programming_overview.html#contract__.contract_programming_overview.constructor_calls

``
A constructor call executes the following steps:

1. Check the constructor preconditions.
2. Initialize base classes and members executing the constructor
member initialization list if present.
3. Check the static class invariants (but not the non-static class invariants).
4. Execute the constructor body.
5. Check the static class invariants (even if the body throws an exception).
6. Check the non-static class invariants, but only if the body did not
throw an exception.
7. Check the constructor postconditions, but only if the body did not
throw an exception.

Preconditions are checked before initializing base classes and members
so that these initializations can relay on preconditions to be true
(for example to validate constructor arguments before they are used to
initialize member variables). C++ object construction mechanism will
automatically check base class contracts when subcontracting.
''

Preconditions are checked before initializers (but static class
invariants are not). That's in the spirit of N1962 (even if not
explicitly stated as clarified by Thorsten a couple of years back in
this ML, we all discussed this together). It wasn't at all easy to
implement this... but it should work correctly now :D (essentially, I
use and extra base class that is initlialized before anything else,
pass it the pointer to the static member function that checks
preconditions, and the base class constructor calls the function so it
checks the pre).

> 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.

Thanks,
--Lorenzo