From 2b73d42ee17b4aa6169e35eceb028bdda479e18d Mon Sep 17 00:00:00 2001 From: Lorenzo Caminiti Date: Thu, 20 Jul 2017 08:44:03 -0700 Subject: [PATCH] added comments to docs from all references recentely read (n/p-papers, boost emails, etc.) --- doc/{advanced_topics.qbk => advanced.qbk} | 12 +-- doc/bibliography.qbk | 36 ++++++- doc/contract_programming_overview.qbk | 112 +++++++++++++++++++-- doc/examples.qbk | 1 + doc/{extra_topics.qbk => extras.qbk} | 41 +++++++- doc/full_table_of_contents.qbk | 24 ++--- doc/introduction.qbk | 29 ++++-- doc/main.qbk | 65 +++++++----- doc/tutorial.qbk | 5 +- example/Jamfile.v2 | 4 +- example/features/ifdef_audit.cpp | 56 +++++++++++ example/features/introduction.cpp | 2 +- example/features/introduction_comments.cpp | 2 +- example/features/introduction_public.cpp | 89 ++++++++++++++++ example/n1962/vector.cpp | 21 ++++ example/n1962/vector_n1962.hpp | 21 ++++ include/boost/contract.hpp | 4 - 17 files changed, 449 insertions(+), 75 deletions(-) rename doc/{advanced_topics.qbk => advanced.qbk} (98%) rename doc/{extra_topics.qbk => extras.qbk} (94%) create mode 100644 example/features/ifdef_audit.cpp create mode 100644 example/features/introduction_public.cpp diff --git a/doc/advanced_topics.qbk b/doc/advanced.qbk similarity index 98% rename from doc/advanced_topics.qbk rename to doc/advanced.qbk index 234c04a..32416c7 100644 --- a/doc/advanced_topics.qbk +++ b/doc/advanced.qbk @@ -4,7 +4,7 @@ [/ file LICENSE_1_0.txt or a copy at http://www.boost.org/LICENSE_1_0.txt).] [/ See: http://www.boost.org/doc/libs/release/libs/contract/doc/html/index.html] -[section Advanced Topics] +[section Advanced] This section illustrates more advanced uses of this library. @@ -200,7 +200,7 @@ Therefore, [macroref BOOST_CONTRACT_OVERRIDE] only needs to be invoked once for [endsect] -[section Lambdas, Loops, Code Blocks, Etc.] +[section Lambdas, Loops, Code Blocks (and `constexpr`)] So far we have been focused on specifying contracts for function and class interfaces. While contracts are in general most useful when used to specify interfaces, this library also allows to check contract conditions for implementation code (lambda functions, code blocks, loops, etc.). @@ -223,7 +223,7 @@ For example (see also [@../../example/features/code_block.cpp =code_block.cpp=]) [import ../example/features/code_block.cpp] [code_block] -Finally, this library does not support contracts for functions declared `constexpr`. +Finally, at the moment this library does not support contracts for functions declared `constexpr`. [footnote *Rationale:* In general, it might be useful to specify contracts for constexpr functions and literal classes. @@ -373,14 +373,14 @@ All these members can be declared `private` as long as the [classref boost::cont This technique is not used in most examples of this documentation only for brevity, but programmers are encouraged to use it in real code. [warning -Not declaring this class friend of user-defined classes will cause compiler errors on some compilers (e.g., MSVC) because the private members needed to check the contracts will not be accessible. +Not declaring this class friend of user-defined classes might cause compiler errors on some compilers (e.g., MSVC) because the private members needed to check the contracts will not be accessible. On other compilers (e.g., GCC and CLang), the private access will instead fail SFINAE and no compiler error will be reported while invariants and subcontracting will be silently skipped at run-time. Therefore, programmers must make sure to either declare invariant functions and base types @c typedef as public members or to declare this class as friend. ] [endsect] -[section Throw on Failure] +[section Throw on Failure (and `noexcept`)] If a conditions checked using [macroref BOOST_CONTRACT_ASSERT] is evaluated to be `false` or more in general if any of the specified contract code throws an exception (in fact, [macroref BOOST_CONTRACT_ASSERT] simply expands to code that throws a [classref boost::contract::assertion_failure] exception, see also __No_Macros__), this library will call an appropriate /contract failure handler/ function as follow: @@ -444,7 +444,7 @@ For example, if the following precondition functor throws the user-defined excep [throw_on_failure_ctor] [throw_on_failure_class_end] -Finally, note that the exception specifiers `noexcept` (and `throw`, deprecated since C++11) of the enclosing operation declaring the contract apply to the contract code itself. +Finally, note that the exception specifiers `noexcept` (since C++11) and `throw` (deprecated in C++11) of the enclosing operation declaring the contract correctly apply to the contract code itself. Therefore, even if the contract failure handlers are reprogrammed to throw exceptions in case of contract failures, such exception will never be thrown outside the context of the enclosing operation if that is not in accordance with the exception specifiers of such operation (notably all destructors are implicitly declared `noexcept(true)` in C++11). For example, the following code will never throw from the destructor, not even if the class invariants checked at destructor entry throw `too_large_error` and the contract failure handlers for invariants are programmed to throw from destructors as well (the program will always terminate in this case instead, see also [@../../example/features/throw_on_failure.cpp =throw_on_failure.cpp=]): diff --git a/doc/bibliography.qbk b/doc/bibliography.qbk index 415fe88..d445bdb 100644 --- a/doc/bibliography.qbk +++ b/doc/bibliography.qbk @@ -8,13 +8,15 @@ This section lists all references consulted while designing and developing this library. +[#Andrzej13_anchor] [Andrzej13] A. Krzemienski. [@https://akrzemi1.wordpress.com/2013/01/04/preconditions-part-i/ /Andrzej's C++ blog: Preconditions/]. 2013. + [#Bright04_anchor] [Bright04] W. Bright. [@http://www.digitalmars.com/d/2.0/dbc.html /Contract Programming for the D Programming Language/]. 2004. [#Bright04b_anchor] [Bright04b] W. Bright. [@http://www.digitalmars.com/ctg/contract.html /Contract Programming for the Digital Mars C++ Compiler/]. 2004. [#C2_anchor] [C2] Aechmea. [@http://www.programmersheaven.com/app/news/DisplayNews.aspx?NewsID=3843 /C^2 Contract Programming add-on for C++/]. 2005. -[#Chrome02_anchor] [Chrome02] RemObjects. [@http://blogs.remobjects.com/blogs/mh/2008/05/01/p216 /Chrome: Contract Programming for Object Pascal in .NET/]. 2002. +[#Chrome_anchor] [Chrome] RemObjects. [@http://blogs.remobjects.com/blogs/mh/2008/05/01/p216 /Chrome: Contract Programming for Object Pascal in .NET/]. 2002. [#Clarke06_anchor] [Clarke06] L. A. Clarke and D. S. Rosenblum. [@http://discovery.ucl.ac.uk/4991/1/4991.pdf /A Historical Perspective on Runtime Assertion Checking in Software Development/]. Newsletter ACM SIGSOFT Software Engineering Notes, 2006. @@ -54,12 +56,42 @@ This section lists all references consulted while designing and developing this [#N1962_anchor] [N1962] L. Crowl and T. Ottosen. [@http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2006/n1962.html /Proposal to add Contract Programming to C++ (revision 4)/]. The C++ Standards Committee, N1962, 2006. -[#N2081_anchor] [N2081] D. Gregor, B. Stroustrup. [@http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2006/n2081.pdf /Concepts (revision 1)/]. The C++ Standards Committee, N2081, 2006. +[#N2081_anchor] [N2081] D. Gregor and B. Stroustrup. [@http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2006/n2081.pdf /Concepts (revision 1)/]. The C++ Standards Committee, N2081, 2006. + +[#N2887_anchor] [N2887] G. Dos Reis, B. Stroustrup, and A. Meredith. [@http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2009/n2887.pdf /Axioms: Semantics Aspects of C++ Concepts/]. The C++ Standards Committee, N2887, 2009. [#N2914_anchor] [N2914] P. Becker. [@http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2009/n2914.pdf /Working Draft, Standard for Programming Language C++/]. The C++ Standards Committee, N2914, 2009. [#N2906_anchor] [N2906] B. Stroustrup. [@http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2009/n2906.pdf /Simplifying the sue of concepts/]. The C++ Standards Committee, N2906, 2009. +[#N3248_anchor] [N3248] J. Lakos. [@http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2011/n3248.pdf ['[^noexcept] Prevents Library Validation]]. The C++ Standards Committee, N3248, 2011. + +[#N4154_anchor] [N4154] D. Krauss. [@http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2014/n4154.pdf ['Operator [^assert]]]. The C++ Standards Committee, N4154, 2014. + +[#N4160_anchor] [N4160] A. Krzemienski. [@http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2014/n4160.html /Value constraints/]. The C++ Standards Committee, N4160, 2014. + +[#N4248_anchor] [N4248] A. Meredith. [@http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2014/n4248.html /Library Preconditions are a Language Feature/]. The C++ Standards Committee, N4248, 2014. + +[#N4293_anchor] [N4293] J. D. Garcia. [@http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2014/n4293.pdf /C++ language support for contract programming/]. The C++ Standards Committee, N4293, 2014. + +[#N4378_anchor] [N4378] J. Lakos, N. Myers, A. Zakharov, and A. Beels. [@http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2015/n4378.pdf /Language Support for Contract Assertions (Revision 10)/]. The C++ Standards Committee, N4378, 2015. + +[#N4379_anchor] [N4378] J. Lakos and N. Myers. [@http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2015/n4379.pdf /FAQ about Contract Assertions/]. The C++ Standards Committee, N4379, 2015. + +[#N4435_anchor] [N4435] W. E. Brown. [@http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2015/n4435.pdf /Proposing Contract Attributes/]. The C++ Standards Committee, N4435, 2015. + +[#P0147_anchor] [P0147] L. Crowl. [@http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2015/p0147r0.html /The Use and Implementation of Contracts/]. The C++ Standards Committee, P0147R0, 2015. + +[#P0166_anchor] [P0166] J. D. Garcia. [@http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2015/p0166r0.pdf /Three interesting questions about contracts/]. The C++ Standards Committee, P0166R0, 2015. + +[#P0246_anchor] [P0246] N. Myers. [@http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2016/p0246r0.pdf /Criteria for Contract Support Merged Proposal/]. The C++ Standards Committee, P0246R0, 2016. + +[#P0287_anchor] [P0287] G. Dos Reis, J.D. Garcia, F. Logozzo, M. Fahndrich, S. Lahiri. [@http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2016/p0287r0.pdf /Simple Contracts for C++ (R1)/]. The C++ Standards Committee, P0287R0, 2016. + +[#P0380_anchor] [P0380] G. Dos Reis, J.D. Garcia, J. Lakos, A. Meredith, N. Myers, and B. Stroustrup. [@http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2016/p0380r1.pdf /A Contract Design/]. The C++ Standards Committee, P0380R1, 2016. + +[#P0542_anchor] [P0542] G. Dos Reis, J.D. Garcia, J. Lakos, A. Meredith, N. Myers, and B. Stroustrup. [@http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2017/p0542r0.html /Support for contract based programming in C++/]. The C++ Standards Committee, P0542R0, 2017. + [#Rosenblum95_anchor] [Rosenblum95] D. S. Rosenblum. [@http://www.cs.toronto.edu/~chechik/courses06/csc410/rosenblum_assert95.pdf /A practical Approach to Programming With Assertions/]. IEEE Transactions on Software Engineering, 1995. [#SPARKAda_anchor] [SPARKAda] Praxis. [@http://www.praxis-his.com/sparkada/language.asp /SPARKAda (Ada-like Language with Contract Programming)/]. diff --git a/doc/contract_programming_overview.qbk b/doc/contract_programming_overview.qbk index 3e10820..7dfc809 100644 --- a/doc/contract_programming_overview.qbk +++ b/doc/contract_programming_overview.qbk @@ -23,6 +23,12 @@ Then, this library aims to be the best and more complete Contract Programming li Contract Programming is characterized by the following assertion mechanisms: * /Preconditions/: These are logical conditions that programmers expect to be true when a function is called (e.g., to check constraints on function arguments). +Operations that logically have no preconditions (i.e., that are always well-defined for the entire domain of their inputs) are often referred to as having a /wide contract/. +This is in contrast with operations that have preconditions which are often referred to as having a /narrow contract/ (note that an operation with truly narrow contracts should not throw exceptions). +[footnote +The nomenclature of wide and narrow contracts has gained some popularity in recent years in the C++ community (appearing in a number of more recent proposals to add contract programming to the C++ standard, see __Bibliography__). +This nomenclature is perfectly reasonable but it is not often used in this document because the authors generally prefer to explicit mention "this operation has no preconditions..." or "this operation has preconditions..." just for a matter of clarity and style. +] * /Postconditions/: These are logical conditions that programmers expect to be true when a function exits without throwing an exception (e.g., to check the result and any side effect that a function might have). Postconditions can access the function return value (for non-void functions) and /old values/ that expressions had before the function body was executed. * /Exception guarantees/: These are logical conditions that programmers except to be true when a function exits throwing an exception. @@ -40,6 +46,8 @@ It is also possible to specify /static class invariants/ which are excepted to b Static and volatile class invariants were first introduced by this library to reflect the fact that C++ supports both static and volatile member functions. Static and volatile class invariants are not part of __N1962__ or other references listed in the __Bibliography__. ] +Arguably, class invariants can be used as a criterion for good abstraction: If it is not possible to specify an invariant, it might be an indication that the design abstraction maybe be poor and it should not have been made a class. +Class invariants can also be used to specify /basic/ exception safety guarantees for an object (because they are checked at exit of public member function even when those throw an exception), while exception guarantees assertions can be used to specify /strong/ exception safety for given operations on the same object. * /Subcontracting/: This indicates that preconditions cannot be strengthen, while postconditions and class invariants cannot be weaken when a public function in a derived class overrides public functions in one or more of its base classes (this is formally defined according to the __substitution_principle__). Furthermore, it is a common requirement for Contract Programming to automatically disable contract checking while already checking assertions from another contract (in order to avoid infinite recursion while checking contract assertions). @@ -54,6 +62,12 @@ This library will automatically protect such a global variable from race conditi In general, it is recommended to specify different contract conditions using separate assertion statements and not to group them together into a single condition using logical operators (`&&`, `||`, etc.). This is because when contract conditions are programmed together in a single assertion using logical operators, it is not be clear which condition actually failed in case the entire assertion fails at run-time. +Of course, not all formal contract assertions can actually be programmed in C++. +For example, in C++ is it not possible to assert the validity of an iterator range in the general case because the only way to check if two iterators form a valid range is to keep incrementing the first iterator until we reach the second iterator. +However, in case the iterator range is invalid, such a code would render undefined behaviour or run forever instead of failing an assertion. +Nevertheless, a large amount of contract conditions can be successfully programmed in C++ as illustrated by the numerous examples in this documentation and from the literature (see also __Examples__ and __Bibliography__). + + A limited form of Contract Programming is the use of the C-style `assert` macro. Using `assert` is common practice for many programmers but it suffers of the following limitations: @@ -353,7 +367,7 @@ The following table compares Contract Programming features among this library, t [Feature] [This Library] [__N1962__ Proposal (not part of C++)] - [__P0186__ Proposal (being considered for C++1z)] + [__P0380__ Proposal (being considered for C++1z)] [ISE Eiffel 5.4 (see __Meyer97__)] [D (see __Bright04__)] ][ @@ -514,13 +528,21 @@ Therefore, this feature was removed in the current revision of this library. ][ [['Disable contract checking]] [ -Yes, contract checking can be skipped at run-time by defining combinations of the [macroref BOOST_CONTRACT_NO_PRECONDITIONS], [macroref BOOST_CONTRACT_NO_POSTCONDITIONS], [macroref BOOST_CONTRACT_NO_INVARIANTS], [macroref BOOST_CONTRACT_NO_ENTRY_INVARIANTS], and [macroref BOOST_CONTRACT_NO_EXIT_INVARIANTS] macros. -(Also removing contract code from compiled object code is possible but requires users to program a fare amount of boiler-plate code, see __Disable_Contract_Checking__.) +Yes, contract checking can be skipped at run-time by defining combinations of the [macroref BOOST_CONTRACT_NO_PRECONDITIONS], [macroref BOOST_CONTRACT_NO_POSTCONDITIONS], [macroref BOOST_CONTRACT_NO_INVARIANTS], [macroref BOOST_CONTRACT_NO_ENTRY_INVARIANTS], and [macroref BOOST_CONTRACT_NO_EXIT_INVARIANTS] macros (completely removing contract code from compiled object code is possible but requires using macro API, see __Disable_Contract_Compilation__.) ] [Yes (contract code also removed from compiled object code, but details compiler implementation specific).] [Yes (contract code also removed from compiled object code, but details compiler implementation specific).] [Yes, but only predefined combinations of preconditions, postconditions, and class invariants can be disabled (contract code also removed from compiled object code).] [Yes.] +][ + [['Assertion levels]] + [ +Yes, programmers can define their own assertion levels as needed (including "audit" and "axiom", see __Disable_Contract_Checking__). +] + [No (but a previous revision of this proposal considered adding assertion levels called "assertion ordering").] + [Yes, predefined "audit" and "axiom".] + [No.] + [No.] ] ] @@ -570,13 +592,85 @@ This is an Ada-like programming language with support for Contract Programming. ] ] ] -To the best knowledge of the authors, this the only library that fully supports all Contract Programming features for C++. +To the best knowledge of the authors, this the only library that fully supports all Contract Programming features for C++: + +* Generally speaking, implementing preconditions and postconditions in C++ is not difficult (e.g., using some kind of RAII object). +* Implementing postcondition old values is also not too difficult usually requiring programmers to copy old values into local variables, but it is already somewhat more difficult to ensure such copies are not performed when postconditions are disabled. [footnote -Generally speaking, implementing preconditions and postconditions in C++ is not difficult (e.g., using some kind of RAII object). -Implementing postcondition old values is also not too difficult (usually requiring programmers to copy old values into local variables, but it is somewhat more difficult to ensure such copies are not performed when postconditions are disabled). -Most Contract Programming libraries for C++ stop here because implementing class invariants is already somewhat more involved (especially if done automatically, without requiring programmers to manually invoke an extra function to check invariants). -After that, implementing subcontracting involves a significant amount of complexity and it seems to not be properly supported by any library other than this one (especially when handling multiple inheritance, correctly copying postcondition old values across all overridden contracts deep in the inheritance tree, and correctly reporting the return value to the postconditions of overridden virtual functions in base classes). -This library supports all of these features instead. +For example, the following emulation of old values based on __P0380__ never disables old value copies plus requires boiler-plate code to make sure postconditions are correctly checked in a `scope_exit` RAII object after all other local objects have been destroyed (because some of these destructors contribute to establishing the postconditions) and only if the function did not throw an exception: +`` + void fswap(file& x, file& y) + [[requires: x.closed()]] + [[requires: y.closed()]] + // Postconditions in function definition below to emulate old values. + { + file old_x = x; // Emulate old values with local copies (not disabled). + file old_y = y; + scope_exit ensures([&] { // Check after local objects destroyed. + if(!std::uncaught_exception()) { // Check only if no throw. + [[assert: x.closed()]] + [[assert: y.closed()]] + [[assert: x == old_y]] + [[assert: y == old_x]] + } + }); + + x.open(); + scope_exit close_x([&] { x.close(); }); + y.open(); + scope_exit close_y([&] { y.close(); }); + file t = file::temp(); + t.open; + scope_exit close_t([&] { t.close(); }); + + x.mv(t); + y.mv(x); + t.mv(y); + } +`` +Here `scope_exit` is an RAII object that executes the nullary functor passed to its constructor when it is destroyed. +] + +* Implementing class invariants is more involved (especially if done automatically, without requiring programmers to manually invoke extra functions to check the invariants). +[footnote +For example, the following possible emulation of class invariants based on __P0380__ requires boiler-plate code to manually invoke the function that checks the invariants (note that invariants are checked at public function exit regardless of exceptions being thrown while postconditions are not): +`` + template + class vector { + bool invariant() const { // Check invariants at... + [[assert: empty() == (size() == 0)]] + [[assert: size() <= capacity()]] + return true; + } + + public: + vector() + [[ensures: invariant()]] // ...constructor exit (only if no throw). + { ... } + + ~vector() noexcept + [[requires: invariant()]] // ...destructor entry. + { ... } + + void push_back(T const& value) + [[requires: invariant()]] // ...public function entry. + [[ensures: invariant()]] // ...public function exit (if no throw). + try { + ... // Function body. + } catch(...) { + invariant(); // ...public function exit (if throw). + throw; + } + + ... + }; +`` +] +All references reviewed by the authors seem to not consider static and volatile member functions not supporting static and volatile invariants respectively. + +* Implementing subcontracting involves a significant amount of complexity and it seems to not be properly supported by any C++ library other than this one (especially when handling multiple inheritance, correctly copying postcondition old values across all overridden contracts deep in the inheritance tree, and correctly reporting the return value to the postconditions of overridden virtual functions in base classes). +[footnote +For example, it is not really possible to sketch pseudocode based on __P0380__ that emulates subcontracting in the general case. ] [endsect] diff --git a/doc/examples.qbk b/doc/examples.qbk index 4181482..fd44fb8 100644 --- a/doc/examples.qbk +++ b/doc/examples.qbk @@ -45,6 +45,7 @@ On compilers that support C++17 `if constexpr`, the above example using this lib [n1962_circle] [endsect] +[#N1962_factorial_anchor] [section \[N1962\] Factorial: Recursion and assertion computational complexity] [import ../example/n1962/factorial.cpp] [n1962_factorial] diff --git a/doc/extra_topics.qbk b/doc/extras.qbk similarity index 94% rename from doc/extra_topics.qbk rename to doc/extras.qbk index b97e925..7164fec 100644 --- a/doc/extra_topics.qbk +++ b/doc/extras.qbk @@ -4,7 +4,7 @@ [/ file LICENSE_1_0.txt or a copy at http://www.boost.org/LICENSE_1_0.txt).] [/ See: http://www.boost.org/doc/libs/release/libs/contract/doc/html/index.html] -[section Extra Topics] +[section Extras] This section can be consulted selectively for specific topics of interest. @@ -114,7 +114,6 @@ If [^['then1]], [^['then2]], ..., [^['else]] are nullary functor templates (not All the `else_if<...>(...)` statements are optional, the `else_(...)` statement is optional if the functor calls return `void` but it is required otherwise. In general, [funcref boost::contract::call_if] can be used to program contract assertions that compile and check different functor templates depending on related conditions being statically evaluated to be `true` or `false` at compile-time (but in most cases [funcref boost::contract::condition_if] should be sufficient, simpler and less verbose to use). - The [funcref boost::contract::condition_if_c], [funcref boost::contract::call_if_c], and `.else_if_c` function templates work similarly to their counterparts without the `..._c` postfix above, but they take their condition template parameters as static boolean values instead of nullary boolean meta-functions. [heading Static-If Emulation (C++14)] @@ -130,6 +129,25 @@ This implementation is more concise, easier to read and maintain than the usual Boost.Hana (`boost::hana::if_`) can also be used together with C++14 generic lambdas to emulate statements similar to C++17 `if constexpr`. ] +[heading Static-If (C++17)] + +Another example where assertion requirements might be useful is to disable assertions in that might be constant-correct for specific template types. +For example, `std::distance` does not alter its iterator arguments but only for forward iterators so the follow template function evaluates its preconditions only for for these types: + + template + void display_first_second_next(InputIter begin, InputIter end) { + boost::contract::check c = boost::contract::function() + .precondition([&] { + if constexpr(is_forward_iterator::value) { + BOOST_CONTRACT_ASSERT(std::distance(begin, end) >= 2); + } // Otherwise, std::distance would change begin and end. + }) + ; + ... + } + +(For convenience this example used C++17 `if constexpr` but it could have been similarly implemented using C++14 generic lambdas or in C++11 using binding to a functor template that calls `std::distance` in its `operator()`.) + [endsect] [section Volatile Public Functions] @@ -225,7 +243,7 @@ A part from that, this library is used as usual to program contracts for unions, [endsect] -[section Disable Contract Checking] +[section Disable Contract Checking (and Assertion Levels)] Checking contracts adds run-time overhead and can slow down program execution (see also __Benefits_and_Costs__). Therefore, programmers can define the following configuration macros (`-D` option in Clang and GCC, `/D` option in MSVC, etc.) to instruct this library to not check specific kind of contract conditions at run-time: @@ -247,6 +265,21 @@ For example, programmers could decide to check all contracts during early develo Old values can be used by both postconditions and exception guarantees so it is necessary to define both [macroref BOOST_CONTRACT_NO_POSTCONDITIONS] and [macroref BOOST_CONTRACT_NO_EXCEPTS] to disable old value copies. ] +[heading Assertion Levels] + +Programmers can use `#if` (or `if`) statements to implement different contract /assertion levels/ that selectively enable and disable assertion checking at compile-time (or run-time). +For example, programmers could define an "audit" level for computationally expensive assertions that alter the computational complexity of the enclosing function and an "axiom" level for computationally prohibitive assertions that should always be excluded from program execution (these are similar to the "audit" and "axiom" assertion levels proposed in __P0380__, see also [@../../example/features/ifdef_audit.cpp =ifdef_audit.cpp=]): + +[import ../example/features/ifdef_audit.cpp] +[ifdef_audit] + +In this example, assertions are still compiled (e.g., to make sure that they are syntactically correct) even when they are not checked at run-time (because they are asserted using `CONTRACT_ASSERT_AUDIT` when `CONTRACT_AUDIT` is not defined, or because they are asserted using `CONTRACT_ASSERT_AXIOM`). +See [link N1962_factorial_anchor \[N1962\] Factorial] for a similar example that completely disables assertions at compile-time based on their computational complexity. + +This library does not prescribe any specific assertion level. +However, assertion levels can be very useful in some programs to granularly disable specific assertions (because too expensive or for some other reason specific to that program). +Programmers can freely implement assertion levels as they see fit for their programs using simple `#if` (or `if`) statements similar to the ones shown in the example above. + [endsect] [section Disable Contract Compilation (Macro Interface)] @@ -377,7 +410,7 @@ The authors think this library is most useful when used together with C++11 lamb [endsect] -[section No Macros (No C++11)] +[section No Macros (and No Variadic Macros)] It is possible to specify contracts without using most of this library macros and programming the related code manually instead. The only macro that cannot be programmed manually is [macroref BOOST_CONTRACT_OVERRIDE] (and the similar [macroref BOOST_CONTRACT_OVERRIDES] and [macroref BOOST_CONTRACT_NAMED_OVERRIDE]). diff --git a/doc/full_table_of_contents.qbk b/doc/full_table_of_contents.qbk index b9ab12f..37d2d65 100644 --- a/doc/full_table_of_contents.qbk +++ b/doc/full_table_of_contents.qbk @@ -32,32 +32,32 @@ __Tutorial__ __Destructors__ __Public_Functions__ __Virtual_Public_Functions__ - __Public_Function_Overrides__ (Subcontracting) - __Base_Classes__ (Subcontracting) + __Public_Function_Overrides_Subcontracting__ + __Base_Classes_Subcontracting__ __Static_Public_Functions__ -__Advanced_Topics__ +__Advanced__ __Pure_Virtual_Public_Functions__ __Optional_Return_Value__ __Private_and_Protected_Functions__ __Friend_Functions__ __Function_Overloads__ - __Lambdas_Loops_Code_Blocks_Etc__ + __Lambdas_Loops_Code_Blocks_and_constexpr__ __Implementation_Checks__ __Old_Values_at_Body__ __Named_Overrides__ __Access_Specifiers__ - __Throw_on_Failure__ -__Extra_Topics__ - __Old_Value_Requirements__ (Templates) - __Assertion_Requirements__ (Templates) + __Throw_on_Failure_and_noexcept__ +__Extras__ + __Old_Value_Requirements_Templates__ + __Assertion_Requirements_Templates__ __Volatile_Public_Functions__ __Move_Operations__ __Unions__ - __Disable_Contract_Checking__ - __Disable_Contract_Compilation__ (Macro Interface) + __Disable_Contract_Checking_and_Assertion_Levels__ + __Disable_Contract_Compilation_Macro_Interface__ __Separate_Body_Implementation__ - __No_Lambda_Functions__ (No C++11) - __No_Macros__ (No C++11) + __No_Lambda_Functions_No_CXX11__ + __No_Macros_and_No_Variadic_Macros__ __Reference__ __Examples__ __Release_Notes__ diff --git a/doc/introduction.qbk b/doc/introduction.qbk index 0463757..68a9de4 100644 --- a/doc/introduction.qbk +++ b/doc/introduction.qbk @@ -15,9 +15,9 @@ For example, consider the following function `inc` that increments its argument [introduction_comments] The precondition states that at function entry the argument `x` must be strictly smaller than the maximum allowable value of its type (so it can be increased by `1` without overflowing). -The postcondition states that at function exit the argument `x` must be incremented by `1` with respect to the value it had before executing the function `old(x)` (but noting that postconditions are checked only when the execution of the function body did not throw an exception). +The postcondition states that at function exit the argument `x` must be incremented by `1` with respect to the value it had before executing the function indicated with `oldof(x)` (note that postconditions should be checked only when the execution of the function body did not throw an exception). -Now let's program this function and its contract using this library (see also [@../../example/features/introduction.cpp introduction.cpp]): +Now let's program this function and its contract using this library (see also [@../../example/features/introduction.cpp =introduction.cpp=]): [import ../example/features/introduction.cpp] [introduction] @@ -51,13 +51,30 @@ Note that the error messages printed by this library contain all the information The assertion failure message printed by this library follows a format similar to the message printed by Clang when the C-style `assert` macro fails. ] -In addition to contracts for simple non-member functions as shown the in the example above, this library allows to program contracts for constructors, destructors, and member functions. -These can check class invariants and can also /subcontract/ inheriting and extending contracts for derived classes (see __Tutorial__ and also __Advanced_Topics__). - [note C++11 lambda functions are necessary to use this library without having to manually program a significant amount of boiler-plate code (see __No_Lambda_Functions__). -Otherwise this library does not use other C++11 features and should work on most modern C++ compilers (see __Getting_Started__). +Otherwise, this library does not use other C++11 features and should work on most modern C++ compilers (see __Getting_Started__). ] +In addition to contracts for simple non-member functions as shown the in the example above, this library allows to program contracts for constructors, destructors, and member functions. +These can check class invariants and can also /subcontract/ inheriting and extending contracts for derived classes (see also [@../../example/features/introduction_public.cpp =introduction_public.cpp=] and __Public_Function_Overrides__): +[footnote +The `pushable` base class is used here just to exercise subcontracting, it is somewhat arbitrary and it would likely not appear in real production code. +] + +[import ../example/features/introduction_public.cpp] +[introduction_public] + +[heading Language Support] + +The authors of this library advocate for contracts to be added to the core language. +Adding contract programming to the C++ standard has a number of advantages over any library implementation (shorter and more concise syntax to program contracts, specify contracts in declarations instead of definitions, enforce contract constant-correctness, expected faster compile and run times, vendors could develop static analysis tools to recognize and check contracts statically when possible, compiler optimization could be improved based on contract conditions, etc.). + +Unfortunately, detailed and complete proposals to add contracts to the C++ standard such as __N1962__ were rejected by the C++ standard committee and it is not clear if the current proposal for adding contracts to C++ __P0380R1__ will actually be accepted by the standard. +[footnote +The authors find attractive the idea of using C++ attributes to specify contracts as indicated in __P0380R1__. +] +In any case, __P0380R1__ only supports pre- and postconditions while lacking basic features such as class invariants and old values in postconditions, not to mention the lack of more advanced features like subcontracting, all these features are instead supported by this library (see __Feature_Summary__ for a detailed comparison between the features supported by this library and the ones listed in different contract programming proposals, see also __Bibliography__ for a list of references considered in designing and implementing this library including the vast majority of contract programming proposals submitted to the C++ standard committee). + [endsect] diff --git a/doc/main.qbk b/doc/main.qbk index 56432c1..a095994 100644 --- a/doc/main.qbk +++ b/doc/main.qbk @@ -31,7 +31,7 @@ [def __Constant_Correctness__ [link boost_contract.contract_programming_overview.constant_correctness Constant-Correctness]] [def __Specification_vs_Implementation__ [link boost_contract.contract_programming_overview.specification_vs__implementation Specification vs. Implementation]] [def __On_Contract_Failure__ [link boost_contract.contract_programming_overview.on_contract_failure On Contract Failure]] -[def __Feature_Summary__ [link boost_contract.contract_programming_overview.features_summary Feature Summary]] +[def __Feature_Summary__ [link boost_contract.contract_programming_overview.feature_summary Feature Summary]] [def __Tutorial__ [link boost_contract.tutorial Tutorial]] [def __Non_Member_Functions__ [link boost_contract.tutorial.non_member_functions Non-Member Functions]] @@ -46,33 +46,43 @@ [def __Public_Functions__ [link boost_contract.tutorial.public_functions Public Functions]] [def __Virtual_Public_Functions__ [link boost_contract.tutorial.virtual_public_functions Virtual Public Functions]] [def __Public_Function_Overrides__ [link boost_contract.tutorial.public_function_overrides__subcontracting_ Public Function Overrides]] +[def __Public_Function_Overrides_Subcontracting__ [link boost_contract.tutorial.public_function_overrides__subcontracting_ Public Function Overrides (Subcontracting)]] [def __Base_Classes__ [link boost_contract.tutorial.base_classes__subcontracting_ Base Classes]] +[def __Base_Classes_Subcontracting__ [link boost_contract.tutorial.base_classes__subcontracting_ Base Classes (Subcontracting)]] [def __Static_Public_Functions__ [link boost_contract.tutorial.static_public_functions Static Public Functions]] -[def __Advanced_Topics__ [link boost_contract.advanced_topics Advanced Topics]] -[def __Pure_Virtual_Public_Functions__ [link boost_contract.advanced_topics.pure_virtual_public_functions Pure Virtual Public Functions]] -[def __Optional_Return_Value__ [link boost_contract.advanced_topics.optional_return_value Optional Return Value]] -[def __Private_and_Protected_Functions__ [link boost_contract.advanced_topics.private_and_protected_functions Private and Protected Functions]] -[def __Friend_Functions__ [link boost_contract.advanced_topics.friend_functions Friend Functions]] -[def __Function_Overloads__ [link boost_contract.advanced_topics.function_overloads Function Overloads]] -[def __Lambdas_Loops_Code_Blocks_Etc__ [link boost_contract.advanced_topics.lambdas__loops__code_blocks__etc_ Lambdas, Loops, Code Blocks, Etc.]] -[def __Implementation_Checks__ [link boost_contract.advanced_topics.implementation_checks Implementation Checks]] -[def __Old_Values_at_Body__ [link boost_contract.advanced_topics.old_values_at_body Old Values at Body]] -[def __Named_Overrides__ [link boost_contract.advanced_topics.named_overrides Named Overrides]] -[def __Access_Specifiers__ [link boost_contract.advanced_topics.access_specifiers Access Specifiers]] -[def __Throw_on_Failure__ [link boost_contract.advanced_topics.throw_on_failure Throw on Failure]] +[def __Advanced__ [link boost_contract.advanced Advanced]] +[def __Pure_Virtual_Public_Functions__ [link boost_contract.advanced.pure_virtual_public_functions Pure Virtual Public Functions]] +[def __Optional_Return_Value__ [link boost_contract.advanced.optional_return_value Optional Return Value]] +[def __Private_and_Protected_Functions__ [link boost_contract.advanced.private_and_protected_functions Private and Protected Functions]] +[def __Friend_Functions__ [link boost_contract.advanced.friend_functions Friend Functions]] +[def __Function_Overloads__ [link boost_contract.advanced.function_overloads Function Overloads]] +[def __Lambdas_Loops_Code_Blocks__ [link boost_contract.advanced.lambdas__loops__code_blocks__and_constexpr_ Lambdas, Loops, Code Blocks]] +[def __Lambdas_Loops_Code_Blocks_and_constexpr__ [link boost_contract.advanced.lambdas__loops__code_blocks__and_constexpr_ Lambdas, Loops, Code Blocks (and `constexpr`)]] +[def __Implementation_Checks__ [link boost_contract.advanced.implementation_checks Implementation Checks]] +[def __Old_Values_at_Body__ [link boost_contract.advanced.old_values_at_body Old Values at Body]] +[def __Named_Overrides__ [link boost_contract.advanced.named_overrides Named Overrides]] +[def __Access_Specifiers__ [link boost_contract.advanced.access_specifiers Access Specifiers]] +[def __Throw_on_Failure__ [link boost_contract.advanced.throw_on_failure__and_noecept_ Throw on Failure]] +[def __Throw_on_Failure_and_noexcept__ [link boost_contract.advanced.throw_on_failure__and_noecept_ Throw on Failure (and `noexcept`)]] -[def __Extra_Topics__ [link boost_contract.extra_topics Extra Topics]] -[def __Old_Value_Requirements__ [link boost_contract.extra_topics.old_value_requirements__templates_ Old Value Requirements]] -[def __Assertion_Requirements__ [link boost_contract.extra_topics.assertion_requirements__templates_ Assertion Requirements]] -[def __Volatile_Public_Functions__ [link boost_contract.extra_topics.volatile_public_functions Volatile Public Functions]] -[def __Move_Operations__ [link boost_contract.extra_topics.move_operations Move Operations]] -[def __Unions__ [link boost_contract.extra_topics.unions Unions]] -[def __Disable_Contract_Checking__ [link boost_contract.extra_topics.disable_contract_checking Disable Contract Checking]] -[def __Disable_Contract_Compilation__ [link boost_contract.extra_topics.disable_contract_compilation__macro_interface_ Disable Contract Compilation]] -[def __Separate_Body_Implementation__ [link boost_contract.extra_topics.separate_body_implementation Separate Body Implementation]] -[def __No_Lambda_Functions__ [link boost_contract.extra_topics.no_lambda_functions__no_c__11_ No Lambda Functions]] -[def __No_Macros__ [link boost_contract.extra_topics.no_macros__no_c__11_ No Macros]] +[def __Extras__ [link boost_contract.extras Extras]] +[def __Old_Value_Requirements__ [link boost_contract.extras.old_value_requirements__templates_ Old Value Requirements]] +[def __Old_Value_Requirements_Templates__ [link boost_contract.extras.old_value_requirements__templates_ Old Value Requirements (Templates)]] +[def __Assertion_Requirements__ [link boost_contract.extras.assertion_requirements__templates_ Assertion Requirements]] +[def __Assertion_Requirements_Templates__ [link boost_contract.extras.assertion_requirements__templates_ Assertion Requirements (Templates)]] +[def __Volatile_Public_Functions__ [link boost_contract.extras.volatile_public_functions Volatile Public Functions]] +[def __Move_Operations__ [link boost_contract.extras.move_operations Move Operations]] +[def __Unions__ [link boost_contract.extras.unions Unions]] +[def __Disable_Contract_Checking__ [link boost_contract.extras.disable_contract_checking Disable Contract Checking]] +[def __Disable_Contract_Checking_and_Assertion_Levels__ [link boost_contract.extras.disable_contract_checking__and_assertion_levels_ Disable Contract Checking (and Assertion Levels)]] +[def __Disable_Contract_Compilation__ [link boost_contract.extras.disable_contract_compilation__macro_interface_ Disable Contract Compilation]] +[def __Disable_Contract_Compilation_Macro_Interface__ [link boost_contract.extras.disable_contract_compilation__macro_interface_ Disable Contract Compilation (Macro Interface)]] +[def __Separate_Body_Implementation__ [link boost_contract.extras.separate_body_implementation Separate Body Implementation]] +[def __No_Lambda_Functions__ [link boost_contract.extras.no_lambda_functions__no_c__11_ No Lambda Functions]] +[def __No_Lambda_Functions_No_CXX11__ [link boost_contract.extras.no_lambda_functions__no_c__11_ No Lambda Functions (No C++11)]] +[def __No_Macros__ [link boost_contract.extras.no_macros__and_no_variadic_macros_ No Macros]] +[def __No_Macros_and_No_Variadic_Macros__ [link boost_contract.extras.no_macros__and_no_variadic_macros_ No Macros (and No Variadic Macros)]] [def __Reference__ [@reference.html Reference]] [def __Examples__ [link boost_contract.examples Examples]] @@ -102,6 +112,7 @@ [def __N2081__ [link N2081_anchor \[N2081\]]] [def __N2914__ [link N2914_anchor \[N2914\]]] [def __N3613__ [link N3613_anchor \[N3613\]]] +[def __P0380__ [link P0380_anchor \[P0380\]]] [def __SPARKAda__ [link SPARKAda_anchor \[SPARKAda\]]] [def __SpecSharp__ [link SpecSharp_anchor \[SpecSharp\]]] [def __Stroustrup94__ [link Stroustrup94_anchor \[Stroustrup94\]]] @@ -119,7 +130,7 @@ This library implements Design by Contract (DbC) is a registered trademark of the Eiffel Software company and it was first introduced by the Eiffel programming language (see __Meyer97__). ] for the C++ programming language. -All Contract Programming features are supported by this library: subcontracting, class invariants (also for static and volatile member functions), postconditions (with old and return values), preconditions, customizable actions on assertion failure (e.g., terminate the program or throw an exception), optional compilation of assertions, disable assertions while already checking other assertions (to avoid infinite recursion), etc. +All Contract Programming features are supported by this library: subcontracting, class invariants (also for static and volatile member functions), postconditions (with old and return values), preconditions, customizable actions on assertion failure (e.g., terminate the program or throw an exception), optional compilation of assertions, disable assertions while already checking other assertions (to avoid infinite recursion), etc. (see __Feature_Summary__). [note In one of its previous revisions, this library passed Boost formal review and it was accepted into the Boost libraries (see [@https://groups.google.com/forum/?fromgroups=#!topic/boost-list/jQ7OjAmos_Y]). @@ -133,8 +144,8 @@ This library source is hosted at [@https://github.com/lcaminiti/boost-contract]. [include getting_started.qbk] [include contract_programming_overview.qbk] [include tutorial.qbk] -[include advanced_topics.qbk] -[include extra_topics.qbk] +[include advanced.qbk] +[include extras.qbk] [xinclude reference.xml] [include examples.qbk] [include release_notes.qbk] diff --git a/doc/tutorial.qbk b/doc/tutorial.qbk index c3f38f5..7cf0ee3 100644 --- a/doc/tutorial.qbk +++ b/doc/tutorial.qbk @@ -45,6 +45,7 @@ At destruction instead (enclosing function exit): # Check exception guarantees, by calling the nullary functor [^['e]]`()` passed to `.except(`[^['e]]`)`. This ensures that non-member function contracts are correctly checked at run-time (see __Function_Calls__). +(Also note that functions will correctly check their contracts even when they are called via function pointers or function objects.) [note A non-member function can avoid calling [funcref boost::contract::function] for efficiency but only when it has no preconditions, no postconditions, and no exception guarantees. @@ -189,8 +190,8 @@ For example, for [funcref boost::contract::function] (but same for all other con Old values are handled by this library using the smart pointer class template [classref boost::contract::old_ptr] (so programmers do not directly manage the allocation and deallocation of the pointed memory). [footnote *Rationale:* -Old values are optional values because they need to be left uninitialized in case postconditions and exception guarantees are disabled defining [macroref BOOST_CONTRACT_NO_POSTCONDITIONS] and [macroref BOOST_CONTRACT_NO_EXCEPTS] to avoid old value copies in that case (so a pointer or better a `boost::optional` could be used for that). -Furthermore, old values need to be pointers internally allocated by this library so that they are never copied twice even when calling an overridden function multiple times to check preconditions, postconditions, etc. to implement subcontracting (so a smart pointer class template was used). +Old values are optional values because they need to be left uninitialized in case postconditions and exception guarantees are disabled defining [macroref BOOST_CONTRACT_NO_POSTCONDITIONS] and [macroref BOOST_CONTRACT_NO_EXCEPTS] to avoid old value copies in that case (so a pointer or better a `boost::optional` can be used for that). +In addition, old values need to be pointers internally allocated by this library so that they are never copied twice even when calling an overridden function multiple times to check preconditions, postconditions, etc. to implement subcontracting (so a smart pointer class template was used). ] The pointed old value is automatically qualified as `const` (so old values cannot be mistakenly changed by the contract assertions, see __Constant_Correctness__). This library ensures that old value pointers are always not null by the time postconditions and exception guarantees are checked (so programmers can safely dereference these pointers in postcondition and exception-guarantee assertions using `operator*` or `operator->` without having to check if old value pointers are not null first). diff --git a/example/Jamfile.v2 b/example/Jamfile.v2 index c6c9eba..753cae9 100644 --- a/example/Jamfile.v2 +++ b/example/Jamfile.v2 @@ -8,8 +8,9 @@ make help : : help_exit ; explicit help ; test-suite features : - [ subdir-run features : introduction ] [ subdir-run features : introduction_comments ] + [ subdir-run features : introduction ] + [ subdir-run features : introduction_public ] [ subdir-run features : non_member ] [ subdir-run features : lambda ] @@ -42,6 +43,7 @@ test-suite features : [ subdir-run features : separate_body ] [ subdir-run features : throw_on_failure ] [ subdir-run features : ifdef ] + [ subdir-run features : ifdef_audit ] [ subdir-run features : ifdef_macro ] [ subdir-run features : base_types_no_macro ] [ subdir-run features : old_no_macro ] diff --git a/example/features/ifdef_audit.cpp b/example/features/ifdef_audit.cpp new file mode 100644 index 0000000..ba3458f --- /dev/null +++ b/example/features/ifdef_audit.cpp @@ -0,0 +1,56 @@ + +// Copyright (C) 2008-2016 Lorenzo Caminiti +// Distributed under the Boost Software License, Version 1.0 (see accompanying +// file LICENSE_1_0.txt or a copy at http://www.boost.org/LICENSE_1_0.txt). +// See: http://www.boost.org/doc/libs/release/libs/contract/doc/html/index.html + +#include +#include +#include +#include + +#define CONTRACT_AUDIT // Check "audit" assertions for this example. + +//[ifdef_audit +// #define this only when willing to check expensive assertions. +#ifdef CONTRACT_AUDIT + #define CONTRACT_ASSERT_AUDIT(cond) BOOST_CONTRACT_ASSERT(cond) +#else + #define CONTRACT_ASSERT_AUDIT(cond) BOOST_CONTRACT_ASSERT(true || (cond)) +#endif + +// Prohibitively expensive assertions, never checked (same as formal comments). +#define CONTRACT_ASSERT_AXIOM(cond) BOOST_CONTRACT_ASSERT(true || (cond)) + +template +bool random_binary_search(RandomIter first, RandomIter last, T const& value) { + boost::contract::check c = boost::contract::function() + .precondition([&] { + BOOST_CONTRACT_ASSERT(first <= last); + // Expensive O(n) assertion so marked "audit". + CONTRACT_ASSERT_AUDIT(std::is_sorted(first, last)); + }) + ; + + /* ... */ +//] + + while(first < last) { + RandomIter middle = first + ((last - first) >> 1); + BOOST_CONTRACT_CHECK(*first <= *middle || value < *middle || + *middle < value); + + if(value < *middle) last = middle; + else if(value > *middle) first = middle + 1; + else return true; + } + return false; +} + +int main() { + std::vector i(3); + i[0] = 'a'; i[1] = 'b'; i[2] = 'c'; + assert(random_binary_search(i.begin(), i.end(), 'b')); + return 0; +} + diff --git a/example/features/introduction.cpp b/example/features/introduction.cpp index 455b387..898f765 100644 --- a/example/features/introduction.cpp +++ b/example/features/introduction.cpp @@ -11,7 +11,7 @@ #include void inc(int& x) { - boost::contract::old_ptr old_x = BOOST_CONTRACT_OLDOF(x); + boost::contract::old_ptr old_x = BOOST_CONTRACT_OLDOF(x); // Old values. boost::contract::check c = boost::contract::function() .precondition([&] { BOOST_CONTRACT_ASSERT(x < std::numeric_limits::max()); // Line 17. diff --git a/example/features/introduction_comments.cpp b/example/features/introduction_comments.cpp index d0c5a92..81191a0 100644 --- a/example/features/introduction_comments.cpp +++ b/example/features/introduction_comments.cpp @@ -9,7 +9,7 @@ //[introduction_comments void inc(int& x) // Precondition: x < std::numeric_limit::max() - // Postcondition: x == old(x) + 1 + // Postcondition: x == oldof(x) + 1 { ++x; // Function body. } diff --git a/example/features/introduction_public.cpp b/example/features/introduction_public.cpp new file mode 100644 index 0000000..d7c978e --- /dev/null +++ b/example/features/introduction_public.cpp @@ -0,0 +1,89 @@ + +// Copyright (C) 2008-2016 Lorenzo Caminiti +// Distributed under the Boost Software License, Version 1.0 (see accompanying +// file LICENSE_1_0.txt or a copy at http://www.boost.org/LICENSE_1_0.txt). +// See: http://www.boost.org/doc/libs/release/libs/contract/doc/html/index.html + +#include +#include +#include + +template +class pushable { // Somewhat arbitrary base (used just to show subcontracting). +public: + void invariant() const { + BOOST_CONTRACT_ASSERT(capacity() <= max_size()); + } + + virtual void push_back(T const& value, + boost::contract::virtual_* v = 0) = 0; // Pure virtual function. + +protected: + virtual unsigned capacity() const = 0; + virtual unsigned max_size() const = 0; +}; + +template // Contract for pure virtual function. +void pushable::push_back(T const& value, boost::contract::virtual_* v) { + boost::contract::old_ptr old_capacity = + BOOST_CONTRACT_OLDOF(v, capacity()); + boost::contract::guard c = boost::contract::public_function(v, this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(capacity() < max_size()); + }) + .postcondition([&] { + BOOST_CONTRACT_ASSERT(capacity() >= *old_capacity); + }) + ; + assert(false); // Shall never execute this body. +} + +//[introduction_public +template +class vector + #define BASES public pushable + : BASES +{ +public: + typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; // For subcontracting. + #undef BASES + + void invariant() const { // Checked in AND with base class invariants. + BOOST_CONTRACT_ASSERT(size() <= capacity()); + } + + virtual void push_back(T const& value, + boost::contract::virtual_* v = 0) /* override */ { // Tag virtuals. + boost::contract::old_ptr old_size = + BOOST_CONTRACT_OLDOF(v, size()); // Old values for virtuals. + boost::contract::guard c = boost::contract::public_function< // For overrides. + override_push_back>(v, &vector::push_back, this, value) + .precondition([&] { // Checked in OR with base preconditions. + BOOST_CONTRACT_ASSERT(size() < max_size()); + }) + .postcondition([&] { // Checked in AND with base postconditions. + BOOST_CONTRACT_ASSERT(size() == *old_size + 1); + }) + ; + + vect_.push_back(value); + } + BOOST_CONTRACT_OVERRIDE(push_back) // Define `override_push_back` above. + + // 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 vect_; +}; +//] + +int main() { + vector vect; + vect.push_back(123); + assert(vect.size() == 1); + return 0; +} + diff --git a/example/n1962/vector.cpp b/example/n1962/vector.cpp index 5c06866..41b8d11 100644 --- a/example/n1962/vector.cpp +++ b/example/n1962/vector.cpp @@ -470,12 +470,15 @@ public: iterator result; boost::contract::old_ptr old_size = BOOST_CONTRACT_OLDOF(size()); + boost::contract::old_ptr old_capacity = + BOOST_CONTRACT_OLDOF(capacity()); boost::contract::check c = boost::contract::public_function(this) .precondition([&] { BOOST_CONTRACT_ASSERT(size() < max_size()); }) .postcondition([&] { BOOST_CONTRACT_ASSERT(size() == *old_size + 1); + BOOST_CONTRACT_ASSERT(capacity() >= *old_capacity); BOOST_CONTRACT_ASSERT( boost::contract::condition_if >( boost::bind(std::equal_to(), boost::cref(*result), @@ -531,6 +534,8 @@ public: BOOST_CONTRACT_OLDOF(size()); boost::contract::old_ptr old_capacity = BOOST_CONTRACT_OLDOF(capacity()); + boost::contract::old_ptr old_where = + BOOST_CONTRACT_OLDOF(where); boost::contract::check c = boost::contract::public_function(this) .precondition([&] { BOOST_CONTRACT_ASSERT(size() + std::distance(first, last) < @@ -541,6 +546,19 @@ public: BOOST_CONTRACT_ASSERT(size() == *old_size() + std::distance(first, last)); BOOST_CONTRACT_ASSERT(capacity() >= *old_capacity); + if(capacity() == *old_capacity) { + BOOST_CONTRACT_ASSERT( + boost::contract::condition_if >( + boost::bind(all_of_equal_to(), + boost::prior(*old_where), + boost::prior(*old_where) + count, + boost::cref(value) + ) + ) + ); + // [where, end()) is invalid + } + // else [begin(), end()) is invalid }) ; @@ -600,6 +618,9 @@ public: boost::contract::old_ptr old_other = BOOST_CONTRACT_OLDOF(other); boost::contract::check c = boost::contract::public_function(this) + .precondition([&] { + BOOST_CONTRACT_ASSERT(get_allocator() == other.get_allocator()); + }) .postcondition([&] { BOOST_CONTRACT_ASSERT( boost::contract::condition_if= oldof capacity(); if constexpr(boost::has_equal_to::value) { *result == value; } @@ -492,6 +493,8 @@ public: + + void insert(iterator where, size_type count, T const& value) precondition { size() + count < max_size(); @@ -534,6 +537,14 @@ public: postcondition { size() == oldof size() + std::distance(first, last); capacity() >= oldof capacity(); + if constexpr(boost::has_equal_to::value) { + if(capacity() == oldof capacity()) { + boost::algorithm::all_of_equal(boost::prior(oldof where), + boost::prior(oldof where) + count, value); + } + // [where, end()) is invalid + } + // else [begin(), end()) is invalid } { vect_.insert(where, first, last); @@ -547,6 +558,13 @@ public: + + + + + + + iterator erase(iterator where) precondition { !empty(); @@ -596,6 +614,9 @@ public: void swap(vector& other) + precondition { + get_allocator() == other.get_allocator(); + } postcondition { if constexpr(boost::has_equal_to::value) { *this == oldof other; diff --git a/include/boost/contract.hpp b/include/boost/contract.hpp index 44866bc..660c545 100644 --- a/include/boost/contract.hpp +++ b/include/boost/contract.hpp @@ -25,10 +25,6 @@ never be used directly by programmers. @see @RefSect{getting_started, Getting Started} */ -// TODO: Documentation updates based on all emails to Boost (review all emails). - -// TODO: Documentation updates based on all n-papers that I read recently (review notes I wrote on all papers), add those n-papers to the Bibliography section, and add P0380 (the most recent proposal) to the feature comparison table. - #include #include #include