Re: [boost] [contract] Contract Programming Library

Subject: Re: [boost] [contract] Contract Programming Library
From: Lorenzo Caminiti (lorcaminiti_at_[hidden])
Date: 2010-01-09 14:20:26

Hi Vicente:

On Thu, Jan 7, 2010 at 8:30 AM, Vicente Botet Escriba
<vicente.botet_at_[hidden]> wrote:
> I understand that this will not help the compiler to optimize, but why use a
> different technique to test the invariants of block? Why don't follow the
> C++ proposal in this case?

Yes, I have added to look into block invariants to the library TODOs.

As I said, it should be possible to implement block invariants,
essentially just by handling BOOST_CONTRACT_ASSERT() within the block
it self:

    void foo() {
        int i = 0;
        for(;;)
        BOOST_CONTRACT_BLOCK({
            BOOST_CONTRACT_ASSERT(i < 10, "i less than 10");
            ...
        })
    }

IMPLEMENTATION: The BOOST_CONTRACT_BLOCK() macro wraps the block with
a try-catch statement to that will handle a boost::contract::failure
exception invoking boost::contract::block_invariant_failed() (which
will in turn terminate by default but can be redefined by the user).
This would be very similar to the CP C++ Standard Proposal
[Crowl2006].

> Imagine a class that is able to implement the ConstCopyConstructor but that
> don't wants to provide it to its users. This class can implement let me say
> a ContractCopyConstructor like
>
>  C(C const& rhs, backup_t);
>
> When this constructor is defined your library could use it instead of the
> missing ConstCopyConstructor.
>
> We can go one step ahead an require from a class C that can be used on the
> post-condition of a function that there is another class with the same
> interface than C that can be copied from  a const reference to C.
>
> Given the following trait
>
> template <typename T>
> struct backup {
>  typedef T type;
> };
>
> You can request instead of C(C const&)
>
> backup<C>::type(C const&);
>
> If a class C has a backup D, we will add the following specialization
>
> template <>
> struct backup<C> {
>  typedef D type;
> };
>
>
> This has some advantages:
> * separates the creation of real instances from the needed by your library.
> Thus avoiding the call to the CopyCOnstructor and destructor of the class
> which can have non desirable side effects.
> * allow to work with non-copyable classes
> * the user of your library could reduce the scope of operations used on this
> backup class making it more efficient, for example reducing the backed up
> fields or the implemented functions
> * the user can promote private or protected members to public.
>
> Of course this has also some liabilities:
> * the user needs to implement an additional class (optionally)
>
> At the end the default behavior of my design corresponds to your current
> behavior, letting the user the possibility to use more classes on the
> post-condition part. Can this design be adapted to your library?

I see. Yes, this should be possible and I made a note in the library
TODOs to experiment with this idea.

> Just a last question, does your library avoid the evaluation of other
> contracts during execution of the post-condition?

No, but this is a policy question and the implementation could be
changed if needed.

The library should have enough internal infrastructure so that
assertion checking can be disabled when needed (usually in order to
avoid infinite recursion). The current policy that I have implemented
follows the CP C++ Standard Proposal rev 1 [Ottosen2004]:
    1) All assertions are disabled globally when any other assertion
is being checked already.
    2) In nested function calls of the same object, only invariant
checking is disabled.
Both Eiffel and the latest rev of the CP C++ Standard Proposal
[Crowl2006] takes a different approach -- see Feature table of library
documentation.

In my CP projects, [Ottosen2004] policy has been more effective than
[Crowl2006] in preventing infinite recursion. Plus [Ottosen2004] is
closer to (but in my experience better than) Eiffel's policy.
(Actually, [Crowl2006] policy would be easier to implement for the
library.)

I would like to discuss this point more and especially understand the
reason / use case for changing this policy from [Ottosen2004] to
[Crowl2006].

Regards,
Lorenzo