[contract] Without the macros
Hello all, In the last few years my professional and personal lives changed quite a bit limiting my ability to contribute to Boost. However, in my spare time I slowing continued to revise Boost.Contract hoping to be able to commit it to a Boost release someday (after the library was accepted 3+ years ago... https://groups.google.com/forum/?fromgroups=#!topic/boost-list/jQ7OjAmos_Y). While doing so I realized that leveraging C++11 lambda functions, Boost.Contract could be re-implemented without its crazy macros that alter C++ function declaration syntax. Boost.Contract still remains the only C++ library that implements *all* features of Contract Programming (a.k.a., Design by Contract or DbC): subcontracting, class invariants (also static and volatile), postconditions (with old and return values), preconditions, customizable actions on assertion failure (terminate, throw, etc.), optional assertion compilation, disable assertion checking while already checking other assertions (to avoid infinite recursion), etc. Furthermore, in its new incarnation Boost.Contract no longer uses crazy macros so it is easier to use, faster to compile, and gives readable compiler errors. For example: #include <boost/contract.hpp> int inc(int& x) { int result; boost::contract::old_ptr<int> old_x = BOOST_CONTRACT_OLDOF(x); boost::contract::guard c = boost::contract::function() .precondition([&] { BOOST_CONTRACT_ASSERT(x < std::numeric_limits<int>::max()); }) .postcondition([&] { BOOST_CONTRACT_ASSERT(x == *old_x + 1); BOOST_CONTRACT_ASSERT(result == *old_x); }) ; return result = x++; // Function body. } Or with subcontracting: #include <boost/contract.hpp> #include <vector> template<typename T> class pushable; // Arbitrary base to demo subcontracting. template<typename T> class vector #define BASES public pushable<T> : BASES { public: typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; // Subcontracting. #undef BASES void invariant() const { // Checked in AND with base class invariants. BOOST_CONTRACT_ASSERT(size() <= capacity()); // Line 25. } virtual void push_back(T const& value, boost::contract::virtual_* v = 0) /* override */ { boost::contract::old_ptr<unsigned> old_size = BOOST_CONTRACT_OLDOF(v, size()); // Old values. boost::contract::guard c = boost::contract::public_function< override_push_back>(v, &vector::push_back, this, value) .precondition([&] { // Checked in OR with base preconditions. BOOST_CONTRACT_ASSERT(size() < max_size()); // Line 35. }) .postcondition([&] { // Checked in AND with base postconditions. BOOST_CONTRACT_ASSERT(size() == *old_size + 1); // Line 38. }) ; vect_.push_back(value); // Function body. } BOOST_CONTRACT_OVERRIDE(push_back) // For `override_push_back`. // Could program contracts for those as well. unsigned size() const { return vect_.size(); } unsigned max_size() const { return vect_.max_size(); } unsigned capacity() const { return vect_.capacity(); } private: std::vector<T> vect_; }; Full documentation and examples at: https://lcaminiti.github.io/boost-contract What do you think? Thanks, --Lorenzo P.S. The library can also be used without C++11 lambda functions (or any C++11 specific feature) but programmers have to write a fare amount of extra code to program the precondition and postcondition functors (using non-local functions, Boost.LocalFunction, Boost.Funsion, Boost.Lambda, or some other approach) so that might not useful in practice.
On Jun 15, 2016 08:31, "Lorenzo Caminiti" <lorcaminiti@gmail.com> wrote:
Hello all,
In the last few years my professional and personal lives changed quite a bit limiting my ability to contribute to Boost. However, in my spare time I slowing continued to revise Boost.Contract hoping to be able to commit it to a Boost release someday (after the library was accepted 3+ years ago... https://groups.google.com/forum/?fromgroups=#!topic/boost-list/jQ7OjAmos_Y
).
While doing so I realized that leveraging C++11 lambda functions, Boost.Contract could be re-implemented without its crazy macros that alter C++ function declaration syntax.
Awesome to hear that Boost.Contract is still going! I can't wait to take a look. Have you followed any of the recent papers regarding language-level contracts for C++?
Hi Matt! On Wed, Jun 15, 2016 at 8:47 AM, Matt Calabrese <rivorus@gmail.com> wrote:
On Jun 15, 2016 08:31, "Lorenzo Caminiti" <lorcaminiti@gmail.com> wrote: Have you followed any of the recent papers regarding language-level contracts for C++?
No... but I should definitely take a look! Do you have a link to the proposal to get me started? Of course, language support for Contract Programming remains the ultimate solution even if Boost.Contract no longer uses crazy macros (if not for anything else, because language support would provided a more concise syntax, compiler optimizations, and put the contracts with function declaration instead of definitions). Thanks, --Lorenzo
On 15 June 2016 at 23:15, Lorenzo Caminiti <lorcaminiti@gmail.com> wrote:
On Wed, Jun 15, 2016 at 8:47 AM, Matt Calabrese <rivorus@gmail.com> wrote:
On Jun 15, 2016 08:31, "Lorenzo Caminiti" <lorcaminiti@gmail.com> wrote: Have you followed any of the recent papers regarding language-level contracts for C++?
No... but I should definitely take a look! Do you have a link to the proposal to get me started?
Here is the last version of the proposal: http://open-std.org/JTC1/SC22/WG21/docs/papers/2016/p0380r0.pdf It seems like it's close to completion. To be short, it's using attributes and unspecifiedly set constants to drive the compiler into inserting or not the checking code in the produced program. Joël Lamotte
On Wed, Jun 15, 2016 at 2:21 PM, Klaim - Joël Lamotte <mjklaim@gmail.com> wrote:
On 15 June 2016 at 23:15, Lorenzo Caminiti <lorcaminiti@gmail.com> wrote:
On Wed, Jun 15, 2016 at 8:47 AM, Matt Calabrese <rivorus@gmail.com> wrote:
On Jun 15, 2016 08:31, "Lorenzo Caminiti" <lorcaminiti@gmail.com> wrote: Have you followed any of the recent papers regarding language-level contracts for C++?
No... but I should definitely take a look! Do you have a link to the proposal to get me started?
Here is the last version of the proposal: http://open-std.org/JTC1/SC22/WG21/docs/papers/2016/p0380r0.pdf
I always thought it'd be great to have contracts added to the core language... if not for anything else, for a more concise syntax and compiler optimizations. Unfortunately I found this P0380 proposal largely inadequate. In my opinion/experience, the following are major issues with P0380: 1. Complete lack of class invariants. In my experience, class invariants are essentially as important as preconditions when programming contracts for objects. 2. No old values for postconditions. In my experience, most postcondition assertions cannot be programmed without old values. 3. If I understand it correctly, the rule that "the contracts of every declaration of a function must be (ODR) identical" (P0380 section 4) essentially prevent subcontracting. Class invariants, postcondition old values, and subcontracting are key aspects of contract programming. A framework that does not support those is not really a contract programming framework, it's essentially just a bit more than `assert()`. Maybe that was the intent of P0380 to be just a bit more than `assert()`... but is that useful or it's best to just use `assert()` at that point (maybe within #ifdef to emulate the default/axiom/audit levels)? N1962 (http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2006/n1962.html) was a solid proposal for adding Contract Programming to C++. Why not accepting that proposal (maybe with the attributes syntax introduced by P0380)? I might write to P0380 authors with some of these notes. Thanks, --Lorenzo P.S. Of course, these P0380 gaps will make Boost.Contract useful even on C++1z (say if you want to do basic stuff like using old values in postconditions, programming a class invariants, or even more complex stuff like using subcontracting).
2016-06-24 22:10 GMT+02:00 Lorenzo Caminiti <lorcaminiti@gmail.com>:
Here is the last version of the proposal: http://open-std.org/JTC1/SC22/WG21/docs/papers/2016/p0380r0.pdf
I always thought it'd be great to have contracts added to the core language... if not for anything else, for a more concise syntax and compiler optimizations. Unfortunately I found this P0380 proposal largely inadequate. In my opinion/experience, the following are major issues with P0380:
1. Complete lack of class invariants. In my experience, class invariants are essentially as important as preconditions when programming contracts for objects. 2. No old values for postconditions. In my experience, most postcondition assertions cannot be programmed without old values. 3. If I understand it correctly, the rule that "the contracts of every declaration of a function must be (ODR) identical" (P0380 section 4) essentially prevent subcontracting.
Class invariants, postcondition old values, and subcontracting are key aspects of contract programming. A framework that does not support those is not really a contract programming framework, it's essentially just a bit more than `assert()`. Maybe that was the intent of P0380 to be just a bit more than `assert()`... but is that useful or it's best to just use `assert()` at that point (maybe within #ifdef to emulate the default/axiom/audit levels)?
I think you need to look at P0380 as a step towards full contract support. The authors are well aware that more support is needed in the future; they simply decided to add some uncontroversial parts as soon s possible. I think it is a wise choice to add features cautiously, given that there exist no implementation experience in C++. I think contracts in C++ are somewhat different than these in Eiffel. The focus is more on being able to perform static analysis. And it is not clear what exactly is needed to help static analysers. This has been described in n4160 <http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2014/n4160.html> ( http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2014/n4160.html). This limited proposal is already useful on its own, and gives some values to programmers, while buying some time for the Committee to decide how they want to handle invariants in C++. For instance, should class invariant also be required to hold before and and after free functions that are declared friends by our class? Again, it is described in n4160 <http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2014/n4160.html>.
N1962 (http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2006/n1962.html) was a solid proposal for adding Contract Programming to C++. Why not accepting that proposal (maybe with the attributes syntax introduced by P0380)?
This proposal is more feature complete, but it does not go into details of how contracts interact with other c++-specific features like friends, noexcept, constexpr. It does not give evidence that it is sufficient to support static analysers. Regards, &rzej
On Fri, Jun 24, 2016 at 2:25 PM, Andrzej Krzemienski <akrzemi1@gmail.com> wrote:
2016-06-24 22:10 GMT+02:00 Lorenzo Caminiti <lorcaminiti@gmail.com>:
Here is the last version of the proposal: http://open-std.org/JTC1/SC22/WG21/docs/papers/2016/p0380r0.pdf
I always thought it'd be great to have contracts added to the core language... if not for anything else, for a more concise syntax and compiler optimizations. Unfortunately I found this P0380 proposal largely inadequate. In my opinion/experience, the following are major issues with P0380:
<snip>
N1962 (http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2006/n1962.html) was a solid proposal for adding Contract Programming to C++. Why not accepting that proposal (maybe with the attributes syntax introduced by P0380)?
This proposal is more feature complete, but it does not go into details of how contracts interact with other c++-specific features like friends, noexcept, constexpr. It does not give evidence that it is sufficient to support static analysers.
Andrzej, as always your raise very good points and questions! I have now read most (all?) n/p-papers on contracts since N1962. I will try to address the questions above, especially with respect to what Boost.Contract does, in a hand full of separate emails on this mailing list. Thank you. --Lorenzo
On Wed, Jun 15, 2016 at 8:47 AM, Peter Dimov <lists@pdimov.com> wrote:
Lorenzo Caminiti wrote:
boost::contract::old_ptr<int> old_x = BOOST_CONTRACT_OLDOF(x);
Hi Lorenzo,
Why is the old value a pointer instead of just a local copy?
Good question. Old values need to be at least optional values because: 1. They are not copied and therefore left empty when BOOST_CONTRACT_NO_POSTCONDITIONS is #defined. https://lcaminiti.github.io/boost-contract/doc/html/BOOST_CONTRACT_NO_POSTCO... 2. It is possible to copy them after preconditions are checked specifying a functor using `.old(...)`. In that case old values need to be left initialized (i.e., empty) when they are first declared before the contract code. https://lcaminiti.github.io/boost-contract/doc/html/boost_contract/advanced_... So I originally implemented old values using boost::optional. However, that did not suffice when I implemented subcontracting. The reasons are specific to the library implementation so hard to clearly explain in few words... but I'll try: 3. An overriding public function will call the public functions (plural for multiple inheritance) that is overriding and call each of them multiple times. That is to check subcontracted preconditions first, than execute the functor specified to `.old(...)` (if present), and then to check subcontracted postconditions (because preconditions, old, and postconditions functors are part of the overridden function definition so they are only accessible by calling the overridden functions). All these different calls to the overridden functions should not copy old values multiple times. Using smart pointers (instead of just boost::optional values) allows the library to copy an old value and allocate the related pointer only once then pass this one pointer around the multiple calls to the overridden functions needed for subcontracting. I will add rationales 1-3 above the docs (I forgot to list them in the current docs). Thanks, --Lorenzo
On 6/15/2016 11:30 AM, Lorenzo Caminiti wrote:
Hello all,
In the last few years my professional and personal lives changed quite a bit limiting my ability to contribute to Boost. However, in my spare time I slowing continued to revise Boost.Contract hoping to be able to commit it to a Boost release someday (after the library was accepted 3+ years ago... https://groups.google.com/forum/?fromgroups=#!topic/boost-list/jQ7OjAmos_Y). While doing so I realized that leveraging C++11 lambda functions, Boost.Contract could be re-implemented without its crazy macros that alter C++ function declaration syntax.
Boost.Contract still remains the only C++ library that implements *all* features of Contract Programming (a.k.a., Design by Contract or DbC): subcontracting, class invariants (also static and volatile), postconditions (with old and return values), preconditions, customizable actions on assertion failure (terminate, throw, etc.), optional assertion compilation, disable assertion checking while already checking other assertions (to avoid infinite recursion), etc. Furthermore, in its new incarnation Boost.Contract no longer uses crazy macros so it is easier to use, faster to compile, and gives readable compiler errors.
For example:
#include <boost/contract.hpp>
int inc(int& x) { int result; boost::contract::old_ptr<int> old_x = BOOST_CONTRACT_OLDOF(x); boost::contract::guard c = boost::contract::function() .precondition([&] { BOOST_CONTRACT_ASSERT(x < std::numeric_limits<int>::max()); }) .postcondition([&] { BOOST_CONTRACT_ASSERT(x == *old_x + 1); BOOST_CONTRACT_ASSERT(result == *old_x); }) ;
return result = x++; // Function body. }
Or with subcontracting:
#include <boost/contract.hpp> #include <vector>
template<typename T> class pushable; // Arbitrary base to demo subcontracting.
template<typename T> class vector #define BASES public pushable<T> : BASES { public: typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; // Subcontracting. #undef BASES
void invariant() const { // Checked in AND with base class invariants. BOOST_CONTRACT_ASSERT(size() <= capacity()); // Line 25. }
virtual void push_back(T const& value, boost::contract::virtual_* v = 0) /* override */ { boost::contract::old_ptr<unsigned> old_size = BOOST_CONTRACT_OLDOF(v, size()); // Old values. boost::contract::guard c = boost::contract::public_function< override_push_back>(v, &vector::push_back, this, value) .precondition([&] { // Checked in OR with base preconditions. BOOST_CONTRACT_ASSERT(size() < max_size()); // Line 35. }) .postcondition([&] { // Checked in AND with base postconditions. BOOST_CONTRACT_ASSERT(size() == *old_size + 1); // Line 38. }) ;
vect_.push_back(value); // Function body. } BOOST_CONTRACT_OVERRIDE(push_back) // For `override_push_back`.
// Could program contracts for those as well. unsigned size() const { return vect_.size(); } unsigned max_size() const { return vect_.max_size(); } unsigned capacity() const { return vect_.capacity(); }
private: std::vector<T> vect_; };
Full documentation and examples at: https://lcaminiti.github.io/boost-contract
What do you think?
Thanks, --Lorenzo
P.S. The library can also be used without C++11 lambda functions (or any C++11 specific feature) but programmers have to write a fare amount of extra code to program the precondition and postcondition functors (using non-local functions, Boost.LocalFunction, Boost.Funsion, Boost.Lambda, or some other approach) so that might not useful in practice.
You are certainly allowed to have your library require C++11. Since your library has already been accepted into Boost why not add it officially to Boost as a C++11 on up library ?
On Wed, Jun 15, 2016 at 9:03 AM, Edward Diener <eldiener@tropicsoft.com> wrote:
On 6/15/2016 11:30 AM, Lorenzo Caminiti wrote:
P.S. The library can also be used without C++11 lambda functions (or any C++11 specific feature) but programmers have to write a fare amount of extra code to program the precondition and postcondition functors (using non-local functions, Boost.LocalFunction, Boost.Funsion, Boost.Lambda, or some other approach) so that might not useful in practice.
You are certainly allowed to have your library require C++11. Since your library has already been accepted into Boost why not add it officially to Boost as a C++11 on up library ?
True, but the library compiles on C++03 as well. There are explicit comments in the docs that indicate the library is most useful when C++11 lambda functions are available (plus essentially all examples in the docs use lambdas): ``It is possible to use this library without C++11 lambda functions but a large amount of boiler-plate code is required to manually program separate functions to specify preconditions and postconditions (so using this library without C++11 lambda functions is not recommended, see No Lambda Functions).'' https://lcaminiti.github.io/boost-contract/doc/html/boost_contract/getting_s... So, if I'll push the library in Boost, I'd probably push it as a non-C++11 specific library that is however most useful on compiler that support C++11 lambdas. Thanks, --Lorenzo
2016-06-15 17:30 GMT+02:00 Lorenzo Caminiti <lorcaminiti@gmail.com>:
Hello all,
In the last few years my professional and personal lives changed quite a bit limiting my ability to contribute to Boost. However, in my spare time I slowing continued to revise Boost.Contract hoping to be able to commit it to a Boost release someday (after the library was accepted 3+ years ago... https://groups.google.com/forum/?fromgroups=#!topic/boost-list/jQ7OjAmos_Y ). While doing so I realized that leveraging C++11 lambda functions, Boost.Contract could be re-implemented without its crazy macros that alter C++ function declaration syntax.
Boost.Contract still remains the only C++ library that implements *all* features of Contract Programming (a.k.a., Design by Contract or DbC): subcontracting, class invariants (also static and volatile), postconditions (with old and return values), preconditions, customizable actions on assertion failure (terminate, throw, etc.), optional assertion compilation, disable assertion checking while already checking other assertions (to avoid infinite recursion), etc. Furthermore, in its new incarnation Boost.Contract no longer uses crazy macros so it is easier to use, faster to compile, and gives readable compiler errors.
For example:
#include <boost/contract.hpp>
int inc(int& x) { int result; boost::contract::old_ptr<int> old_x = BOOST_CONTRACT_OLDOF(x); boost::contract::guard c = boost::contract::function() .precondition([&] { BOOST_CONTRACT_ASSERT(x < std::numeric_limits<int>::max()); }) .postcondition([&] { BOOST_CONTRACT_ASSERT(x == *old_x + 1); BOOST_CONTRACT_ASSERT(result == *old_x); }) ;
return result = x++; // Function body. }
Or with subcontracting:
#include <boost/contract.hpp> #include <vector>
template<typename T> class pushable; // Arbitrary base to demo subcontracting.
template<typename T> class vector #define BASES public pushable<T> : BASES { public: typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; // Subcontracting. #undef BASES
void invariant() const { // Checked in AND with base class invariants. BOOST_CONTRACT_ASSERT(size() <= capacity()); // Line 25. }
virtual void push_back(T const& value, boost::contract::virtual_* v = 0) /* override */ { boost::contract::old_ptr<unsigned> old_size = BOOST_CONTRACT_OLDOF(v, size()); // Old values. boost::contract::guard c = boost::contract::public_function< override_push_back>(v, &vector::push_back, this, value) .precondition([&] { // Checked in OR with base preconditions. BOOST_CONTRACT_ASSERT(size() < max_size()); // Line 35. }) .postcondition([&] { // Checked in AND with base postconditions. BOOST_CONTRACT_ASSERT(size() == *old_size + 1); // Line 38. }) ;
vect_.push_back(value); // Function body. } BOOST_CONTRACT_OVERRIDE(push_back) // For `override_push_back`.
// Could program contracts for those as well. unsigned size() const { return vect_.size(); } unsigned max_size() const { return vect_.max_size(); } unsigned capacity() const { return vect_.capacity(); }
private: std::vector<T> vect_; };
Full documentation and examples at: https://lcaminiti.github.io/boost-contract
What do you think?
Thanks, --Lorenzo
P.S. The library can also be used without C++11 lambda functions (or any C++11 specific feature) but programmers have to write a fare amount of extra code to program the precondition and postcondition functors (using non-local functions, Boost.LocalFunction, Boost.Funsion, Boost.Lambda, or some other approach) so that might not useful in practice.
If I understand correctly, the change you propose moves the assertions from function declaration into function definition. If this is the case, I would say it is a step in wrong direction. Pre-/post-conditions are part of function contract and belong in function declaration. Also, from the example, it looks like I will have to pay for the existence of `boost::contract::old_ptr` and `boost::contract::guard` (and compiler warnings related to them) even if I disable contracts. Is that right? I do not know what the previous macros did, but I had the impression that they were able to erase any track of contract-related objects. Also, the way you use the return value, forces me to depart from how I normally write return statements. While the new version is clearly more readable, it also has certain important disadvantages compared to the previous version. What more do the new version of pre/postconditions offers compared to putting two asserts at the beginning and the end of the function? Preconditions are evaluated after local object's destructors. What you propose is addressing the subject from a different anle, but is not necessarily superior to the previous version. Regards, &rzej
Hi Andrzej! 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>:
While doing so I realized that leveraging C++11 lambda functions, Boost.Contract could be re-implemented without its crazy macros that alter C++ function declaration syntax.
If I understand correctly, the change you propose moves the assertions from function declaration into function definition. If this is the case, I would say it is a step in wrong direction. Pre-/post-conditions are part of function contract and belong in function declaration.
True this a downside of the new version, but that removes the crazy macros which I consider more important in using the library than keeping contracts with function declarations. If you are willing to manually repeat the function signature, you cal leave a small function definition in header files that will just program the contracts and then calls the body. That emulates keeping contracts with function declarations to the extent they will be clearly visible from the header files that are shipped with the compiled code: ``Contracts are part of the program specification and not of its implementation (see also Specification and Implementation). However, this library uses function definitions to program the contracts so contract code appears together with the function implementation code. ...'' https://lcaminiti.github.io/boost-contract/doc/html/boost_contract/advanced_...
Also, from the example, it looks like I will have to pay for the existence of `boost::contract::old_ptr` and `boost::contract::guard` (and compiler warnings related to them) even if I disable contracts. Is that right?
Yes, you'll pay the cost of declaring a smart pointer for old_ptr that will be assigned to null in this case (no old value copy is actually done when postconditions are disable) and a contract guard that will do nothing. The library implementation code is optimized to remove all internal members, etc. so these objects are rather simple when contracts are disable, but they are still there.
I do not know what the previous macros did, but I had the impression that they were able to erase any track of contract-related objects.
Yes, the old macros where able to completely erase contract code from user code when contracts were disabled. With the new version you can do that manually if that is truly needed: https://lcaminiti.github.io/boost-contract/doc/html/boost_contract/advanced_... However, in my experience if a piece of code is very critical for performance then I don't program contracts for it (because even the cost of checking preconditions might not be acceptable). Most of the code however is not that performance-critical, I program contracts for it, and if this contract code declares an extra empty pointer and guard even when contracts are disabled that's not an issue in practice (plus I usually leave preconditions and entry invariants enabled even in code that is shipped).
Also, the way you use the return value, forces me to depart from how I normally write return statements.
While the new version is clearly more readable, it also has certain important disadvantages compared to the previous version. What more do the new version of pre/postconditions offers compared to putting two asserts at the beginning and the end of the function?
Old values, class invariants, and subcontracting (in increasing order of implementation complexity).
Preconditions are evaluated after local object's destructors. What you propose is addressing the subject from a different anle, but is not necessarily superior to the previous version.
Absolutely correct, there is a trade-off between the old and new version (I think I pointed that out in the docs even if not in a direct comparison with the old macro interface, I will do that comparison in the Release Notes section). That said, the crazy macro syntax, long compilation/preprocessing times, and cryptic compiler/preprocessor errors were major blockers for adopting the old library in real code. The new library no longer suffers from these issues so I hope it can be more widely used. I consider that a fare trade-off with respect to the cost of not having contracts in declarations and small run-time overheads associated with empty old_ptr and guard when contracts are all disabled (also programmers can manually program extra code to get around these limitations in sections of the code where they really are limiting in practice). Thanks, --Lorenzo
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
On Mon, Jun 27, 2016 at 10:48 AM, Lorenzo Caminiti <lorcaminiti@gmail.com> wrote:
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>:
<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
participants (6)
-
Andrzej Krzemienski -
Edward Diener -
Klaim - Joël Lamotte -
Lorenzo Caminiti -
Matt Calabrese -
Peter Dimov