Re: [boost] [contract] diff n1962

Subject: Re: [boost] [contract] diff n1962
From: vicente.botet (vicente.botet_at_[hidden])
Date: 2010-04-12 06:38:49

----- Original Message ----- 
From: "Lorenzo Caminiti" <lorcaminiti_at_[hidden]>
To: <boost_at_[hidden]>
Sent: Monday, April 12, 2010 5:27 AM
Subject: Re: [boost] [contract] diff n1962

Hello,

On Sun, Apr 11, 2010 at 12:35 PM, vicente.botet
<vicente.botet_at_[hidden]> wrote:
> From: "Steven Watanabe" <watanabesj_at_[hidden]>
>>> Finally, the use of CONTRACT_OLDOF(variable) requires programmers to
>>> explicitly indicate that the variable type is copyable using
>>> (copyable) in the function signature adding syntactic overhead.
>>
>> This kind of worries me. Do you always make a copy
>> whether it's needed or not when the object is marked
>> as copiable?

However, why does this worry you? If programmers do not need
CONTRACT_OLDOF() then they simply do not tag the type (copyable) and
there is no overhead. Note that the (copyable) is used within the
function contract, so the object can be (and should be) tagged
(copyable) only for the member functions that use
CONTRACT_OLDOF(this).

Let me explain:
1) Yes, Boost.Contract always makes a copy whether it is needed of not
for object and arguments that are tagged (copyable).
2) Boost.Contract documentation explains that programmers should tag a
type (copyable) only when (a) the relative variable old value
CONTRACT_OLDOF(variable-name) is used in postconditions and (b) the
type has a constant correct copy constructor.
3) Boost.Contract will generate a compile-time error if
CONTRACT_OLDOF() is used on a variable not tagged (copyable) and/or
the tagged type does not have the constant-correct copy constructor.
4) Boost.Contract cannot detect if a variable tagged (copyable) is not
used in postconditions by CONTRACT_OLDOF() in which case the copy and
relative run-time overhead will be wasted.

Ideally, Boost.Contract will be able to automatically detect if
CONTRACT_OLDOF(variable-name) is used in postconditions, then tag the
related type (copyable) at compile-time, and therefore make the copy
at run-time. This is exactly why I was asking if is_macro_called() can
be implemented but it seems that it is not possible...

> What do you think of storing in specific variables the old values and use them on the post condition.
> (postcondition)((old_size) (this)->size())) ({
> CONTRACT_ASSERT( size() == (old_size + 1) );
> })
>
> This has the advantage that only the used old values are copied.
> Do you see another alternative?

This option suggested by Vicente should be feasible but it complicates
the syntax. (Eventually, I like the old variable to follow
(postcondition) as suggested here instead that being after the
function signature.)

_______________________________________________

VBE>I think that what worries Steven is that we need to state explicitly if a given variable must be copied. Maybe the library can provide a mode on which the copies are done always (maybe a trait class could be used to select which one must be copied), so no need to add the (copyable) tag. As post conditions are usualy evaluated only on debug mode, the performance degradation could be considered a minor drawback.

>>> 12) CONSTANT-CORRECTNESS
>>> Block invariants are constant-correct in n1962 but not in
>>> Boost.Contract. (Class invariants and pre/postconditions are
>>> constant-correct in both n1962 and Boost.Contract.)
>>>
>>> Unfortunately, I do not know how to enforce constant-correctness of
>>> block invariants (and also of loop variants) for Boost.Contract
>>> because I cannot inject const within a code block:
>>>
>>> class z {
>>> void f() {
>>> const { // Can't do this... so f() is not const and block
>>> invariants are also not const in this context...
>>> ... // block invariant here
>>> }
>>> }
>>> };
>>>
>>> This is a limitation of Boost.Contract.
>>>
>>
>> You can pull the code block out into a separate function.
>>
>
> Yes as Steven says, you can always define a function with the needed const qualifiers that checks for the block invariant. But IMHO this complicates things a lot. I don't think that I will use these kind of functions so help to ensure that Block invariants are constant-correct. This could be a minor and aceptable limitation of a library solution.

One key issue is that is that the const function will have to offer
all the original function arguments, plus local variables, etc because
everything that is in scope can be used by BLOCK_INVARIANT() (in
constant-correct context) to make the assertion:

    class x {
        void f(int a) {
            int b = a;
            CONTRACT_BLOCK_INVARIANT( a == b );
            ...
        }
        ...
    };

How do I expand this to the separate const-correct function call? Of
course programmers can manually program it:

    class x {
        void bool f_check1_(const int& a, const int& b) { return a == b; }

        void f(int a) {
            int b = a;
            CONTRACT_BLOCK_INVARIANT( f_check1_(a, b) );
            ...
        }
        ...
    };

(I tried to do this with classes declared locally within f() where
BLOCK_INVARIANT() is used but I was not able to get it to work because
you still do not see the function arguments, local variables, outer
object `this`, etc.)

_______________________________________________

VBE> Boost.ScopeExit showed a technique that can be used to emulate local functions. Alexander proposed long time ago to provide it independently from ScopeExit but to my knowledge this has not been done. Using this technique Boost.Contract could try to emulate a const function, but I think yet that compicates the syntax for not too much user advantage.
 
_____________________
Vicente Juan Botet Escribá
http://viboes.blogspot.com/