[:['["It is absurd to make elaborate security checks on debugging runs, when no trust is put in the results, and then remove them in production runs, when an erroneous result could be expensive or disastrous. What would we think of a sailing enthusiast who wears his life-jacket when training on dry land but takes it off as soon as he goes to sea?]]]
[:['-- Charles Antony Richard Hoare (see __Hoare73__)]]
-This section gives an overview of contract programming (see __Meyer97__, __Mitchell02__, and __N1613__ for more detailed introductions to contract programming).
+This section gives an overview of contract programming (see __Meyer97__, __Mitchell02__, and __N1613__ for more extensive introductions to contract programming).
Readers that already have a basic understanding of contract programming can skip this section and maybe come back to it after reading the __Tutorial__.
[note
The objective of this library is not to convince programmers to use contract programming.
It is assumed that programmes understand the benefits and trade-offs associated with contract programming and they have already decided to use this methodology in their code.
-Then, this library aims to be the best and more complete contract programming library for C++ (without using preprocessors and other tools external to the C++ preprocessor and language itself).
+Then, this library aims to be the best and more complete contract programming library for C++ (without using programs and tools external to the C++ language and its preprocessor).
]
[section Assertions]
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 to operations that have preconditions which are often referred to as having a /narrow contract/ (note that operations with truly narrow contracts are expected to also never throw exceptions).
+Operations that logically have no preconditions (i.e., that are always well-defined for the entire domain of their inputs) are also referred to as having a /wide contract/.
+This is in contrast to operations that have preconditions which are also referred to as having a /narrow contract/ (note that operations with truly narrow contracts are also expected to never throw exceptions because the implementation body of these operations is always expected to succeed after its preconditions are checked to be true).
[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 just because the authors generally prefer to explicitly mention "this operation has no preconditions..." or "this operation has preconditions...".
+This nomenclature is perfectly reasonable but it is not often used in this document just because the authors usually prefer to explicitly say "this operation has no preconditions..." or "this operation has preconditions..." (this is just a matter of taste).
]
* /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 also /old values/ (which are the values that expressions had before the function body was executed).
+Postconditions can access the function return value (for non-void functions) and also /old values/ (which are the values that expressions had before the function implementation was executed).
* /Exception guarantees/: These are logical conditions that programmers except to be true when a function exits throwing an exception.
Exception guarantees can access old values (but not the function return value).
[footnote
*Rationale:*
-Contract assertions for exception guarantees were first introduced by this library (even if exception safety guarantees have long been part of C++ STL documentation).
-Contract assertions for exception safety guarantees are not part of __N1962__ or other references listed in the __Bibliography__.
+Contract assertions for exception guarantees were first introduced by this library, they are not part of __N1962__ or other references listed in the __Bibliography__ (even if exception safety guarantees have long been part of C++ STL documentation).
]
* /Class invariants/: These are logical conditions that programmers expect to be true after a constructor exits without throwing an exception, before and after the execution of every non-static public function (even if they throw exceptions), before the destructor is executed (and also after the destructor is executed but only when the destructor throws an exception).
Class invariants define valid states for all objects of a given class.
-It is possible to specify a different set of class invariants for volatile public functions, namely volatile class invariants.
+It is possible to specify a different set of class invariants for volatile public functions, namely /volatile class invariants/.
It is also possible to specify /static class invariants/ which are excepted to be true before and after the execution of any constructor, destructor (even if it does not throw an exception), and public function (even if static).
[footnote
*Rationale:*
-Static and volatile class invariants were first introduced by this library to reflect the fact that C++ supports both static and volatile public functions.
-Static and volatile class invariants are not part of __N1962__ or other references listed in the __Bibliography__.
+Static and volatile class invariants were first introduced by this library (simply to reflect the fact that C++ supports also static and volatile public functions), they are not part of __N1962__ or other references listed in the __Bibliography__.
]
* /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__).
-Class invariants can also be used to specify /basic/ exception safety guarantees for an object (because they are checked at exit of public functions even when those throw exceptions), while contract assertions for exception guarantees can be used to specify /strong/ exception safety guarantees for given operations on the same object.
+The actual function implementation code, that remains outside of these contract assertions, is often referred to as the /function body/ in contract programming.
+
+Class invariants can also be used to specify /basic/ exception safety guarantees for an object (because they are checked at exit of public functions even when those throw exceptions).
+Contract assertions for exception guarantees can be used to specify /strong/ exception safety guarantees for a given operation on the same object.
It is also 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).
[heading C-Style Assertions]
-A limited form of contract programming is the use of the C-style `assert` macro.
+A limited form of contract programming (typically some form of precondition and basic postcondition checking) can be achieved using the C-style `assert` macro.
Using `assert` is common practice for many programmers but it suffers of the following limitations:
* `assert` does not distinguish between preconditions and postconditions.
-In well-tested production code, postconditions can usually be disabled trusting the correctness of the implementation while preconditions might still need to remain enabled because of possible changes in the calling code (e.g., postconditions of a given library could be disabled after testing while its preconditions can be kept enabled given the library cannot predict changes in the user code that will be calling the library).
+In well-tested production code, postconditions can usually be disabled trusting the correctness of the implementation while preconditions might still need to remain enabled because of possible changes in the calling code (e.g., postconditions of a given library could be disabled after testing while keeping the library preconditions enabled given that future changes in the user code that calls the library cannot be anticipated).
Using `assert` it is not possible to selectively disable only postconditions and all assertions must be disabled at once.
+* `assert` requires to manually program extra code to correctly check postconditions (specifically to handle functions with multiple return statements, to not check postconditions when functions throw exceptions, and to implement old values).
* `assert` requires to manually program extra code to check class invariants (extra member functions, try blocks, etc.).
* `assert` does not support subcontracting.
* `assert` calls are usually scattered within function implementations thus the asserted conditions are not immediately visible in their entirety by programmers (as they are instead when the assertions appear in the function declaration or at least at the very top of the function definition).
-Contract programming does not suffers of these limitations.
+Contract programming does not suffer of these limitations.
[endsect]
The main use of contract programming is to improve software quality.
__Meyer97__ discusses how contract programming can be used as the basic tool to write ["correct] software.
__Stroustrup94__ discusses the key importance of class invariants plus advantages and disadvantages of preconditions and postconditions.
+
The following is a short summary of benefits associated with contract programming inspired mainly by __N1613__:
* Preconditions and postconditions:
Contracts are part of the source code, they are checked at run-time so they are always up-to-date with the code itself.
Therefore program specifications, as documented by the contracts, can be trusted to always be up-to-date with the implementation.
* Easier debugging:
-Contract programming can provide a powerful debugging facility because, if contracts are well written, bugs will cause contract assertions to fail exactly where the problem first occurs instead than at some later stage of the program execution in an apparently unrelated (and often hard to debug) manner.
+Contract programming can provide a powerful debugging facility because, if contracts are well-written, bugs will cause contract assertions to fail exactly where the problem first occurs instead than at some later stage of the program execution in an apparently unrelated (and often hard to debug) manner.
Note that a precondition failure points to a bug in the function caller, a postcondition failure points instead to a bug in the function implementation.
[footnote
Of course, if contracts are ill-written then contract programming is of little use.
]
* Easier testing:
Contract programming facilitates testing because a contract naturally specifies what a test should check.
-For example, preconditions of a function state which inputs cause the function to fail and postconditions state which outputs are produced by the function on successful exit (contract programming should be seen as a tool to complement, but obviously not to replace, testing).
+For example, preconditions of a function state which inputs cause the function to fail and postconditions state which outputs are produced by the function on successful exit (contract programming should be seen as a tool to complement and guide, but obviously not to replace, testing).
* Formal design:
-Contract programming can serve to reduce the gap between designers and programmers by providing a precise and unambiguous specification language in terms of the contract assertions.
+Contract programming can serve to reduce the gap between designers and programmers by providing a precise and unambiguous specification language in terms of contract assertions.
Moreover, contracts can make code reviews easier by clarifying some of the semantics and usage of the code.
-* Formalized inheritance:
+* Formalize inheritance:
Contract programming formalizes the virtual function overriding mechanism using subcontracting as justified by the __substitution_principle__.
This keeps the base class programmers in control as overriding functions always have to fully satisfy the contracts of their base classes.
* Replace defensive programming:
Contract programming assertions can replace [@http://en.wikipedia.org/wiki/Defensive_programming defensive programming] checks localizing these checks within the contracts and making the code more readable.
Of course, not all formal contract specifications can be asserted 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.
+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 it reaches the second iterator, but if the iterator range is invalid then such a code would render undefined behaviour or run forever instead of failing an assertion).
Nevertheless, a large amount of contract assertions can be successfully programmed in C++ as illustrated by the numerous examples in this documentation and from the literature (for example see how much of STL [link N1962_vector_anchor `vector`] contract assertions can actually be programmed in C++ using this library).
[heading Costs]
* Check the asserted conditions.
* Copy old values when these are used in postconditions or exception guarantees.
-* Call additional functors that check preconditions, postconditions, exception guarantees, class invariants, etc. (especially for subcontracting).
+* Call additional functors that check preconditions, postconditions, exception guarantees, class invariants, etc. (these can add up to many extra calls especially when using subcontracting).
[note
In general, contracts introduce at least three extra functor calls to check preconditions, postconditions, and exception guarantees for any given non-member function call.
]
To mitigate the run-time performance impact, programmers can selectively disable run-time checking of some of the contract assertions.
-Programmers will have to decide based on the performance trade-offs required by their applications, but a reasonable approach often is to (see __Disable_Contract_Checking__):
+Programmers will have to decide based on the performance trade-offs required by their specific applications, but a reasonable approach often is to (see __Disable_Contract_Checking__):
* Always write contracts to clarify the semantics of the design embedding the specifications directly in the code and making the code self-documenting.
* Check preconditions, postconditions, class invariants, and maybe even exception guarantees during initial testing.
Private and protected functions do not have to satisfy class invariants because these functions are part of the class implementation and not of the class public interface.
Furthermore, the __substitution_principle__ does not apply to private and protected functions because these functions are not accessible to the user at the calling site where the __substitution_principle__ applies.
-Therefore, calls to private and protected functions with contracts execute the same steps as the ones indicated above for non-member functions (checking only preconditions and postconditions, without checking class invariants and subcontracting).
+Therefore, calls to private and protected functions with contracts execute the same steps as the ones indicated above for non-member functions (checking only preconditions and postconditions, without checking class invariants and without subcontracting).
[endsect]
[heading Overriding Public Functions]
-Let's consider a public function in a derived class that overrides public virtual functions declared its public base classes (because of C++ multiple inheritance, the function could override from more than one of its base classes).
+Let's consider a public function in a derived class that overrides public virtual functions declared by its public base classes (because of C++ multiple inheritance, the function could override from more than one of its base classes).
We refer to the function in the derived class as the /overriding function/, and to the set of base classes containing all the /overridden functions/ as /overridden bases/.
-When subcontracting, overridden functions are searched (at compile-time) deeply in the public branches of the inheritance tree (i.e., not just the derived class's direct public parents are inspected, but also all its public grandparents, etc.).
-In case of multiple inheritance this search also extends widely to all multiple public base classes following their order of declaration in the derived class inheritance list (as usual in C++, this search could result in multiple overridden functions and therefore in subcontracting from multiple public base classes).
+When subcontracting, overridden functions are searched (at compile-time) deeply in all public branches of the inheritance tree (i.e., not just the derived class' direct public parents are inspected, but also all its public grandparents, etc.).
+In case of multiple inheritance, this search also extends (at compile-time) widely to all public trees of the multiple inheritance forest (multiple public base classes are searched following their order of declaration in the derived class' inheritance list).
+As usual with C++ multiple inheritance, this search could result in multiple overridden functions and therefore in subcontracting from multiple public base classes.
Note that only public base classes are considered for subcontracting because private and protected base classes are not accessible to the user at the calling site where the __substitution_principle__ applies.
A call to the overriding public function with a contract executes the following steps (see [funcref boost::contract::public_function]):
In this documentation __AND__ and __OR__ indicate the logic /and/ and /or/ operations evaluated in /short-circuit/.
For example: `p` __AND__ `q` is true if and only if both `p` and `q` are true, but `q` is never evaluated when `p` is false; `p` __OR__ `q` is true if and only if either `p` or `q` are true, but `q` is never evaluated when `p` is true.
-As indicated by the steps above and in accordance with the __substitution_principle__, subcontracting checks preconditions in __OR__ while class invariants, postconditions, and exceptions guarantees in __AND__ with preconditions, class invariants, postconditions, and exceptions guarantees of base classes.
+As indicated by the steps above and in accordance with the __substitution_principle__, subcontracting checks preconditions in __OR__ while class invariants, postconditions, and exceptions guarantees are checked in __AND__ with preconditions, class invariants, postconditions, and exceptions guarantees of base classes respectively.
]
[heading Non-Overriding Public Functions]
-A call to a non-static public function with a contract (that does not override functions from any of the public base classes) executes the following steps (see [funcref boost::contract::public_function]):
+A call to a non-static public function with a contract (that does not override functions from any of its public base classes) executes the following steps (see [funcref boost::contract::public_function]):
# Check class static __AND__ non-static invariants (but none of the invariants from base classes).
# Check function preconditions (but none of the preconditions from functions in base classes).
A call to a static public function with a contract executes the following steps (see [funcref boost::contract::public_function]):
# Check static class invariants (but not the non-static invariants and none of the invariants from base classes).
-# Check function preconditions (but none of the preconditions from function in base classes).
+# Check function preconditions (but none of the preconditions from functions in base classes).
# Execute the function body.
# Check static class invariants (even if the body threw an exception, but not the non-static invariants and none of the invariants from base classes).
# If the body did not throw an exception, check function postconditions (but none of the postconditions from functions in base classes).
# Check static class invariants (even if the body threw an exception).
# If the body did not throw an exception:
# Check non-static __AND__ volatile class invariants (because the object is now successfully constructed).
- # Check constructor postconditions (but these cannot access the object old value [^['oldof]]`(*this)` because there was no object before the execution of the constructor body).
-# Else, check constructor exception guarantees (but these cannot access the object old value [^['oldof]]`(*this)` because there was no object before the execution of the constructor body, plus they can only access class static members because the object was not successfully constructed upon the constructor body throwing an exception).
+ # Check constructor postconditions (but these cannot access the object old value [^['oldof]]`(*this)` because the object was not constructed before the execution of the constructor body).
+# Else, check constructor exception guarantees (but these cannot access the object old value [^['oldof]]`(*this)` because the object was not constructed before the execution of the constructor body, plus they can only access class' static members because the object has not been successfully constructed given the constructor body threw an exception in this case).
Constructor preconditions are checked before executing the member initialization list so programming these initializations can be simplified assuming the constructor preconditions are satisfied (e.g., constructor arguments can be validated by the constructor preconditions before they are used to initialize base classes and data members).
# Execute the destructor body (destructors have no parameters and they can be called at any time after object construction so they have no preconditions).
# Check static class invariants (even if the body threw an exception).
# If the body did not throw an exception:
- # Check destructor postconditions (but these can only access class static members and the object old value [^['oldof]]`(*this)` because there is no object after successful execution of the destructor body).
+ # Check destructor postconditions (but these can only access class' static members and the object old value [^['oldof]]`(*this)` because the object has been destroyed after successful execution of the destructor body).
[footnote
*Rationale:*
Postconditions for destructors are not part of __N1962__ or other references listed in the __Bibliography__ (but with respect to __Meyer97__ it should be noted that Eiffel does not support static data members and that might by why destructors do not have postconditions in Eiffel).
]
# Destroy any base class (public or not) according with C++ destruction mechanism and also check the contracts of these base destructors (according with steps similar to the ones listed here).
# Else (even if destructors should rarely, if ever, be allowed to throw exceptions in C++):
- # Check non-static class invariants (because the object was not successfully destructed so it still exists and should satisfy its invariants).
+ # Check non-static __AND__ volatile class invariants (because the object was not successfully destructed so it still exists and should satisfy its invariants).
# Check destructor exception guarantees.
As indicated in step 4.b. above, C++ object destruction mechanism will automatically check base class contracts when the destructor exits without throwing an exception (no explicit subcontracting behaviour is required here).
Contracts should not be allowed to modify the program state because they are only responsible to check (and not to change) the program state in order to verify its compliance with the specifications.
Therefore, contracts should only access objects, function arguments, function return values, old values, and all other program variables in `const` context (via `const&`, `const* const`, `const volatile`, etc.).
-Whenever possible (e.g., class invariants and postcondition old values), this library automatically enforces this constant-correctness constraint at compile-time using `const`.
+Whenever possible (e.g., class invariants and postcondition old values), this library automatically enforces this /constant-correctness constraint/ at compile-time using `const`.
However, this library cannot automatically enforce this constraint in all cases (for preconditions and postconditions of mutable member functions, for global variables, etc.).
-See __No_Lambda_Functions__ for ways of using this library that enforces the constant-correctness constraint at compile-time (but at the cost of significant boiler-plate code to be programmed manually so not recommended in general).
+See __No_Lambda_Functions__ for ways of using this library that enforce the constant-correctness constraint at compile-time (but at the cost of significant boiler-plate code to be programmed manually so not recommended in general).
[note
In general, it is the responsibility of the programmers to code assertions that only check, and do not change, program variables.
[section Specifications vs. Implementation]
-Contracts are part of the program specifications and not of its implementation.
+Contracts are part of the program specification and not of its implementation.
Therefore, contracts should ideally be programmed within C++ declarations, and not within definitions.
In general, this library cannot satisfy this requirement.
However, even when contracts are programmed together with the body in the function definition, it is still fairly easy for users to identify and read just the contract portion of the function definition (because the contract code must always be programmed at the very top of the function definition).
-See __Separate_Body_Implementation__ for ways of using this library to program contract specifications outside of the body implementation (but at the cost of writing one extra function for any given function, for applications where this requirement is truly important).
+See __Separate_Body_Implementation__ for ways of using this library to program contract specifications outside of the body implementation (but at the cost of writing one extra function for any given function so not recommended in general).
Furthermore, contracts are most useful when they assert conditions only using public members (in most cases, the need for using non-public members to check contracts, especially in preconditions, indicates an error in the class design).
For example, the caller of a public function cannot in general make sure that the function preconditions are satisfied if the precondition assertions use private members that are not callable by the caller (therefore, a failure in the preconditions will not necessarily indicate a bug in the caller given that the caller was made unable to fully check the preconditions in the first place).
-However, given that C++ provides programmers ways around access level restrictions (`friend`, function pointers, etc.), this library leaves it up to the programmers to make sure that only public members are used in contract assertions (especially in preconditions). (__N1962__ follows the same approach not restricting contracts to only use public members, Eiffel instead generates a compile-time error if preconditions are asserted using non-public members.)
+However, given that C++ provides programmers ways around access level restrictions (`friend`, function pointers, etc.), this library leaves it up to programmers to make sure that only public members are used in contract assertions (especially in preconditions). (__N1962__ follows the same approach not restricting contracts to only use public members, Eiffel instead generates a compile-time error if preconditions are asserted using non-public members.)
[footnote
*Rationale:*
-If C++ [@http://www.open-std.org/jtc1/sc22/wg21/docs/cwg_defects.html#45 defect 45] had not been fixed, this library could have been implemented to generate a compile-time error when precondition assertions use non-public members more similarly to Eiffel's implementation (but not necessary the best approach for C++).
+Out of curiosity, if C++ [@http://www.open-std.org/jtc1/sc22/wg21/docs/cwg_defects.html#45 defect 45] had not been fixed, this library could have been implemented to generate a compile-time error when precondition assertions use non-public members more similarly to Eiffel's implementation (but still, not necessary the best approach for C++).
]
[endsect]
[section On Contract Failures]
If preconditions, postconditions, exception guarantees, or class invariants are either checked to be false or their evaluation throws an exception at run-time then this library will call specific /failure handler functions/.
+[footnote
+*Rationale:*
+If the evaluation of a contract assertion throws an exception, the assertion cannot be checked to be true so the only safe thing to assume is that the assertion failed (indeed the contract assertion checking failed) and call the contract failure handler in this case also.
+]
By default, these failure handler functions print a message to the standard error `std::cerr` (with detailed information about the failure) and then terminate the program calling `std::terminate`.
However, using [funcref boost::contract::set_precondition_failure], [funcref boost::contract::set_postcondition_failure], [funcref boost::contract::set_except_failure], [funcref boost::contract::set_invariant_failure], etc. programmers can define their own failure handler functions that can take any user-specified action (throw an exception, exit the program with an error code, etc., see __Throw_on_Failures__).
[note
In C++ there are a number of issues with programming contract failure handlers that throw exceptions instead of terminating the program.
Specifically, destructors check class invariants so they will throw if programmers change class invariant failure handlers to throw instead of terminating the program, but in general destructors should not throw in C++ (to comply with STL exception safety, C++11 implicit `noexcept` declarations for destructors, etc.).
-Furthermore, programming a failure handler that throws for exception guarantees will throw an exception (the one reporting the contract failure) while there is already an active exception (the one that caused the exception guarantees to be checked in the first place), and this will force C++ to terminate the program anyway.
+Furthermore, programming a failure handler that throws on exception guarantee failures results in throwing an exception (the one reporting the contract failure) while there is already an active exception (the one that caused the exception guarantees to be checked in the first place), and this will force C++ to terminate the program anyway.
]
Therefore, it is recommended to terminate the program at least for contract failures from destructors and exception guarantees (if not in all other cases of contract failures as it is done by default by this library).
[section Feature Summary]
The contract programming features supported by this library are largely based on __N1962__ and on the Eiffel programming language.
-The following table compares contract programming features among this library, __N1962__ (unfortunately the C++ standard committee rejected this proposal commenting on a lack of interest in adding contract programming to C++ at that time, even if __N1962__ itself is sound), a more recent proposal __P0380__ (which has gain some traction within the C++ standard committee but unfortunately only supports preconditions and postconditions, while does not support class invariants, old values, and subcontracting), the Eiffel and D programming languages:
+
+The following table compares contract programming features among this library, __N1962__ (unfortunately the C++ standard committee rejected this proposal commenting on a lack of interest in adding contract programming to C++ at that time, even if __N1962__ itself is sound), a more recent proposal __P0380__ (which was accepted in the C++20 standard but unfortunately only supports preconditions and postconditions, while does not support class invariants, old values, and subcontracting), the Eiffel and D programming languages.
+Some of the items listed in this summary table will become clear in detail after reading the remaining sections of this documentation.
[table
[
[Feature]
[This Library]
[__N1962__ Proposal (not accepted in C++)]
- [__P0380__ Proposal (being considered for C++2x)]
+ [C++20 (see __P0380__)]
[ISE Eiffel 5.4 (see __Meyer97__)]
[D (see __Bright04__)]
][
][
[['Old values in postconditions]]
[
-Yes, [macroref BOOST_CONTRACT_OLDOF] macro and [classref boost::contract::old_ptr] (but copied before preconditions unless `.old(...)` is used as shown in __Old_Value_Copies_at_Body__).
-For templates, [classref boost::contract::old_ptr_if_copyable] skips old value copies for non-copyable types and [funcref boost::contract::condition_if] skips old value copies selectively based on old expression type requirements.
+Yes, [macroref BOOST_CONTRACT_OLDOF] macro and [classref boost::contract::old_ptr] (but copied before preconditions unless `.old(...)` is used as shown in __Old_Values_Copied_at_Body__).
+For templates, [classref boost::contract::old_ptr_if_copyable] skips old value copies for non-copyable types and [funcref boost::contract::condition_if] skips old value copies selectively based on old expression type requirements (on compilers that do not support `if constexpr`).
]
[
Yes, `oldof` keyword (copied right after preconditions).
][
[['Subcontracting]]
[
-Yes, also supports subcontracting for multiple inheritance ([macroref BOOST_CONTRACT_BASE_TYPES], [macroref BOOST_CONTRACT_OVERRIDE], and [classref boost::contract::virtual_] are used for declaring base classes, overrides and virtual public functions respectively).
+Yes, also supports subcontracting for multiple inheritance ([macroref BOOST_CONTRACT_BASE_TYPES], [macroref BOOST_CONTRACT_OVERRIDE], and [classref boost::contract::virtual_] are used to declare base classes, overrides and virtual public functions respectively).
]
[
Yes, also supports subcontracting for multiple inheritance, but preconditions cannot be subcontracted.
*Rationale:*
The authors of __N1962__ decided to forbid derived classes from subcontracting preconditions because they found that such a feature was rarely, if ever, used (see [@http://lists.boost.org/Archives/boost/2010/04/164862.php Re: \[boost\] \[contract\] diff n1962]).
Still, it should be noted that even in __N1962__ if a derived class overrides two functions with preconditions coming from two different base classes via multiple inheritance, the overriding function contract will check preconditions from its two base class functions in __OR__ (so even in __N1962__ preconditions can indirectly subcontract when multiple inheritance is used).
-The authors of this library found that confusing about __N1962__.
Furthermore, subcontracting preconditions is soundly defined by the __substitution_principle__ so this library allows to subcontract preconditions as Eiffel does (users can always avoid using this feature if they have no need for it).
-(This is essentially the only feature on which this library deliberately differ from __N1962__.)
+(This is essentially the only feature on which this library deliberately differs from __N1962__.)
]
]
[No.]
[['Arbitrary code in contracts]]
[Yes (but users are generally recommended to only program assertions using [macroref BOOST_CONTRACT_ASSERT] and if-guard statements within contracts to avoid introducing bugs and expensive code in contracts, and also to only use public functions to program preconditions).]
[No, assertions only (use of only public functions to program preconditions is recommended but not prescribed).]
- [No, assertions only (in addition only public members can be used in preconditions).]
+ [No, assertions only (in addition contracts of public, protected, and private members can only use other public, public/protected, and public/protected/private members respectively).]
[No, assertions only (in addition only public members can be used in preconditions).]
[Yes.]
][
[['Constant-correctness]]
[No, enforced only for class invariants and old values (making also preconditions and postconditions constant-correct is possible but requires users to program a fare amount of boiler-plate code).]
[Yes.]
- [Yes.]
+ [Yes (side effects in contracts lead to undefined behaviour).]
[Yes.]
[No, enforced only for class invariants.]
][
][
[['Disable assertion checking within assertions checking (to avoid infinite recursion when checking contracts)]]
[
-Yes, but use [macroref BOOST_CONTRACT_PRECONDITIONS_DISABLE_NO_ASSERTION] to disable no assertion while checking preconditions (see [macroref BOOST_CONTRACT_ALL_DISABLE_NO_ASSERTION]).
+Yes, but use [macroref BOOST_CONTRACT_PRECONDITIONS_DISABLE_NO_ASSERTION] to disable no assertion while checking preconditions (see also [macroref BOOST_CONTRACT_ALL_DISABLE_NO_ASSERTION]).
[footnote
*Rationale:*
-Theoretically, it can be shown that an incorrect argument might be passed to the function body when assertion checking is disabled while checking preconditions (see [@http://lists.boost.org/Archives/boost/2010/04/164862.php Re: \[boost\] \[contract\] diff n1962]).
-However, that possibility is limited to contract checking when an incorrect argument will simply fail the contract and call the related contract failure handler as expected anyway.
-In any case, because of that __N1962__ does not disable any assertion while checking preconditions.
-That makes it possible to have infinite recursion while checking preconditions so Eiffel disables assertion checking also while checking preconditions.
-Therefore, this library by default disables assertion checking also while checking preconditions, but it also provides the [macroref BOOST_CONTRACT_PRECONDITIONS_DISABLE_NO_ASSERTION] configuration macro so users can change this behaviour to match __N1962__ if needed.
+Technically, it can be shown that an invalid argument can reach the function body when assertion checking is disabled while checking preconditions (that is why __N1962__ does not disable any assertion while checking preconditions, see [@http://lists.boost.org/Archives/boost/2010/04/164862.php Re: \[boost\] \[contract\] diff n1962]).
+However, this can only happen while checking contracts when an invalid argument passed to the body, which should results in the body either throwing an exception or returning an incorrect result, will in turn fail the contract assertion being checked by the caller of the body and invoke the related contract failure handler as desired in the first place.
+Furthermore, not disabling assertions while checking preconditions (like __N1962__ does) makes it possible to have infinite recursion while checking preconditions.
+Therefore, this library by default disables assertion checking also while checking preconditions (like Eiffel does), but it also provides the [macroref BOOST_CONTRACT_PRECONDITIONS_DISABLE_NO_ASSERTION] configuration macro so users can change this behaviour to match __N1962__ if needed.
]
(In multi-threaded programs this introduces a global lock, see [macroref BOOST_CONTRACT_DISABLE_THREADS].)
]
[footnote
*Rationale:*
Older versions of this library defined a data member in the user class that was automatically used to disable checking of class invariants within nested member function calls (similarly to Eiffel).
-This feature was required by older revisions of __N1962__ but it is no longer required in __N1962__ (because it seems to be motivated purely by optimization reasons while similar performances can be achieved by disabling invariants for release builds).
+This feature was required by older revisions of __N1962__ but it is no longer required by __N1962__ (because it seems to be motivated purely by optimization reasons while similar performances can be achieved by disabling invariants for release builds).
Furthermore, in multi-threaded programs this feature would introduce a lock that synchronizes all member functions calls for a given object.
Therefore, this feature was removed in the current revision of this library.
]
[Disable nothing.]
][
[['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 macros shown in __Disable_Contract_Compilation__).]
+ [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 also possible but requires using macros as shown in __Disable_Contract_Compilation__).]
[Yes (contract code also removed from compiled object code, but details are compiler-implementation specific).]
[Yes (contract code also removed from compiled object code, but details are 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).]
]
]
-The authors of this library consulted the following references that implement contract programming for C++ (but usually for only a limited set of features, or using preprocessing tools other than the C++ preprocessor and external to the language itself) and for other languages (see __Bibliography__ for a complete list of all the references consulted during the design and development of this library):
+The authors of this library consulted the following references that implement contract programming for C++ (but usually for only a limited set of features, or using preprocessing tools other than the C++ preprocessor and external to the language itself) and for other languages (see __Bibliography__ for a complete list of all references consulted during the design and development of this library):
[table
[ [Reference] [Language] [Notes] ]
] ]
]
-To the best knowledge of the authors, this the only library that fully supports all contract programming features for C++ (without using preprocessing tools external to the language itself):
+To the best knowledge of the authors, this the only library that fully supports all contract programming features for C++ (without using preprocessing tools external to the language itself).
+In general:
* 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.
+* 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
-For example, the following pseudocode attempts to emulate old values using __P0380__ (`scope_exit` here is an RAII object that executes the nullary functor passed to its constructor when it is destroyed):
+For example, the following pseudocode attempts to emulate old values in __P0380__:
``
+ struct scope_exit { // RAII.
+ template<typename F>
+ explicit scope_exit(F f) : f_(f) {}
+ ~scope_exit() { f_(); }
+
+ scope_exit(scope_exit const&) = delete;
+ scope_exit& operator=(scope_exit const&) = delete;
+ private:
+ std::function<void ()> f_;
+ };
+
void fswap(file& x, file& y)
[[expects: x.closed()]]
- [[excepts: y.closed()]]
- // Postconditions in function definition below to emulate old values.
+ [[expects: y.closed()]]
+ // Cannot use [[ensures]] for postconditions so 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.
+ if(std::uncaught_exceptions() == 0) { // Check only if no throw.
[[assert: x.closed()]]
[[assert: y.closed()]]
[[assert: x == old_y]]
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(); });
+ file z = file::temp();
+ z.open;
+ scope_exit close_z([&] { z.close(); });
- x.mv(t);
+ x.mv(z);
y.mv(x);
- t.mv(y);
+ z.mv(y);
}
``
This requires boiler-plate code to make sure postconditions are correctly checked only if the function did not throw an exception and in a `scope_exit` RAII object after all other local objects have been destroyed (because some of these destructors contribute to establishing the postconditions).
-Still, it never disables old value copies (not even if postconditions are disabled in release builds).
+Still, it never disables old value copies (not even if postconditions are disabled in release builds, this would require adding even more boiler-plate code using `#ifdef`, etc.).
]
* 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 pseudocode attempts to emulation of class invariants using __P0380__:
+For example, the following pseudocode attempts to emulation of class invariants in __P0380__:
``
template<typename T>
class vector {
In case the destructor can throw (e.g., it is declared `noexcept(false)`), the destructor also requires a `try-catch` statement similar to the one programmed for `push_back` to check class invariants at destructor exit when it throws exceptions.
Still, an outstanding issue remains to avoid infinite recursion if also `empty` and `size` are public functions programmed to check class invariants (because __P0380__ does not automatically disable assertions while checking other assertions).
]
-All references reviewed by the authors seem to not consider static and volatile functions not supporting static and volatile invariants respectively.
+In addition, all references reviewed by the authors seem to not consider static and volatile 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
projects / platform / upstream / boost.git / blobdiff