Re: [boost] [contract] Without the macros

On Mon, Jun 27, 2016 at 10:48 AM, Lorenzo Caminiti wrote:

On Fri, Jun 24, 2016 at 3:49 PM, Lorenzo Caminiti wrote:

...

On Fri, Jun 24, 2016 at 2:43 PM, Andrzej Krzemienski wrote:

...

2016-06-15 17:30 GMT+02:00 Lorenzo Caminiti :

<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