Re: [boost] [contract] Without the macros

Subject: Re: [boost] [contract] Without the macros
From: Lorenzo Caminiti (lorcaminiti_at_[hidden])
Date: 2016-06-30 10:25:56

On Mon, Jun 27, 2016 at 10:48 AM, Lorenzo Caminiti
<lorcaminiti_at_[hidden]> wrote:
> On Fri, Jun 24, 2016 at 3:49 PM, Lorenzo Caminiti <lorcaminiti_at_[hidden]> wrote:
>> On Fri, Jun 24, 2016 at 2:43 PM, Andrzej Krzemienski <akrzemi1_at_[hidden]> wrote:
>>> 2016-06-15 17:30 GMT+02:00 Lorenzo Caminiti <lorcaminiti_at_[hidden]>:
>>
> <snip>
>     void fswap(file& x, file& y) // (A)
>         [[requires: x.closed() && y.closed()]]
>         [[ensures: x.closed() && y.closed()]]
>         [[ensures: x == oldof(y) && y == oldof(x)]]
> <snip>
> That is also why P0380 should add old value support... that is because
> the above cannot be emulated using [[assert]] like suggested in P0380
> at page 10:
> <snip>
>
>     void fswap(file& x, file& y)
>         [[requires: x.closed() && y.closed()]]
>     {
>         file old_x = x;
>         file old_y = y;
>         scope_exit ensures([&] {
>             [[assert: x.closed() && y.closed()]]
>             [[assert: x == old_y && y == old_x]]
>         });

I forgot to note that even the above is not sufficient because:
1. Postconditions should not be checked if the function body throws so
the above lambda should be programmed to check the [[assert]]s only if
there is no active exception (Boost.Contract does that).
2. The old value copies are not removed from the code when
postconditions compilation and checking is disabled (Boost.Contract
will remove the old copies leaving the related old pointers null in
that case).
3. The postcondition [[assert]]s no longer appear in the function
declarations where contracts ideally belong (Boost.Contract also
suffers of this limitation).
The above reasons should reinforce the fact that old values cannot
really be "emulated" as suggested in P0380 page 10 thus old values
should be added to the core language together with [[ensures]] if at
all possible.

Thanks.
--Lorenzo