|
|
Boost : |
Subject: Re: [boost] [contract] Without the macros
From: Lorenzo Caminiti (lorcaminiti_at_[hidden])
Date: 2016-06-27 13:48:41
Sorry for the many code examples in this reply... but I think they
illustrate the topics better than my English ;)
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]>:
>
>> Preconditions are evaluated after local object's destructors.
Andrzej, thanks for clarifying (to me in a separate email) that this
means "postconditions should be evaluated after local object
destruction". That is indeed what Boost.Contract does and it is
necessary because in C++ non-trivial destructors can actively
participate to establishing postconditions (using RAII, etc.). For
example:
void fswap(file& x, file& y) // (A)
[[requires: x.closed() && y.closed()]]
[[ensures: x.closed() && y.closed()]]
[[ensures: x == oldof(y) && y == oldof(x)]]
{
x.open();
scope_exit close_x([&x] { x.close(); });
y.open();
scope_exit close_y([&y] { y.close(); });
file t = file::temp();
t.open();
scope_exit close_t([&t] { t.close(); });
x.mv(t);
y.mv(x);
t.mv(y);
}
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:
void fswap(file& x, file& y)
[[requires: x.closed() && y.closed()]]
{
file old_x = x;
file old_y = y;
x.open();
scope_exit close_x([&x] { x.close(); });
y.open();
scope_exit close_y([&y] { y.close(); });
file t = file::temp();
t.open();
scope_exit close_t([&t] { t.close(); });
x.mv(t);
y.mv(x);
t.mv(y);
[[assert: x.closed() && y.closed()]] // Fails! (Established by
local dtors).
[[assert: x == old_y && y == old_x]]
}
To make old value emulation work here [[assert]] would need to also be
programmed in a scope_exit:
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]]
});
x.open();
scope_exit close_x([&x] { x.close(); });
y.open();
scope_exit close_y([&y] { y.close(); });
file t = file::temp();
t.open();
scope_exit close_t([&t] { t.close(); });
x.mv(t);
y.mv(x);
t.mv(y);
}
Now that's a lot of boiler-plate code to program manually for a
language that has native support for an [[ensure]] statement. I really
would expect to be able to do something like (A) above in a language
that supports [[ensures]].
Of course, when you introduce old values then there is the question of
what to do in template code when the generic type of an old value
expression might be copy constructible some times, but not all the
times. Boost.Contract allows programmers to use a type
old_ptr_noncopyable<T> that will copy the old value in the pointer if
T is copy constructible, otherwise it will leave the pointer null
(without generating a compiler error). Then programmers can assert
postconditions that use that old value only if the related pointer is
not null. For example:
template<typename T>
void accumulate(T& total, T const& x) {
// No compiler error if T has no copy constructor...
boost::contract::old_ptr_noncopyable<T> old_total =
BOOST_CONTRACT_OLDOF(total);
boost::contract::guard c = boost::contract::function()
.postcondition([&] {
// ...but old value null if T has no copy constructor.
if(old_total) BOOST_CONTRACT_ASSERT(total == *old_total + x);
})
;
total += x;
}
If programmers decide to use old_ptr<T> instead then Boost.Contract
will generate a compiler error if T is not copy constructible (and
that might be a fare way to program contracts as well in some cases,
it's up to the programmers).
With language support something similar could be done if some sort of
static-if could be used within contract assertions (this is not a full
blown static-if which was rejected already for C++... it'd just be a
static-if to be used in contract assertions):
template<typename T>
void accumulate(T& total, T const& x)
[[ensures: static if(is_copyable<T>::value) total == oldof(total) + x]]
{
total += x;
}
Otherwise, if static-if could not be added to contracts (because too
controversial, etc.), assuming Boost.Contract call_if/check_if
facility and generic lambdas can be used from contract assertions the
following could be done (a bit more verbose then the static-if
version):
template<typename T>
void accumulate(T& total, T const& x)
[[ensures:
check_if<is_copyable<T> >(bind([] (auto total, auto x) {
return total == oldof(total) + x;
}, cref(total), cref(x)))
]]
{
total += x;
}
Note that similar issues arise with contract assertions for templates
in general. These issues are not limited to the copy constructible
requirement introduced by old values, they are in fact about all the
extra type requirement introduced by the operations used to program
contract assertions. So if old values are considered controversial for
templates because of they introduce the copy constructible
requirement, then all assertions (including [[requires]]) should be
considered controversial for templates because they introduce
additional requirements on the generic types used to program the
assertions. For example, `vector<T>::push_back(value)` postcondition
`back() == value` introduces the extra requirement that T must have
operator== while vector<T> only requires T to be copyable (you can
imagine similar examples for preconditions). The good news is that
this can also be handled with static-if:
template<typename T>
class vector {
public:
void push_back(T const& value)
...
[[ensures: static if(has_equal_to<T>::value) back() == value]]
{
vect_.push_back(value);
}
...
};
Again, if static-if is too controversial to be added, Boost.Contract
call_if/check_if and generic lambdas can do the trick (but more
verbose):
template<typename T>
class vector {
public:
void push_back(T const& value)
...
[[ensures:
check_if<has_equal_to<T> >(bind([] (auto back, auto value) {
return back == value;
}, cref(back()), cref(value)))
]]
{
vect_.push_back(value);
}
...
};
Finally, that is indeed what Boost.Contract does:
template<typename T>
class vector {
public:
void push_back(T const& value) {
boost::contract::guard c = boost::contract::public_function(this)
/* ... */
.postcondition([&] {
// Instead of `ASSERT(back() == value)` to handle T no `==`.
BOOST_CONTRACT_ASSERT(
boost::contract::check_if<boost::has_equal_to<T> >(
boost::bind(std::equal_to<T>(),
boost::cref(back()),
boost::cref(value)
)
)
);
})
;
vect_.push_back(value);
}
/* ... */
};
In summary:
(1) The extra copy constructible type requirement introduced by old
values for templates is just an example for the larger (and arbitrary)
set of extra type requirements that contract assertions (even just
preconditions) can introduce in a program.
(2) Programmers can let the program fail to compile if such extra type
requirements are not met (because contracts cannot be checked so
programmers can decide the program should not even compile and that is
one approach). Or, programmers can chose to selectively disable
compilation of contract assertions that introduce the extra type
requirements using static-if (or its emulation via Boost.Contract
call_if/check_if).
That is what Boost.Contract currently does. P0380 could do the same
(and support old values, also because again the extra type requirement
problem is not limited to old values as indicated in (1) above).
Thanks.
--Lorenzo
Boost list run by bdawes at acm.org, gregod at cs.rpi.edu, cpdaniel at pacbell.net, john at johnmaddock.co.uk