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@gmail.com> wrote:
On Fri, Jun 24, 2016 at 2:43 PM, Andrzej Krzemienski <akrzemi1@gmail.com> wrote:
2016-06-15 17:30 GMT+02:00 Lorenzo Caminiti <lorcaminiti@gmail.com>:
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; } https://lcaminiti.github.io/boost-contract/doc/html/boost_contract/advanced_... 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; } https://lcaminiti.github.io/boost-contract/doc/html/boost_contract/advanced_... 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); } /* ... */ }; https://lcaminiti.github.io/boost-contract/doc/html/boost_contract/advanced_... 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