2146 lines
130 KiB
HTML
2146 lines
130 KiB
HTML
<html>
|
||
<head>
|
||
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
|
||
<title>Contract Programming Overview</title>
|
||
<link rel="stylesheet" href="../../../../../doc/src/boostbook.css" type="text/css">
|
||
<meta name="generator" content="DocBook XSL Stylesheets V1.79.1">
|
||
<link rel="home" href="../index.html" title="Chapter 1. Boost.Contract 1.0.0">
|
||
<link rel="up" href="../index.html" title="Chapter 1. Boost.Contract 1.0.0">
|
||
<link rel="prev" href="getting_started.html" title="Getting Started">
|
||
<link rel="next" href="tutorial.html" title="Tutorial">
|
||
</head>
|
||
<body bgcolor="white" text="black" link="#0000FF" vlink="#840084" alink="#0000FF">
|
||
<table cellpadding="2" width="100%"><tr>
|
||
<td valign="top"><img alt="Boost C++ Libraries" width="277" height="86" src="../../../../../boost.png"></td>
|
||
<td align="center"><a href="../../../../../index.html">Home</a></td>
|
||
<td align="center"><a href="../../../../../libs/libraries.htm">Libraries</a></td>
|
||
<td align="center"><a href="http://www.boost.org/users/people.html">People</a></td>
|
||
<td align="center"><a href="http://www.boost.org/users/faq.html">FAQ</a></td>
|
||
<td align="center"><a href="../../../../../more/index.htm">More</a></td>
|
||
</tr></table>
|
||
<hr>
|
||
<div class="spirit-nav">
|
||
<a accesskey="p" href="getting_started.html"><img src="../../../../../doc/src/images/prev.png" alt="Prev"></a><a accesskey="u" href="../index.html"><img src="../../../../../doc/src/images/up.png" alt="Up"></a><a accesskey="h" href="../index.html"><img src="../../../../../doc/src/images/home.png" alt="Home"></a><a accesskey="n" href="tutorial.html"><img src="../../../../../doc/src/images/next.png" alt="Next"></a>
|
||
</div>
|
||
<div class="section">
|
||
<div class="titlepage"><div><div><h2 class="title" style="clear: both">
|
||
<a name="boost_contract.contract_programming_overview"></a><a class="link" href="contract_programming_overview.html" title="Contract Programming Overview">Contract
|
||
Programming Overview</a>
|
||
</h2></div></div></div>
|
||
<div class="toc"><dl class="toc">
|
||
<dt><span class="section"><a href="contract_programming_overview.html#boost_contract.contract_programming_overview.assertions">Assertions</a></span></dt>
|
||
<dt><span class="section"><a href="contract_programming_overview.html#boost_contract.contract_programming_overview.benefits_and_costs">Benefits
|
||
and Costs</a></span></dt>
|
||
<dt><span class="section"><a href="contract_programming_overview.html#boost_contract.contract_programming_overview.function_calls">Function
|
||
Calls</a></span></dt>
|
||
<dt><span class="section"><a href="contract_programming_overview.html#boost_contract.contract_programming_overview.public_function_calls">Public
|
||
Function Calls</a></span></dt>
|
||
<dt><span class="section"><a href="contract_programming_overview.html#boost_contract.contract_programming_overview.constructor_calls">Constructor
|
||
Calls</a></span></dt>
|
||
<dt><span class="section"><a href="contract_programming_overview.html#boost_contract.contract_programming_overview.destructor_calls">Destructor
|
||
Calls</a></span></dt>
|
||
<dt><span class="section"><a href="contract_programming_overview.html#boost_contract.contract_programming_overview.constant_correctness">Constant-Correctness</a></span></dt>
|
||
<dt><span class="section"><a href="contract_programming_overview.html#boost_contract.contract_programming_overview.specifications_vs__implementation">Specifications
|
||
vs. Implementation</a></span></dt>
|
||
<dt><span class="section"><a href="contract_programming_overview.html#boost_contract.contract_programming_overview.on_contract_failures">On
|
||
Contract Failures</a></span></dt>
|
||
<dt><span class="section"><a href="contract_programming_overview.html#boost_contract.contract_programming_overview.feature_summary">Feature
|
||
Summary</a></span></dt>
|
||
</dl></div>
|
||
<div class="blockquote"><blockquote class="blockquote"><p>
|
||
<span class="emphasis"><em><span class="quote">“<span class="quote">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?</span>”</span></em></span>
|
||
</p></blockquote></div>
|
||
<div class="blockquote"><blockquote class="blockquote"><p>
|
||
<span class="emphasis"><em>-- Charles Antony Richard Hoare (see <a class="link" href="bibliography.html#Hoare73_anchor">[Hoare73]</a>)</em></span>
|
||
</p></blockquote></div>
|
||
<p>
|
||
This section gives an overview of contract programming (see <a class="link" href="bibliography.html#Meyer97_anchor">[Meyer97]</a>,
|
||
<a class="link" href="bibliography.html#Mitchell02_anchor">[Mitchell02]</a>, and <a class="link" href="bibliography.html#N1613_anchor">[N1613]</a>
|
||
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 <a class="link" href="tutorial.html" title="Tutorial">Tutorial</a>.
|
||
</p>
|
||
<div class="note"><table border="0" summary="Note">
|
||
<tr>
|
||
<td rowspan="2" align="center" valign="top" width="25"><img alt="[Note]" src="../../../../../doc/src/images/note.png"></td>
|
||
<th align="left">Note</th>
|
||
</tr>
|
||
<tr><td align="left" valign="top"><p>
|
||
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 programs
|
||
and tools external to the C++ language and its preprocessor).
|
||
</p></td></tr>
|
||
</table></div>
|
||
<div class="section">
|
||
<div class="titlepage"><div><div><h3 class="title">
|
||
<a name="boost_contract.contract_programming_overview.assertions"></a><a class="link" href="contract_programming_overview.html#boost_contract.contract_programming_overview.assertions" title="Assertions">Assertions</a>
|
||
</h3></div></div></div>
|
||
<p>
|
||
Contract programming is characterized by the following assertion mechanisms:
|
||
</p>
|
||
<div class="itemizedlist"><ul class="itemizedlist" style="list-style-type: disc; ">
|
||
<li class="listitem">
|
||
<span class="emphasis"><em>Preconditions</em></span>: 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 also referred to as having a <span class="emphasis"><em>wide contract</em></span>.
|
||
This is in contrast to operations that have preconditions which are also
|
||
referred to as having a <span class="emphasis"><em>narrow contract</em></span> (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).
|
||
<a href="#ftn.boost_contract.contract_programming_overview.assertions.f0" class="footnote" name="boost_contract.contract_programming_overview.assertions.f0"><sup class="footnote">[6]</sup></a>
|
||
</li>
|
||
<li class="listitem">
|
||
<span class="emphasis"><em>Postconditions</em></span>: 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 <span class="emphasis"><em>old values</em></span> (which are
|
||
the values that expressions had before the function implementation was
|
||
executed).
|
||
</li>
|
||
<li class="listitem">
|
||
<span class="emphasis"><em>Exception guarantees</em></span>: 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). <a href="#ftn.boost_contract.contract_programming_overview.assertions.f1" class="footnote" name="boost_contract.contract_programming_overview.assertions.f1"><sup class="footnote">[7]</sup></a>
|
||
</li>
|
||
<li class="listitem">
|
||
<span class="emphasis"><em>Class invariants</em></span>: 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 <span class="emphasis"><em>volatile class
|
||
invariants</em></span>. It is also possible to specify <span class="emphasis"><em>static
|
||
class invariants</em></span> 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). <a href="#ftn.boost_contract.contract_programming_overview.assertions.f2" class="footnote" name="boost_contract.contract_programming_overview.assertions.f2"><sup class="footnote">[8]</sup></a>
|
||
</li>
|
||
<li class="listitem">
|
||
<span class="emphasis"><em>Subcontracting</em></span>: 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 <a href="http://en.wikipedia.org/wiki/Liskov_substitution_principle" target="_top">substitution
|
||
principle</a>).
|
||
</li>
|
||
</ul></div>
|
||
<p>
|
||
The actual function implementation code, that remains outside of these contract
|
||
assertions, is often referred to as the <span class="emphasis"><em>function body</em></span>
|
||
in contract programming.
|
||
</p>
|
||
<p>
|
||
Class invariants can also be used to specify <span class="emphasis"><em>basic</em></span> 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 <span class="emphasis"><em>strong</em></span> exception safety
|
||
guarantees for a given operation on the same object.
|
||
</p>
|
||
<p>
|
||
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).
|
||
</p>
|
||
<div class="note"><table border="0" summary="Note">
|
||
<tr>
|
||
<td rowspan="2" align="center" valign="top" width="25"><img alt="[Note]" src="../../../../../doc/src/images/note.png"></td>
|
||
<th align="left">Note</th>
|
||
</tr>
|
||
<tr><td align="left" valign="top"><p>
|
||
This library implements this requirement but in order to globally disable
|
||
assertions while checking another assertion some kind of global arbitrating
|
||
variable needs to be used by this library implementation. This library
|
||
will automatically protect such a global variable from race conditions
|
||
in multi-threated programs, but this will effectively introduce a global
|
||
lock in the program (the <code class="computeroutput"><a class="link" href="../BOOST_CO_idm45028039741520.html" title="Macro BOOST_CONTRACT_DISABLE_THREADS">BOOST_CONTRACT_DISABLE_THREADS</a></code>
|
||
macro can be defined to disable this global lock but at the risk of incurring
|
||
in race conditions). <a href="#ftn.boost_contract.contract_programming_overview.assertions.f3" class="footnote" name="boost_contract.contract_programming_overview.assertions.f3"><sup class="footnote">[9]</sup></a>
|
||
</p></td></tr>
|
||
</table></div>
|
||
<p>
|
||
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 (<code class="computeroutput"><span class="special">&&</span></code>,
|
||
<code class="computeroutput"><span class="special">||</span></code>, etc.). This is because when
|
||
contract conditions are programmed together in a single assertion using logical
|
||
operators, it might not be clear which condition actually failed in case
|
||
the entire assertion fails at run-time.
|
||
</p>
|
||
<h5>
|
||
<a name="boost_contract.contract_programming_overview.assertions.h0"></a>
|
||
<span class="phrase"><a name="boost_contract.contract_programming_overview.assertions.c_style_assertions"></a></span><a class="link" href="contract_programming_overview.html#boost_contract.contract_programming_overview.assertions.c_style_assertions">C-Style
|
||
Assertions</a>
|
||
</h5>
|
||
<p>
|
||
A limited form of contract programming (typically some form of precondition
|
||
and basic postcondition checking) can be achieved using the C-style <code class="computeroutput"><span class="identifier">assert</span></code> macro. Using <code class="computeroutput"><span class="identifier">assert</span></code>
|
||
is common practice for many programmers but it suffers of the following limitations:
|
||
</p>
|
||
<div class="itemizedlist"><ul class="itemizedlist" style="list-style-type: disc; ">
|
||
<li class="listitem">
|
||
<code class="computeroutput"><span class="identifier">assert</span></code> 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 keeping the
|
||
library preconditions enabled given that future changes in the user code
|
||
that calls the library cannot be anticipated). Using <code class="computeroutput"><span class="identifier">assert</span></code>
|
||
it is not possible to selectively disable only postconditions and all
|
||
assertions must be disabled at once.
|
||
</li>
|
||
<li class="listitem">
|
||
<code class="computeroutput"><span class="identifier">assert</span></code> 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).
|
||
</li>
|
||
<li class="listitem">
|
||
<code class="computeroutput"><span class="identifier">assert</span></code> requires to manually
|
||
program extra code to check class invariants (extra member functions,
|
||
try blocks, etc.).
|
||
</li>
|
||
<li class="listitem">
|
||
<code class="computeroutput"><span class="identifier">assert</span></code> does not support
|
||
subcontracting.
|
||
</li>
|
||
<li class="listitem">
|
||
<code class="computeroutput"><span class="identifier">assert</span></code> 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).
|
||
</li>
|
||
</ul></div>
|
||
<p>
|
||
Contract programming does not suffer of these limitations.
|
||
</p>
|
||
</div>
|
||
<div class="section">
|
||
<div class="titlepage"><div><div><h3 class="title">
|
||
<a name="boost_contract.contract_programming_overview.benefits_and_costs"></a><a class="link" href="contract_programming_overview.html#boost_contract.contract_programming_overview.benefits_and_costs" title="Benefits and Costs">Benefits
|
||
and Costs</a>
|
||
</h3></div></div></div>
|
||
<h5>
|
||
<a name="boost_contract.contract_programming_overview.benefits_and_costs.h0"></a>
|
||
<span class="phrase"><a name="boost_contract.contract_programming_overview.benefits_and_costs.benefits"></a></span><a class="link" href="contract_programming_overview.html#boost_contract.contract_programming_overview.benefits_and_costs.benefits">Benefits</a>
|
||
</h5>
|
||
<p>
|
||
The main use of contract programming is to improve software quality. <a class="link" href="bibliography.html#Meyer97_anchor">[Meyer97]</a> discusses how contract programming
|
||
can be used as the basic tool to write <span class="quote">“<span class="quote">correct</span>”</span> software.
|
||
<a class="link" href="bibliography.html#Stroustrup94_anchor">[Stroustrup94]</a> discusses the key
|
||
importance of class invariants plus advantages and disadvantages of preconditions
|
||
and postconditions.
|
||
</p>
|
||
<p>
|
||
The following is a short summary of benefits associated with contract programming
|
||
inspired mainly by <a class="link" href="bibliography.html#N1613_anchor">[N1613]</a>:
|
||
</p>
|
||
<div class="itemizedlist"><ul class="itemizedlist" style="list-style-type: disc; ">
|
||
<li class="listitem">
|
||
Preconditions and postconditions: Using function preconditions and postconditions,
|
||
programmers can give a precise semantic description of what a function
|
||
requires at its entry and what it ensures at its exit (if it does not
|
||
throw an exception). In particular, using postcondition old values, contract
|
||
programming provides a mechanism that allows programmers to compare values
|
||
of an expression before and after the function body execution. This mechanism
|
||
is powerful enough to enable programmers to express many correctness
|
||
constraints within the code itself, constraints that would otherwise
|
||
have to be captured at best only informally by documentation.
|
||
</li>
|
||
<li class="listitem">
|
||
Class invariants: Using class invariants, programmers can describe what
|
||
to expect from a class and the logic dependencies between the class members.
|
||
It is the job of the constructor to ensure that the class invariants
|
||
are satisfied when the object is first created. Then the implementation
|
||
of the member functions can be largely simplified as they can be written
|
||
knowing that the class invariants are satisfied because contract programming
|
||
checks them before and after the execution of every public function.
|
||
Finally, the destructor makes sure that the class invariants held for
|
||
the entire life of the object checking the class invariants one last
|
||
time before the object is destructed. Class invariants can also be used
|
||
as a criteria for good abstractions: 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 into a class (maybe a namespace
|
||
would have sufficed instead).
|
||
</li>
|
||
<li class="listitem">
|
||
Self-documenting code: 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.
|
||
</li>
|
||
<li class="listitem">
|
||
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. 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. <a href="#ftn.boost_contract.contract_programming_overview.benefits_and_costs.f0" class="footnote" name="boost_contract.contract_programming_overview.benefits_and_costs.f0"><sup class="footnote">[10]</sup></a>
|
||
</li>
|
||
<li class="listitem">
|
||
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 and guide, but obviously
|
||
not to replace, testing).
|
||
</li>
|
||
<li class="listitem">
|
||
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 contract assertions. Moreover, contracts can make
|
||
code reviews easier by clarifying some of the semantics and usage of
|
||
the code.
|
||
</li>
|
||
<li class="listitem">
|
||
Formalize inheritance: Contract programming formalizes the virtual function
|
||
overriding mechanism using subcontracting as justified by the <a href="http://en.wikipedia.org/wiki/Liskov_substitution_principle" target="_top">substitution
|
||
principle</a>. This keeps the base class programmers in control as
|
||
overriding functions always have to fully satisfy the contracts of their
|
||
base classes.
|
||
</li>
|
||
<li class="listitem">
|
||
Replace defensive programming: Contract programming assertions can replace
|
||
<a href="http://en.wikipedia.org/wiki/Defensive_programming" target="_top">defensive
|
||
programming</a> checks localizing these checks within the contracts
|
||
and making the code more readable.
|
||
</li>
|
||
</ul></div>
|
||
<p>
|
||
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 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 <a class="link" href="examples.html#N1962_vector_anchor"><code class="computeroutput"><span class="identifier">vector</span></code></a> contract assertions can actually
|
||
be programmed in C++ using this library).
|
||
</p>
|
||
<h5>
|
||
<a name="boost_contract.contract_programming_overview.benefits_and_costs.h1"></a>
|
||
<span class="phrase"><a name="boost_contract.contract_programming_overview.benefits_and_costs.costs"></a></span><a class="link" href="contract_programming_overview.html#boost_contract.contract_programming_overview.benefits_and_costs.costs">Costs</a>
|
||
</h5>
|
||
<p>
|
||
In general, contract programming benefits come at the cost of performance
|
||
as discussed in detail by both <a class="link" href="bibliography.html#Stroustrup94_anchor">[Stroustrup94]</a>
|
||
and <a class="link" href="bibliography.html#Meyer97_anchor">[Meyer97]</a>. While performance trade-offs
|
||
should be carefully considered depending on the specific application domain,
|
||
software quality cannot be sacrificed: It is difficult to see value in software
|
||
that quickly and efficiently provides incorrect results.
|
||
</p>
|
||
<p>
|
||
The run-time performances are negatively impacted by contract programming
|
||
mainly because of extra time require to:
|
||
</p>
|
||
<div class="itemizedlist"><ul class="itemizedlist" style="list-style-type: disc; ">
|
||
<li class="listitem">
|
||
Check the asserted conditions.
|
||
</li>
|
||
<li class="listitem">
|
||
Copy old values when these are used in postconditions or exception guarantees.
|
||
</li>
|
||
<li class="listitem">
|
||
Call additional functors that check preconditions, postconditions, exception
|
||
guarantees, class invariants, etc. (these can add up to many extra calls
|
||
especially when using subcontracting).
|
||
</li>
|
||
</ul></div>
|
||
<div class="note"><table border="0" summary="Note">
|
||
<tr>
|
||
<td rowspan="2" align="center" valign="top" width="25"><img alt="[Note]" src="../../../../../doc/src/images/note.png"></td>
|
||
<th align="left">Note</th>
|
||
</tr>
|
||
<tr><td align="left" valign="top"><p>
|
||
In general, contracts introduce at least three extra functor calls to check
|
||
preconditions, postconditions, and exception guarantees for any given non-member
|
||
function call. Public functions introduce also two more function calls
|
||
to check class invariants (at entry and at exit). For subcontracting, these
|
||
extra calls (some of which become virtual calls) are repeated for the number
|
||
of functions being overridden from the base classes (possibly deep in the
|
||
inheritance tree). In addition to that, this library introduces a number
|
||
of function calls internal to its implementation in order to properly check
|
||
the contracts.
|
||
</p></td></tr>
|
||
</table></div>
|
||
<p>
|
||
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
|
||
specific applications, but a reasonable approach often is to (see <a class="link" href="extras.html#boost_contract.extras.disable_contract_checking" title="Disable Contract Checking">Disable
|
||
Contract Checking</a>):
|
||
</p>
|
||
<div class="itemizedlist"><ul class="itemizedlist" style="list-style-type: disc; ">
|
||
<li class="listitem">
|
||
Always write contracts to clarify the semantics of the design embedding
|
||
the specifications directly in the code and making the code self-documenting.
|
||
</li>
|
||
<li class="listitem">
|
||
Check preconditions, postconditions, class invariants, and maybe even
|
||
exception guarantees during initial testing.
|
||
</li>
|
||
<li class="listitem">
|
||
Check only preconditions (and maybe class invariants, but not postconditions
|
||
and exception guarantees) during release testing and for the final release.
|
||
</li>
|
||
</ul></div>
|
||
<p>
|
||
This approach is usually reasonable because in well-tested production code,
|
||
validating the function body implementation using postconditions is rarely
|
||
needed since the function has shown itself to be <span class="quote">“<span class="quote">correct</span>”</span> during
|
||
testing. On the other hand, checking function arguments using preconditions
|
||
is always needed because of changes that can be made to the calling code
|
||
(without having to necessarily re-test and re-release the called code). Furthermore,
|
||
postconditions and also exception guarantees, with related old value copies,
|
||
are often computationally more expensive to check than preconditions and
|
||
class invariants.
|
||
</p>
|
||
</div>
|
||
<div class="section">
|
||
<div class="titlepage"><div><div><h3 class="title">
|
||
<a name="boost_contract.contract_programming_overview.function_calls"></a><a class="link" href="contract_programming_overview.html#boost_contract.contract_programming_overview.function_calls" title="Function Calls">Function
|
||
Calls</a>
|
||
</h3></div></div></div>
|
||
<h5>
|
||
<a name="boost_contract.contract_programming_overview.function_calls.h0"></a>
|
||
<span class="phrase"><a name="boost_contract.contract_programming_overview.function_calls.non_member_functions"></a></span><a class="link" href="contract_programming_overview.html#boost_contract.contract_programming_overview.function_calls.non_member_functions">Non-Member
|
||
Functions</a>
|
||
</h5>
|
||
<p>
|
||
A call to a non-member function with a contract executes the following steps
|
||
(see <code class="computeroutput"><a class="link" href="../boost/contract/function.html" title="Function function">boost::contract::function</a></code>):
|
||
</p>
|
||
<div class="orderedlist"><ol class="orderedlist" type="1">
|
||
<li class="listitem">
|
||
Check function preconditions.
|
||
</li>
|
||
<li class="listitem">
|
||
Execute the function body.
|
||
</li>
|
||
<li class="listitem">
|
||
If the body did not throw an exception, check function postconditions.
|
||
</li>
|
||
<li class="listitem">
|
||
Else, check function exception guarantees.
|
||
</li>
|
||
</ol></div>
|
||
<h5>
|
||
<a name="boost_contract.contract_programming_overview.function_calls.h1"></a>
|
||
<span class="phrase"><a name="boost_contract.contract_programming_overview.function_calls.private_and_protected_functions"></a></span><a class="link" href="contract_programming_overview.html#boost_contract.contract_programming_overview.function_calls.private_and_protected_functions">Private
|
||
and Protected Functions</a>
|
||
</h5>
|
||
<p>
|
||
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 <a href="http://en.wikipedia.org/wiki/Liskov_substitution_principle" target="_top">substitution
|
||
principle</a> does not apply to private and protected functions because
|
||
these functions are not accessible to the user at the calling site where
|
||
the <a href="http://en.wikipedia.org/wiki/Liskov_substitution_principle" target="_top">substitution
|
||
principle</a> applies.
|
||
</p>
|
||
<p>
|
||
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).
|
||
</p>
|
||
</div>
|
||
<div class="section">
|
||
<div class="titlepage"><div><div><h3 class="title">
|
||
<a name="boost_contract.contract_programming_overview.public_function_calls"></a><a class="link" href="contract_programming_overview.html#boost_contract.contract_programming_overview.public_function_calls" title="Public Function Calls">Public
|
||
Function Calls</a>
|
||
</h3></div></div></div>
|
||
<h5>
|
||
<a name="boost_contract.contract_programming_overview.public_function_calls.h0"></a>
|
||
<span class="phrase"><a name="boost_contract.contract_programming_overview.public_function_calls.overriding_public_functions"></a></span><a class="link" href="contract_programming_overview.html#boost_contract.contract_programming_overview.public_function_calls.overriding_public_functions">Overriding
|
||
Public Functions</a>
|
||
</h5>
|
||
<p>
|
||
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 <span class="emphasis"><em>overriding
|
||
function</em></span>, and to the set of base classes containing all the <span class="emphasis"><em>overridden
|
||
functions</em></span> as <span class="emphasis"><em>overridden bases</em></span>.
|
||
</p>
|
||
<p>
|
||
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 <a href="http://en.wikipedia.org/wiki/Liskov_substitution_principle" target="_top">substitution
|
||
principle</a> applies.
|
||
</p>
|
||
<p>
|
||
A call to the overriding public function with a contract executes the following
|
||
steps (see <code class="computeroutput"><a class="link" href="../boost/contract/public_f_idm45028038882752.html" title="Function template public_function">boost::contract::public_function</a></code>):
|
||
</p>
|
||
<div class="orderedlist"><ol class="orderedlist" type="1">
|
||
<li class="listitem">
|
||
Check static class invariants <a class="link" href="contract_programming_overview.html#and_anchor"><code class="literal"><span class="emphasis"><em>AND</em></span></code></a>
|
||
non-static class invariants for all overridden bases, <a class="link" href="contract_programming_overview.html#and_anchor"><code class="literal"><span class="emphasis"><em>AND</em></span></code></a>
|
||
then check the derived class static <a class="link" href="contract_programming_overview.html#and_anchor"><code class="literal"><span class="emphasis"><em>AND</em></span></code></a>
|
||
non-static invariants.
|
||
</li>
|
||
<li class="listitem">
|
||
Check preconditions of overridden public functions from all overridden
|
||
bases in <a class="link" href="contract_programming_overview.html#or_anchor"><code class="literal"><span class="emphasis"><em>OR</em></span></code></a>
|
||
with each other, <a class="link" href="contract_programming_overview.html#or_anchor"><code class="literal"><span class="emphasis"><em>OR</em></span></code></a>
|
||
else check the overriding function preconditions in the derived class.
|
||
</li>
|
||
<li class="listitem">
|
||
Execute the overriding function body.
|
||
</li>
|
||
<li class="listitem">
|
||
Check static class invariants <a class="link" href="contract_programming_overview.html#and_anchor"><code class="literal"><span class="emphasis"><em>AND</em></span></code></a>
|
||
non-static class invariants for all overridden bases, <a class="link" href="contract_programming_overview.html#and_anchor"><code class="literal"><span class="emphasis"><em>AND</em></span></code></a>
|
||
then check the derived class static <a class="link" href="contract_programming_overview.html#and_anchor"><code class="literal"><span class="emphasis"><em>AND</em></span></code></a>
|
||
non-static invariants (even if the body threw an exception).
|
||
</li>
|
||
<li class="listitem">
|
||
If the body did not throw an exception, check postconditions of overridden
|
||
public functions from all overridden bases in <a class="link" href="contract_programming_overview.html#and_anchor"><code class="literal"><span class="emphasis"><em>AND</em></span></code></a>
|
||
with each other, <a class="link" href="contract_programming_overview.html#and_anchor"><code class="literal"><span class="emphasis"><em>AND</em></span></code></a>
|
||
then check the overriding function postconditions in the derived class.
|
||
</li>
|
||
<li class="listitem">
|
||
Else, check exception guarantees of overridden public functions from
|
||
all overridden bases in <a class="link" href="contract_programming_overview.html#and_anchor"><code class="literal"><span class="emphasis"><em>AND</em></span></code></a>
|
||
with each other, <a class="link" href="contract_programming_overview.html#and_anchor"><code class="literal"><span class="emphasis"><em>AND</em></span></code></a>
|
||
then check the overriding function exception guarantees in the derived
|
||
class.
|
||
</li>
|
||
</ol></div>
|
||
<p>
|
||
Volatile public functions check static class invariants <a class="link" href="contract_programming_overview.html#and_anchor"><code class="literal"><span class="emphasis"><em>AND</em></span></code></a>
|
||
volatile class invariants instead. Preconditions and postconditions of volatile
|
||
public functions and volatile class invariants access the object as <code class="computeroutput"><span class="keyword">volatile</span></code>.
|
||
</p>
|
||
<p>
|
||
Class invariants are checked before preconditions and postconditions so programming
|
||
precondition and postcondition assertions can be simplified assuming that
|
||
class invariants are satisfied already (e.g., if class invariants assert
|
||
that a pointer cannot be null then preconditions and postconditions can safety
|
||
dereference that pointer without additional checking). Similarly, static
|
||
class invariants are checked before non-static class invariants so programming
|
||
non-static class invariant (volatile and non) can be simplified assuming
|
||
that static class invariants are satisfied already. Furthermore, subcontracting
|
||
checks contracts of public base classes before checking the derived class
|
||
contracts so programming derived class contract assertions can be simplified
|
||
by assuming that public base class contracts are satisfied already.
|
||
</p>
|
||
<div class="note"><table border="0" summary="Note">
|
||
<tr>
|
||
<td rowspan="2" align="center" valign="top" width="25"><img alt="[Note]" src="../../../../../doc/src/images/note.png"></td>
|
||
<th align="left">Note</th>
|
||
</tr>
|
||
<tr><td align="left" valign="top">
|
||
<p>
|
||
<a name="and_anchor"></a><a name="or_anchor"></a>In this documentation
|
||
<a class="link" href="contract_programming_overview.html#and_anchor"><code class="literal"><span class="emphasis"><em>AND</em></span></code></a>
|
||
and <a class="link" href="contract_programming_overview.html#or_anchor"><code class="literal"><span class="emphasis"><em>OR</em></span></code></a>
|
||
indicate the logic <span class="emphasis"><em>and</em></span> and <span class="emphasis"><em>or</em></span>
|
||
operations evaluated in <span class="emphasis"><em>short-circuit</em></span>. For example:
|
||
<code class="computeroutput"><span class="identifier">p</span></code> <a class="link" href="contract_programming_overview.html#and_anchor"><code class="literal"><span class="emphasis"><em>AND</em></span></code></a>
|
||
<code class="computeroutput"><span class="identifier">q</span></code> is true if and only if
|
||
both <code class="computeroutput"><span class="identifier">p</span></code> and <code class="computeroutput"><span class="identifier">q</span></code> are true, but <code class="computeroutput"><span class="identifier">q</span></code>
|
||
is never evaluated when <code class="computeroutput"><span class="identifier">p</span></code>
|
||
is false; <code class="computeroutput"><span class="identifier">p</span></code> <a class="link" href="contract_programming_overview.html#or_anchor"><code class="literal"><span class="emphasis"><em>OR</em></span></code></a>
|
||
<code class="computeroutput"><span class="identifier">q</span></code> is true if and only if
|
||
either <code class="computeroutput"><span class="identifier">p</span></code> or <code class="computeroutput"><span class="identifier">q</span></code> are true, but <code class="computeroutput"><span class="identifier">q</span></code>
|
||
is never evaluated when <code class="computeroutput"><span class="identifier">p</span></code>
|
||
is true.
|
||
</p>
|
||
<p>
|
||
As indicated by the steps above and in accordance with the <a href="http://en.wikipedia.org/wiki/Liskov_substitution_principle" target="_top">substitution
|
||
principle</a>, subcontracting checks preconditions in <a class="link" href="contract_programming_overview.html#or_anchor"><code class="literal"><span class="emphasis"><em>OR</em></span></code></a>
|
||
while class invariants, postconditions, and exceptions guarantees are checked
|
||
in <a class="link" href="contract_programming_overview.html#and_anchor"><code class="literal"><span class="emphasis"><em>AND</em></span></code></a>
|
||
with preconditions, class invariants, postconditions, and exceptions guarantees
|
||
of base classes respectively.
|
||
</p>
|
||
</td></tr>
|
||
</table></div>
|
||
<h5>
|
||
<a name="boost_contract.contract_programming_overview.public_function_calls.h1"></a>
|
||
<span class="phrase"><a name="boost_contract.contract_programming_overview.public_function_calls.non_overriding_public_functions"></a></span><a class="link" href="contract_programming_overview.html#boost_contract.contract_programming_overview.public_function_calls.non_overriding_public_functions">Non-Overriding
|
||
Public Functions</a>
|
||
</h5>
|
||
<p>
|
||
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 <code class="computeroutput"><a class="link" href="../boost/contract/public_f_idm45028038882752.html" title="Function template public_function">boost::contract::public_function</a></code>):
|
||
</p>
|
||
<div class="orderedlist"><ol class="orderedlist" type="1">
|
||
<li class="listitem">
|
||
Check class static <a class="link" href="contract_programming_overview.html#and_anchor"><code class="literal"><span class="emphasis"><em>AND</em></span></code></a>
|
||
non-static invariants (but none of the invariants from base classes).
|
||
</li>
|
||
<li class="listitem">
|
||
Check function preconditions (but none of the preconditions from functions
|
||
in base classes).
|
||
</li>
|
||
<li class="listitem">
|
||
Execute the function body.
|
||
</li>
|
||
<li class="listitem">
|
||
Check the class static <a class="link" href="contract_programming_overview.html#and_anchor"><code class="literal"><span class="emphasis"><em>AND</em></span></code></a>
|
||
non-static invariants (even if the body threw an exception, but none
|
||
of the invariants from base classes).
|
||
</li>
|
||
<li class="listitem">
|
||
If the body did not throw an exception, check function postconditions
|
||
(but none of the postconditions from functions in base classes).
|
||
</li>
|
||
<li class="listitem">
|
||
Else, check function exception guarantees (but none of the exception
|
||
guarantees from functions in base classes).
|
||
</li>
|
||
</ol></div>
|
||
<p>
|
||
Volatile public functions check static class invariants <a class="link" href="contract_programming_overview.html#and_anchor"><code class="literal"><span class="emphasis"><em>AND</em></span></code></a>
|
||
volatile class invariants instead. Preconditions and postconditions of volatile
|
||
functions and volatile class invariants access the object as <code class="computeroutput"><span class="keyword">volatile</span></code>.
|
||
</p>
|
||
<p>
|
||
Class invariants are checked because this function is part of the class public
|
||
interface. However, none of the contracts of the base classes are checked
|
||
because this function does not override any functions from any of the public
|
||
base classes (so the <a href="http://en.wikipedia.org/wiki/Liskov_substitution_principle" target="_top">substitution
|
||
principle</a> does not require to subcontract in this case).
|
||
</p>
|
||
<h5>
|
||
<a name="boost_contract.contract_programming_overview.public_function_calls.h2"></a>
|
||
<span class="phrase"><a name="boost_contract.contract_programming_overview.public_function_calls.static_public_functions"></a></span><a class="link" href="contract_programming_overview.html#boost_contract.contract_programming_overview.public_function_calls.static_public_functions">Static
|
||
Public Functions</a>
|
||
</h5>
|
||
<p>
|
||
A call to a static public function with a contract executes the following
|
||
steps (see <code class="computeroutput"><a class="link" href="../boost/contract/public_f_idm45028038882752.html" title="Function template public_function">boost::contract::public_function</a></code>):
|
||
</p>
|
||
<div class="orderedlist"><ol class="orderedlist" type="1">
|
||
<li class="listitem">
|
||
Check static class invariants (but not the non-static invariants and
|
||
none of the invariants from base classes).
|
||
</li>
|
||
<li class="listitem">
|
||
Check function preconditions (but none of the preconditions from functions
|
||
in base classes).
|
||
</li>
|
||
<li class="listitem">
|
||
Execute the function body.
|
||
</li>
|
||
<li class="listitem">
|
||
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).
|
||
</li>
|
||
<li class="listitem">
|
||
If the body did not throw an exception, check function postconditions
|
||
(but none of the postconditions from functions in base classes).
|
||
</li>
|
||
<li class="listitem">
|
||
Else, check function exception guarantees (but none of the exception
|
||
guarantees from functions in base classes).
|
||
</li>
|
||
</ol></div>
|
||
<p>
|
||
Class invariants are checked because this function is part of the class public
|
||
interface, but only static class invariants can be checked (because this
|
||
is a static function so it cannot access the object that would instead be
|
||
required to check non-static class invariants, volatile or not). Furthermore,
|
||
static functions cannot override any function so the <a href="http://en.wikipedia.org/wiki/Liskov_substitution_principle" target="_top">substitution
|
||
principle</a> does not apply and they do not subcontract.
|
||
</p>
|
||
<p>
|
||
Preconditions and postconditions of static functions and static class invariants
|
||
cannot access the object (because they are checked from <code class="computeroutput"><span class="keyword">static</span></code>
|
||
member functions).
|
||
</p>
|
||
</div>
|
||
<div class="section">
|
||
<div class="titlepage"><div><div><h3 class="title">
|
||
<a name="boost_contract.contract_programming_overview.constructor_calls"></a><a class="link" href="contract_programming_overview.html#boost_contract.contract_programming_overview.constructor_calls" title="Constructor Calls">Constructor
|
||
Calls</a>
|
||
</h3></div></div></div>
|
||
<p>
|
||
A call to a constructor with a contract executes the following steps (see
|
||
<code class="computeroutput"><a class="link" href="../boost/contract/constructor_precondition.html" title="Class template constructor_precondition">boost::contract::constructor_precondition</a></code>
|
||
and <code class="computeroutput"><a class="link" href="../boost/contract/constructor.html" title="Function template constructor">boost::contract::constructor</a></code>):
|
||
</p>
|
||
<div class="orderedlist"><ol class="orderedlist" type="1">
|
||
<li class="listitem">
|
||
Check constructor preconditions (but these cannot access the object because
|
||
the object is not constructed yet).
|
||
</li>
|
||
<li class="listitem">
|
||
Execute the constructor member initialization list (if present).
|
||
<div class="orderedlist"><ol class="orderedlist" type="a"><li class="listitem">
|
||
Construct any base class (public or not) according with C++ construction
|
||
mechanism and also check the contracts of these base constructors
|
||
(according with steps similar to the ones listed here).
|
||
</li></ol></div>
|
||
</li>
|
||
<li class="listitem">
|
||
Check static class invariants (but not the non-static or volatile class
|
||
invariants, because the object is not constructed yet).
|
||
</li>
|
||
<li class="listitem">
|
||
Execute the constructor body.
|
||
</li>
|
||
<li class="listitem">
|
||
Check static class invariants (even if the body threw an exception).
|
||
</li>
|
||
<li class="listitem">
|
||
If the body did not throw an exception:
|
||
<div class="orderedlist"><ol class="orderedlist" type="a">
|
||
<li class="listitem">
|
||
Check non-static <a class="link" href="contract_programming_overview.html#and_anchor"><code class="literal"><span class="emphasis"><em>AND</em></span></code></a>
|
||
volatile class invariants (because the object is now successfully
|
||
constructed).
|
||
</li>
|
||
<li class="listitem">
|
||
Check constructor postconditions (but these cannot access the object
|
||
old value <code class="literal"><span class="emphasis"><em>oldof</em></span></code><code class="computeroutput"><span class="special">(*</span><span class="keyword">this</span><span class="special">)</span></code> because the object was not constructed
|
||
before the execution of the constructor body).
|
||
</li>
|
||
</ol></div>
|
||
</li>
|
||
<li class="listitem">
|
||
Else, check constructor exception guarantees (but these cannot access
|
||
the object old value <code class="literal"><span class="emphasis"><em>oldof</em></span></code><code class="computeroutput"><span class="special">(*</span><span class="keyword">this</span><span class="special">)</span></code> 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).
|
||
</li>
|
||
</ol></div>
|
||
<p>
|
||
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).
|
||
</p>
|
||
<p>
|
||
As indicated in step 2.a. above, C++ object construction mechanism will automatically
|
||
check base class contracts when these bases are initialized (no explicit
|
||
subcontracting behaviour is required here).
|
||
</p>
|
||
</div>
|
||
<div class="section">
|
||
<div class="titlepage"><div><div><h3 class="title">
|
||
<a name="boost_contract.contract_programming_overview.destructor_calls"></a><a class="link" href="contract_programming_overview.html#boost_contract.contract_programming_overview.destructor_calls" title="Destructor Calls">Destructor
|
||
Calls</a>
|
||
</h3></div></div></div>
|
||
<p>
|
||
A call to a destructor with a contract executes the following steps (see
|
||
<code class="computeroutput"><a class="link" href="../boost/contract/destructor.html" title="Function template destructor">boost::contract::destructor</a></code>):
|
||
</p>
|
||
<div class="orderedlist"><ol class="orderedlist" type="1">
|
||
<li class="listitem">
|
||
Check static class invariants <a class="link" href="contract_programming_overview.html#and_anchor"><code class="literal"><span class="emphasis"><em>AND</em></span></code></a>
|
||
non-static <a class="link" href="contract_programming_overview.html#and_anchor"><code class="literal"><span class="emphasis"><em>AND</em></span></code></a>
|
||
volatile class invariants.
|
||
</li>
|
||
<li class="listitem">
|
||
Execute the destructor body (destructors have no parameters and they
|
||
can be called at any time after object construction so they have no preconditions).
|
||
</li>
|
||
<li class="listitem">
|
||
Check static class invariants (even if the body threw an exception).
|
||
</li>
|
||
<li class="listitem">
|
||
If the body did not throw an exception:
|
||
<div class="orderedlist"><ol class="orderedlist" type="a">
|
||
<li class="listitem">
|
||
Check destructor postconditions (but these can only access class'
|
||
static members and the object old value <code class="literal"><span class="emphasis"><em>oldof</em></span></code><code class="computeroutput"><span class="special">(*</span><span class="keyword">this</span><span class="special">)</span></code> because the object has been destroyed
|
||
after successful execution of the destructor body). <a href="#ftn.boost_contract.contract_programming_overview.destructor_calls.f0" class="footnote" name="boost_contract.contract_programming_overview.destructor_calls.f0"><sup class="footnote">[11]</sup></a>
|
||
</li>
|
||
<li class="listitem">
|
||
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).
|
||
</li>
|
||
</ol></div>
|
||
</li>
|
||
<li class="listitem">
|
||
Else (even if destructors should rarely, if ever, be allowed to throw
|
||
exceptions in C++):
|
||
<div class="orderedlist"><ol class="orderedlist" type="a">
|
||
<li class="listitem">
|
||
Check non-static <a class="link" href="contract_programming_overview.html#and_anchor"><code class="literal"><span class="emphasis"><em>AND</em></span></code></a>
|
||
volatile class invariants (because the object was not successfully
|
||
destructed so it still exists and should satisfy its invariants).
|
||
</li>
|
||
<li class="listitem">
|
||
Check destructor exception guarantees.
|
||
</li>
|
||
</ol></div>
|
||
</li>
|
||
</ol></div>
|
||
<p>
|
||
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).
|
||
</p>
|
||
<div class="note"><table border="0" summary="Note">
|
||
<tr>
|
||
<td rowspan="2" align="center" valign="top" width="25"><img alt="[Note]" src="../../../../../doc/src/images/note.png"></td>
|
||
<th align="left">Note</th>
|
||
</tr>
|
||
<tr><td align="left" valign="top"><p>
|
||
Given that C++ allows destructors to throw, this library handles the case
|
||
when the destructor body throws an exception as indicated above. However,
|
||
in order to comply with STL exception safety guarantees and good C++ programming
|
||
practices, programmers should implement destructor bodies to rarely, if
|
||
ever, throw exceptions (in fact destructors are implicitly declared <code class="computeroutput"><span class="keyword">noexcept</span></code> in C++11).
|
||
</p></td></tr>
|
||
</table></div>
|
||
</div>
|
||
<div class="section">
|
||
<div class="titlepage"><div><div><h3 class="title">
|
||
<a name="boost_contract.contract_programming_overview.constant_correctness"></a><a class="link" href="contract_programming_overview.html#boost_contract.contract_programming_overview.constant_correctness" title="Constant-Correctness">Constant-Correctness</a>
|
||
</h3></div></div></div>
|
||
<p>
|
||
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 <code class="computeroutput"><span class="keyword">const</span></code>
|
||
context (via <code class="computeroutput"><span class="keyword">const</span><span class="special">&</span></code>,
|
||
<code class="computeroutput"><span class="keyword">const</span><span class="special">*</span>
|
||
<span class="keyword">const</span></code>, <code class="computeroutput"><span class="keyword">const</span>
|
||
<span class="keyword">volatile</span></code>, etc.).
|
||
</p>
|
||
<p>
|
||
Whenever possible (e.g., class invariants and postcondition old values),
|
||
this library automatically enforces this <span class="emphasis"><em>constant-correctness constraint</em></span>
|
||
at compile-time using <code class="computeroutput"><span class="keyword">const</span></code>.
|
||
However, this library cannot automatically enforce this constraint in all
|
||
cases (for preconditions and postconditions of mutable member functions,
|
||
for global variables, etc.). See <a class="link" href="extras.html#boost_contract.extras.no_lambda_functions__no_c__11_" title="No Lambda Functions (No C++11)">No
|
||
Lambda Functions</a> 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).
|
||
</p>
|
||
<div class="note"><table border="0" summary="Note">
|
||
<tr>
|
||
<td rowspan="2" align="center" valign="top" width="25"><img alt="[Note]" src="../../../../../doc/src/images/note.png"></td>
|
||
<th align="left">Note</th>
|
||
</tr>
|
||
<tr><td align="left" valign="top"><p>
|
||
In general, it is the responsibility of the programmers to code assertions
|
||
that only check, and do not change, program variables. <a href="#ftn.boost_contract.contract_programming_overview.constant_correctness.f0" class="footnote" name="boost_contract.contract_programming_overview.constant_correctness.f0"><sup class="footnote">[12]</sup></a>
|
||
</p></td></tr>
|
||
</table></div>
|
||
</div>
|
||
<div class="section">
|
||
<div class="titlepage"><div><div><h3 class="title">
|
||
<a name="boost_contract.contract_programming_overview.specifications_vs__implementation"></a><a class="link" href="contract_programming_overview.html#boost_contract.contract_programming_overview.specifications_vs__implementation" title="Specifications vs. Implementation">Specifications
|
||
vs. Implementation</a>
|
||
</h3></div></div></div>
|
||
<p>
|
||
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.
|
||
</p>
|
||
<p>
|
||
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 <a class="link" href="extras.html#boost_contract.extras.separate_body_implementation" title="Separate Body Implementation">Separate
|
||
Body Implementation</a> 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).
|
||
</p>
|
||
<p>
|
||
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 (<code class="computeroutput"><span class="keyword">friend</span></code>, 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).
|
||
(<a class="link" href="bibliography.html#N1962_anchor">[N1962]</a> 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.)
|
||
<a href="#ftn.boost_contract.contract_programming_overview.specifications_vs__implementation.f0" class="footnote" name="boost_contract.contract_programming_overview.specifications_vs__implementation.f0"><sup class="footnote">[13]</sup></a>
|
||
</p>
|
||
</div>
|
||
<div class="section">
|
||
<div class="titlepage"><div><div><h3 class="title">
|
||
<a name="boost_contract.contract_programming_overview.on_contract_failures"></a><a class="link" href="contract_programming_overview.html#boost_contract.contract_programming_overview.on_contract_failures" title="On Contract Failures">On
|
||
Contract Failures</a>
|
||
</h3></div></div></div>
|
||
<p>
|
||
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 <span class="emphasis"><em>failure handler functions</em></span>.
|
||
<a href="#ftn.boost_contract.contract_programming_overview.on_contract_failures.f0" class="footnote" name="boost_contract.contract_programming_overview.on_contract_failures.f0"><sup class="footnote">[14]</sup></a>
|
||
</p>
|
||
<p>
|
||
By default, these failure handler functions print a message to the standard
|
||
error <code class="computeroutput"><span class="identifier">std</span><span class="special">::</span><span class="identifier">cerr</span></code> (with detailed information about the
|
||
failure) and then terminate the program calling <code class="computeroutput"><span class="identifier">std</span><span class="special">::</span><span class="identifier">terminate</span></code>.
|
||
However, using <code class="computeroutput"><a class="link" href="../boost/contract/set_precondition_failure.html" title="Function set_precondition_failure">boost::contract::set_precondition_failure</a></code>,
|
||
<code class="computeroutput"><a class="link" href="../boost/contract/set_postcondition_failure.html" title="Function set_postcondition_failure">boost::contract::set_postcondition_failure</a></code>,
|
||
<code class="computeroutput"><a class="link" href="../boost/contract/set_except_failure.html" title="Function set_except_failure">boost::contract::set_except_failure</a></code>,
|
||
<code class="computeroutput"><a class="link" href="../boost/contract/set_invariant_failure.html" title="Function set_invariant_failure">boost::contract::set_invariant_failure</a></code>,
|
||
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 <a class="link" href="advanced.html#boost_contract.advanced.throw_on_failures__and__noexcept__" title="Throw on Failures (and noexcept)">Throw
|
||
on Failures</a>). <a href="#ftn.boost_contract.contract_programming_overview.on_contract_failures.f1" class="footnote" name="boost_contract.contract_programming_overview.on_contract_failures.f1"><sup class="footnote">[15]</sup></a>
|
||
</p>
|
||
<div class="note"><table border="0" summary="Note">
|
||
<tr>
|
||
<td rowspan="2" align="center" valign="top" width="25"><img alt="[Note]" src="../../../../../doc/src/images/note.png"></td>
|
||
<th align="left">Note</th>
|
||
</tr>
|
||
<tr><td align="left" valign="top"><p>
|
||
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 <code class="computeroutput"><span class="keyword">noexcept</span></code>
|
||
declarations for destructors, etc.). 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.
|
||
</p></td></tr>
|
||
</table></div>
|
||
<p>
|
||
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). The contract
|
||
failure handler functions programmed using this library have information
|
||
about the failed contract (preconditions, postconditions, etc.) and the operation
|
||
that was checking the contract (constructor, destructor, etc.) so programmers
|
||
can granularly distinguish all cases and decide when it is appropriate to
|
||
terminate, throw, or take some other user-specific action.
|
||
</p>
|
||
</div>
|
||
<div class="section">
|
||
<div class="titlepage"><div><div><h3 class="title">
|
||
<a name="boost_contract.contract_programming_overview.feature_summary"></a><a class="link" href="contract_programming_overview.html#boost_contract.contract_programming_overview.feature_summary" title="Feature Summary">Feature
|
||
Summary</a>
|
||
</h3></div></div></div>
|
||
<p>
|
||
The contract programming features supported by this library are largely based
|
||
on <a class="link" href="bibliography.html#N1962_anchor">[N1962]</a> and on the Eiffel programming
|
||
language.
|
||
</p>
|
||
<p>
|
||
The following table compares contract programming features among this library,
|
||
<a class="link" href="bibliography.html#N1962_anchor">[N1962]</a> (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 <a class="link" href="bibliography.html#N1962_anchor">[N1962]</a>
|
||
itself is sound), a more recent proposal <a class="link" href="bibliography.html#P0380_anchor">[P0380]</a>
|
||
(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.
|
||
</p>
|
||
<div class="informaltable"><table class="table">
|
||
<colgroup>
|
||
<col>
|
||
<col>
|
||
<col>
|
||
<col>
|
||
<col>
|
||
<col>
|
||
</colgroup>
|
||
<thead><tr>
|
||
<th>
|
||
<p>
|
||
Feature
|
||
</p>
|
||
</th>
|
||
<th>
|
||
<p>
|
||
This Library
|
||
</p>
|
||
</th>
|
||
<th>
|
||
<p>
|
||
<a class="link" href="bibliography.html#N1962_anchor">[N1962]</a> Proposal (not accepted
|
||
in C++)
|
||
</p>
|
||
</th>
|
||
<th>
|
||
<p>
|
||
C++20 (see <a class="link" href="bibliography.html#P0380_anchor">[P0380]</a>)
|
||
</p>
|
||
</th>
|
||
<th>
|
||
<p>
|
||
ISE Eiffel 5.4 (see <a class="link" href="bibliography.html#Meyer97_anchor">[Meyer97]</a>)
|
||
</p>
|
||
</th>
|
||
<th>
|
||
<p>
|
||
D (see <a class="link" href="bibliography.html#Bright04_anchor">[Bright04]</a>)
|
||
</p>
|
||
</th>
|
||
</tr></thead>
|
||
<tbody>
|
||
<tr>
|
||
<td>
|
||
<p>
|
||
<span class="emphasis"><em>Keywords and specifiers</em></span>
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Specifiers: <code class="computeroutput"><span class="identifier">precondition</span></code>,
|
||
<code class="computeroutput"><span class="identifier">postcondition</span></code>,
|
||
<code class="computeroutput"><span class="identifier">invariant</span></code>, <code class="computeroutput"><span class="identifier">static_invariant</span></code>, and <code class="computeroutput"><span class="identifier">base_types</span></code>. The last three specifiers
|
||
appear in user code so their names can be referred to or changed
|
||
using <code class="computeroutput"><a class="link" href="../BOOST_CONTRACT_INVARIANT.html" title="Macro BOOST_CONTRACT_INVARIANT">BOOST_CONTRACT_INVARIANT</a></code>,
|
||
<code class="computeroutput"><a class="link" href="../BOOST_CO_idm45028038619104.html" title="Macro BOOST_CONTRACT_STATIC_INVARIANT">BOOST_CONTRACT_STATIC_INVARIANT</a></code>,
|
||
and <code class="computeroutput"><a class="link" href="../BOOST_CO_idm45028039730032.html" title="Macro BOOST_CONTRACT_BASES_TYPEDEF">BOOST_CONTRACT_BASES_TYPEDEF</a></code>
|
||
macros respectively to avoid name clashes.
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Keywords: <code class="computeroutput"><span class="identifier">precondition</span></code>,
|
||
<code class="computeroutput"><span class="identifier">postcondition</span></code>,
|
||
<code class="computeroutput"><span class="identifier">oldof</span></code>, and <code class="computeroutput"><span class="identifier">invariant</span></code>.
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Attributes: <code class="computeroutput"><span class="special">[[</span><span class="identifier">expects</span><span class="special">]]</span></code> and <code class="computeroutput"><span class="special">[[</span><span class="identifier">ensures</span><span class="special">]]</span></code>.
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Keywords: <code class="literal">require</code>, <code class="literal">require else</code>,
|
||
<code class="literal">ensure</code>, <code class="literal">ensure then</code>, <code class="literal">old</code>,
|
||
<code class="literal">result</code>, <code class="literal">do</code>, and <code class="literal">invariant</code>.
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Keywords: <code class="literal">in</code>, <code class="literal">out</code>, <code class="literal">do</code>,
|
||
<code class="literal">assert</code>, and <code class="literal">invariant</code>.
|
||
</p>
|
||
</td>
|
||
</tr>
|
||
<tr>
|
||
<td>
|
||
<p>
|
||
<span class="emphasis"><em>On contract failures</em></span>
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Print an error to <code class="computeroutput"><span class="identifier">std</span><span class="special">::</span><span class="identifier">cerr</span></code>
|
||
and call <code class="computeroutput"><span class="identifier">std</span><span class="special">::</span><span class="identifier">terminate</span></code> (but can be customized
|
||
to throw exceptions, exit with an error code, etc.).
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Call <code class="computeroutput"><span class="identifier">std</span><span class="special">::</span><span class="identifier">terminate</span></code> (but can be customized
|
||
to throw exceptions, exit with an error code, etc.).
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Call <code class="computeroutput"><span class="identifier">std</span><span class="special">::</span><span class="identifier">abort</span></code> (but can be customized
|
||
to throw exceptions, exit with an error code, etc.).
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Throw exceptions.
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Throw exceptions.
|
||
</p>
|
||
</td>
|
||
</tr>
|
||
<tr>
|
||
<td>
|
||
<p>
|
||
<span class="emphasis"><em>Return values in postconditions</em></span>
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Yes, captured by or passed as a parameter to (for virtual functions)
|
||
the postcondition functor.
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Yes, <code class="computeroutput"><span class="identifier">postcondition</span><span class="special">(</span></code><code class="literal"><span class="emphasis"><em>result-variable-name</em></span></code><code class="computeroutput"><span class="special">)</span></code>.
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Yes, <code class="computeroutput"><span class="special">[[</span><span class="identifier">ensures</span>
|
||
</code><code class="literal"><span class="emphasis"><em>result-variable-name</em></span></code><code class="computeroutput"><span class="special">:</span> <span class="special">...]]</span></code>.
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Yes, <code class="literal">result</code> keyword.
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Yes, <code class="computeroutput"><span class="identifier">out</span><span class="special">(</span></code><code class="literal"><span class="emphasis"><em>result-variable-name</em></span></code><code class="computeroutput"><span class="special">)</span></code>.
|
||
</p>
|
||
</td>
|
||
</tr>
|
||
<tr>
|
||
<td>
|
||
<p>
|
||
<span class="emphasis"><em>Old values in postconditions</em></span>
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Yes, <code class="computeroutput"><a class="link" href="../BOOST_CONTRACT_OLDOF.html" title="Macro BOOST_CONTRACT_OLDOF">BOOST_CONTRACT_OLDOF</a></code>
|
||
macro and <code class="computeroutput"><a class="link" href="../boost/contract/old_ptr.html" title="Class template old_ptr">boost::contract::old_ptr</a></code>
|
||
(but copied before preconditions unless <code class="computeroutput"><span class="special">.</span><span class="identifier">old</span><span class="special">(...)</span></code>
|
||
is used as shown in <a class="link" href="advanced.html#boost_contract.advanced.old_values_copied_at_body" title="Old Values Copied at Body">Old
|
||
Values Copied at Body</a>). For templates, <code class="computeroutput"><a class="link" href="../boost/contract/old_ptr_if_copyable.html" title="Class template old_ptr_if_copyable">boost::contract::old_ptr_if_copyable</a></code>
|
||
skips old value copies for non-copyable types and <code class="computeroutput"><a class="link" href="../boost/contract/condition_if.html" title="Function template condition_if">boost::contract::condition_if</a></code>
|
||
skips old value copies selectively based on old expression type
|
||
requirements (on compilers that do not support <code class="computeroutput"><span class="keyword">if</span>
|
||
<span class="keyword">constexpr</span></code>).
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Yes, <code class="computeroutput"><span class="identifier">oldof</span></code> keyword
|
||
(copied right after preconditions). (Never skipped, not even in
|
||
templates for non-copyable types.)
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
No.
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Yes, <code class="literal">old</code> keyword (copied right after preconditions).
|
||
(Never skipped, but all types are copyable in Eiffel.)
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
No.
|
||
</p>
|
||
</td>
|
||
</tr>
|
||
<tr>
|
||
<td>
|
||
<p>
|
||
<span class="emphasis"><em>Class invariants</em></span>
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Yes, checked at constructor exit, at destructor entry and throw,
|
||
and at public function entry, exit, and throw. Same for volatile
|
||
class invariants. Static class invariants checked at entry, exit,
|
||
and throw for constructors, destructors, and any (also <code class="computeroutput"><span class="keyword">static</span></code>) public function.
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Yes, checked at constructor exit, at destructor entry and throw,
|
||
and at public function entry, exit, and throw. (Volatile and static
|
||
class invariants not supported.)
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
No.
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Yes, checked at constructor exit, and around public functions.
|
||
(Volatile and static class invariants do not apply to Eiffel.)
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Yes, checked at constructor exit, at destructor entry, and around
|
||
public functions. However, invariants cannot call public functions
|
||
(to avoid infinite recursion because D does not disable contracts
|
||
while checking other contracts). (Volatile and static class invariants
|
||
not supported, <code class="computeroutput"><span class="keyword">volatile</span></code>
|
||
was deprecated all together in D.)
|
||
</p>
|
||
</td>
|
||
</tr>
|
||
<tr>
|
||
<td>
|
||
<p>
|
||
<span class="emphasis"><em>Subcontracting</em></span>
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Yes, also supports subcontracting for multiple inheritance (<code class="computeroutput"><a class="link" href="../BOOST_CONTRACT_BASE_TYPES.html" title="Macro BOOST_CONTRACT_BASE_TYPES">BOOST_CONTRACT_BASE_TYPES</a></code>,
|
||
<code class="computeroutput"><a class="link" href="../BOOST_CONTRACT_OVERRIDE.html" title="Macro BOOST_CONTRACT_OVERRIDE">BOOST_CONTRACT_OVERRIDE</a></code>,
|
||
and <code class="computeroutput"><a class="link" href="../boost/contract/virtual_.html" title="Class virtual_">boost::contract::virtual_</a></code>
|
||
are used to declare base classes, overrides and virtual public
|
||
functions respectively).
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Yes, also supports subcontracting for multiple inheritance, but
|
||
preconditions cannot be subcontracted. <a href="#ftn.boost_contract.contract_programming_overview.feature_summary.f0" class="footnote" name="boost_contract.contract_programming_overview.feature_summary.f0"><sup class="footnote">[a]</sup></a>
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
No.
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Yes.
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Yes.
|
||
</p>
|
||
</td>
|
||
</tr>
|
||
<tr>
|
||
<td>
|
||
<p>
|
||
<span class="emphasis"><em>Contracts for pure virtual functions</em></span>
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Yes (programmed via out-of-line functions as always in C++ with
|
||
pure virtual function definitions).
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Yes.
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
No (because no subcontracting).
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Yes (contracts for abstract functions).
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
No.
|
||
</p>
|
||
</td>
|
||
</tr>
|
||
<tr>
|
||
<td>
|
||
<p>
|
||
<span class="emphasis"><em>Arbitrary code in contracts</em></span>
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Yes (but users are generally recommended to only program assertions
|
||
using <code class="computeroutput"><a class="link" href="../BOOST_CONTRACT_ASSERT.html" title="Macro BOOST_CONTRACT_ASSERT">BOOST_CONTRACT_ASSERT</a></code>
|
||
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).
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
No, assertions only (use of only public functions to program preconditions
|
||
is recommended but not prescribed).
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
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).
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
No, assertions only (in addition only public members can be used
|
||
in preconditions).
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Yes.
|
||
</p>
|
||
</td>
|
||
</tr>
|
||
<tr>
|
||
<td>
|
||
<p>
|
||
<span class="emphasis"><em>Constant-correctness</em></span>
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
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).
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Yes.
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Yes (side effects in contracts lead to undefined behaviour).
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Yes.
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
No, enforced only for class invariants.
|
||
</p>
|
||
</td>
|
||
</tr>
|
||
<tr>
|
||
<td>
|
||
<p>
|
||
<span class="emphasis"><em>Contracts in specifications</em></span>
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
No, in function definitions instead (unless programmers manually
|
||
write an extra function for any given function).
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Yes (in function declarations).
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Yes (in function declarations).
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Yes.
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Yes.
|
||
</p>
|
||
</td>
|
||
</tr>
|
||
<tr>
|
||
<td>
|
||
<p>
|
||
<span class="emphasis"><em>Function code ordering</em></span>
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Preconditions, postconditions, exception guarantees, body.
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Preconditions, postconditions, body.
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Preconditions, postconditions, body.
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Preconditions, body, postconditions.
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Preconditions, postconditions, body.
|
||
</p>
|
||
</td>
|
||
</tr>
|
||
<tr>
|
||
<td>
|
||
<p>
|
||
<span class="emphasis"><em>Disable assertion checking within assertions checking
|
||
(to avoid infinite recursion when checking contracts)</em></span>
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Yes, but use <code class="computeroutput"><a class="link" href="../BOOST_CO_idm45028039682816.html" title="Macro BOOST_CONTRACT_PRECONDITIONS_DISABLE_NO_ASSERTION">BOOST_CONTRACT_PRECONDITIONS_DISABLE_NO_ASSERTION</a></code>
|
||
to disable no assertion while checking preconditions (see also
|
||
<code class="computeroutput"><a class="link" href="../BOOST_CO_idm45028039677008.html" title="Macro BOOST_CONTRACT_ALL_DISABLE_NO_ASSERTION">BOOST_CONTRACT_ALL_DISABLE_NO_ASSERTION</a></code>).
|
||
<a href="#ftn.boost_contract.contract_programming_overview.feature_summary.f1" class="footnote" name="boost_contract.contract_programming_overview.feature_summary.f1"><sup class="footnote">[b]</sup></a> (In multi-threaded programs this introduces a global
|
||
lock, see <code class="computeroutput"><a class="link" href="../BOOST_CO_idm45028039741520.html" title="Macro BOOST_CONTRACT_DISABLE_THREADS">BOOST_CONTRACT_DISABLE_THREADS</a></code>.)
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Yes for class invariants and postconditions, but preconditions
|
||
disable no assertion.
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
No.
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Yes.
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
No.
|
||
</p>
|
||
</td>
|
||
</tr>
|
||
<tr>
|
||
<td>
|
||
<p>
|
||
<span class="emphasis"><em>Nested member function calls</em></span>
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Disable nothing. <a href="#ftn.boost_contract.contract_programming_overview.feature_summary.f2" class="footnote" name="boost_contract.contract_programming_overview.feature_summary.f2"><sup class="footnote">[c]</sup></a>
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Disable nothing.
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Disable nothing.
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Disable all contract assertions.
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Disable nothing.
|
||
</p>
|
||
</td>
|
||
</tr>
|
||
<tr>
|
||
<td>
|
||
<p>
|
||
<span class="emphasis"><em>Disable contract checking</em></span>
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Yes, contract checking can be skipped at run-time by defining combinations
|
||
of the <code class="computeroutput"><a class="link" href="../BOOST_CO_idm45028039660048.html" title="Macro BOOST_CONTRACT_NO_PRECONDITIONS">BOOST_CONTRACT_NO_PRECONDITIONS</a></code>,
|
||
<code class="computeroutput"><a class="link" href="../BOOST_CO_idm45028039653664.html" title="Macro BOOST_CONTRACT_NO_POSTCONDITIONS">BOOST_CONTRACT_NO_POSTCONDITIONS</a></code>,
|
||
<code class="computeroutput"><a class="link" href="../BOOST_CO_idm45028039619664.html" title="Macro BOOST_CONTRACT_NO_INVARIANTS">BOOST_CONTRACT_NO_INVARIANTS</a></code>,
|
||
<code class="computeroutput"><a class="link" href="../BOOST_CO_idm45028039634896.html" title="Macro BOOST_CONTRACT_NO_ENTRY_INVARIANTS">BOOST_CONTRACT_NO_ENTRY_INVARIANTS</a></code>,
|
||
and <code class="computeroutput"><a class="link" href="../BOOST_CO_idm45028039627280.html" title="Macro BOOST_CONTRACT_NO_EXIT_INVARIANTS">BOOST_CONTRACT_NO_EXIT_INVARIANTS</a></code>
|
||
macros (completely removing contract code from compiled object
|
||
code is also possible but requires using macros as shown in <a class="link" href="extras.html#boost_contract.extras.disable_contract_compilation__macro_interface_" title="Disable Contract Compilation (Macro Interface)">Disable
|
||
Contract Compilation</a>).
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Yes (contract code also removed from compiled object code, but
|
||
details are compiler-implementation specific).
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Yes (contract code also removed from compiled object code, but
|
||
details are compiler-implementation specific).
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Yes, but only predefined combinations of preconditions, postconditions,
|
||
and class invariants can be disabled (contract code also removed
|
||
from compiled object code).
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Yes.
|
||
</p>
|
||
</td>
|
||
</tr>
|
||
<tr>
|
||
<td>
|
||
<p>
|
||
<span class="emphasis"><em>Assertion levels</em></span>
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Yes, predefined default, audit, and axiom, in addition programmers
|
||
can also define their own levels.
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
No (but a previous revision of this proposal considered adding
|
||
assertion levels under the name of "assertion ordering").
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Yes, predefined default, audit, and axiom.
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
No.
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
No.
|
||
</p>
|
||
</td>
|
||
</tr>
|
||
</tbody>
|
||
<tbody class="footnotes"><tr><td colspan="6">
|
||
<div id="ftn.boost_contract.contract_programming_overview.feature_summary.f0" class="footnote"><p><a href="#boost_contract.contract_programming_overview.feature_summary.f0" class="para"><sup class="para">[a] </sup></a>
|
||
<span class="bold"><strong>Rationale:</strong></span> The authors of <a class="link" href="bibliography.html#N1962_anchor">[N1962]</a> decided to forbid derived
|
||
classes from subcontracting preconditions because they found
|
||
that such a feature was rarely, if ever, used (see <a href="http://lists.boost.org/Archives/boost/2010/04/164862.php" target="_top">Re:
|
||
[boost] [contract] diff n1962</a>). Still, it should be noted
|
||
that even in <a class="link" href="bibliography.html#N1962_anchor">[N1962]</a> 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 <a class="link" href="contract_programming_overview.html#or_anchor"><code class="literal"><span class="emphasis"><em>OR</em></span></code></a>
|
||
(so even in <a class="link" href="bibliography.html#N1962_anchor">[N1962]</a> preconditions
|
||
can indirectly subcontract when multiple inheritance is used).
|
||
Furthermore, subcontracting preconditions is soundly defined
|
||
by the <a href="http://en.wikipedia.org/wiki/Liskov_substitution_principle" target="_top">substitution
|
||
principle</a> 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 differs from <a class="link" href="bibliography.html#N1962_anchor">[N1962]</a>.)
|
||
</p></div>
|
||
<div id="ftn.boost_contract.contract_programming_overview.feature_summary.f1" class="footnote"><p><a href="#boost_contract.contract_programming_overview.feature_summary.f1" class="para"><sup class="para">[b] </sup></a>
|
||
<span class="bold"><strong>Rationale:</strong></span> 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 <a class="link" href="bibliography.html#N1962_anchor">[N1962]</a> does
|
||
not disable any assertion while checking preconditions, see
|
||
<a href="http://lists.boost.org/Archives/boost/2010/04/164862.php" target="_top">Re:
|
||
[boost] [contract] diff n1962</a>). 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 <a class="link" href="bibliography.html#N1962_anchor">[N1962]</a>
|
||
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 <code class="computeroutput"><a class="link" href="../BOOST_CO_idm45028039682816.html" title="Macro BOOST_CONTRACT_PRECONDITIONS_DISABLE_NO_ASSERTION">BOOST_CONTRACT_PRECONDITIONS_DISABLE_NO_ASSERTION</a></code>
|
||
configuration macro so users can change this behaviour to match
|
||
<a class="link" href="bibliography.html#N1962_anchor">[N1962]</a> if needed.
|
||
</p></div>
|
||
<div id="ftn.boost_contract.contract_programming_overview.feature_summary.f2" class="footnote"><p><a href="#boost_contract.contract_programming_overview.feature_summary.f2" class="para"><sup class="para">[c] </sup></a>
|
||
<span class="bold"><strong>Rationale:</strong></span> 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 <a class="link" href="bibliography.html#N1962_anchor">[N1962]</a>
|
||
but it is no longer required by <a class="link" href="bibliography.html#N1962_anchor">[N1962]</a>
|
||
(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.
|
||
</p></div>
|
||
</td></tr></tbody>
|
||
</table></div>
|
||
<p>
|
||
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 <a class="link" href="bibliography.html" title="Bibliography">Bibliography</a>
|
||
for a complete list of all references consulted during the design and development
|
||
of this library):
|
||
</p>
|
||
<div class="informaltable"><table class="table">
|
||
<colgroup>
|
||
<col>
|
||
<col>
|
||
<col>
|
||
</colgroup>
|
||
<thead><tr>
|
||
<th>
|
||
<p>
|
||
Reference
|
||
</p>
|
||
</th>
|
||
<th>
|
||
<p>
|
||
Language
|
||
</p>
|
||
</th>
|
||
<th>
|
||
<p>
|
||
Notes
|
||
</p>
|
||
</th>
|
||
</tr></thead>
|
||
<tbody>
|
||
<tr>
|
||
<td>
|
||
<p>
|
||
<a class="link" href="bibliography.html#Bright04b_anchor">[Bright04b]</a>
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Digital Mars C++
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
The Digital Mars C++ compiler extends C++ adding contract programming
|
||
language support (among many other features).
|
||
</p>
|
||
</td>
|
||
</tr>
|
||
<tr>
|
||
<td>
|
||
<p>
|
||
<a class="link" href="bibliography.html#Maley99_anchor">[Maley99]</a>
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
C++
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
This supports contract programming including subcontracting but
|
||
with limitations (e.g., programmers need to manually build an inheritance
|
||
tree using artificial template parameters), it does not use macros
|
||
but programmers are required to write by hand a significant amount
|
||
of boiler-plate code. (The authors have found this work very inspiring
|
||
when developing initial revisions of this library especially for
|
||
its attempt to support subcontracting.)
|
||
</p>
|
||
</td>
|
||
</tr>
|
||
<tr>
|
||
<td>
|
||
<p>
|
||
<a class="link" href="bibliography.html#Lindrud04_anchor">[Lindrud04]</a>
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
C++
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
This supports class invariants and old values but it does not support
|
||
subcontracting (contracts are specified within definitions instead
|
||
of declarations and assertions are not constant-correct).
|
||
</p>
|
||
</td>
|
||
</tr>
|
||
<tr>
|
||
<td>
|
||
<p>
|
||
<a class="link" href="bibliography.html#Tandin04_anchor">[Tandin04]</a>
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
C++
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Interestingly, these contract macros automatically generate Doxygen
|
||
documentation <a href="#ftn.boost_contract.contract_programming_overview.feature_summary.f3" class="footnote" name="boost_contract.contract_programming_overview.feature_summary.f3"><sup class="footnote">[a]</sup></a> but old values, class invariants, and subcontracting
|
||
are not supported (plus contracts are specified within definitions
|
||
instead of declarations and assertions are not constant-correct).
|
||
</p>
|
||
</td>
|
||
</tr>
|
||
<tr>
|
||
<td>
|
||
<p>
|
||
<a class="link" href="bibliography.html#Nana_anchor">[Nana]</a>
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
GCC C++
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
This uses macros but it only works on GCC (and maybe Clang, but
|
||
it does not work on MSVC, etc.). It does not support subcontracting.
|
||
It requires extra care to program postconditions for functions
|
||
with multiple return statements. It seems that it might not check
|
||
class invariants when functions throw exceptions (unless the <code class="computeroutput"><span class="identifier">END</span></code> macro does that...). (In
|
||
addition, it provides tools for logging and integration with GDB.)
|
||
</p>
|
||
</td>
|
||
</tr>
|
||
<tr>
|
||
<td>
|
||
<p>
|
||
<a class="link" href="bibliography.html#C2_anchor">[C2]</a>
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
C++
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
This uses an external preprocessing tool (the authors could no
|
||
longer find this project's code to evaluate it).
|
||
</p>
|
||
</td>
|
||
</tr>
|
||
<tr>
|
||
<td>
|
||
<p>
|
||
<a class="link" href="bibliography.html#iContract_anchor">[iContract]</a>
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Java
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
This uses an external preprocessing tool.
|
||
</p>
|
||
</td>
|
||
</tr>
|
||
<tr>
|
||
<td>
|
||
<p>
|
||
<a class="link" href="bibliography.html#Jcontract_anchor">[Jcontract]</a>
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Java
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
This uses an external preprocessing tool.
|
||
</p>
|
||
</td>
|
||
</tr>
|
||
<tr>
|
||
<td>
|
||
<p>
|
||
<a class="link" href="bibliography.html#CodeContracts_anchor">[CodeContracts]</a>
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
.NET
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Microsoft contract programming for .NET programming languages.
|
||
</p>
|
||
</td>
|
||
</tr>
|
||
<tr>
|
||
<td>
|
||
<p>
|
||
<a class="link" href="bibliography.html#SpecSharp_anchor">[SpecSharp]</a>
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
C#
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
This is a C# extension with contract programming language support.
|
||
</p>
|
||
</td>
|
||
</tr>
|
||
<tr>
|
||
<td>
|
||
<p>
|
||
<a class="link" href="bibliography.html#Chrome_anchor">[Chrome]</a>
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Object Pascal
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
This is the .NET version of Object Pascal and it has language support
|
||
for contract programming.
|
||
</p>
|
||
</td>
|
||
</tr>
|
||
<tr>
|
||
<td>
|
||
<p>
|
||
<a class="link" href="bibliography.html#SPARKAda_anchor">[SPARKAda]</a>
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
Ada
|
||
</p>
|
||
</td>
|
||
<td>
|
||
<p>
|
||
This is an Ada-like programming language with support for contract
|
||
programming.
|
||
</p>
|
||
</td>
|
||
</tr>
|
||
</tbody>
|
||
<tbody class="footnotes"><tr><td colspan="3"><div id="ftn.boost_contract.contract_programming_overview.feature_summary.f3" class="footnote"><p><a href="#boost_contract.contract_programming_overview.feature_summary.f3" class="para"><sup class="para">[a] </sup></a>
|
||
<span class="bold"><strong>Rationale:</strong></span> Older versions of
|
||
this library also automatically generated Doxygen documentation
|
||
from contract definition macros. This functionality was abandoned
|
||
for a number of reasons: This library no longer uses macros to
|
||
program contracts; even before that, the implementation of this
|
||
library macros became too complex and the Doxygen preprocessor
|
||
was no longer able to expand them; the Doxygen documentation
|
||
was just a repeat of the contract code (so programmers could
|
||
directly look at contracts in the source code); Doxygen might
|
||
not necessarily be the documentation tool used by all C++ programmers.
|
||
</p></div></td></tr></tbody>
|
||
</table></div>
|
||
<p>
|
||
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:
|
||
</p>
|
||
<div class="itemizedlist"><ul class="itemizedlist" style="list-style-type: disc; ">
|
||
<li class="listitem">
|
||
Implementing preconditions and postconditions in C++ is not difficult
|
||
(e.g., using some kind of RAII object).
|
||
</li>
|
||
<li class="listitem">
|
||
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. <a href="#ftn.boost_contract.contract_programming_overview.feature_summary.f4" class="footnote" name="boost_contract.contract_programming_overview.feature_summary.f4"><sup class="footnote">[16]</sup></a>
|
||
</li>
|
||
<li class="listitem">
|
||
Implementing class invariants is more involved (especially if done automatically,
|
||
without requiring programmers to manually invoke extra functions to check
|
||
the invariants). <a href="#ftn.boost_contract.contract_programming_overview.feature_summary.f5" class="footnote" name="boost_contract.contract_programming_overview.feature_summary.f5"><sup class="footnote">[17]</sup></a> In addition, all references reviewed by the authors seem
|
||
to not consider static and volatile functions not supporting static and
|
||
volatile invariants respectively.
|
||
</li>
|
||
<li class="listitem">
|
||
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). <a href="#ftn.boost_contract.contract_programming_overview.feature_summary.f6" class="footnote" name="boost_contract.contract_programming_overview.feature_summary.f6"><sup class="footnote">[18]</sup></a>
|
||
</li>
|
||
</ul></div>
|
||
</div>
|
||
<div class="footnotes">
|
||
<br><hr style="width:100; text-align:left;margin-left: 0">
|
||
<div id="ftn.boost_contract.contract_programming_overview.assertions.f0" class="footnote"><p><a href="#boost_contract.contract_programming_overview.assertions.f0" class="para"><sup class="para">[6] </sup></a>
|
||
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
|
||
<a class="link" href="bibliography.html" title="Bibliography">Bibliography</a>). 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).
|
||
</p></div>
|
||
<div id="ftn.boost_contract.contract_programming_overview.assertions.f1" class="footnote"><p><a href="#boost_contract.contract_programming_overview.assertions.f1" class="para"><sup class="para">[7] </sup></a>
|
||
<span class="bold"><strong>Rationale:</strong></span> Contract assertions for
|
||
exception guarantees were first introduced by this library, they are
|
||
not part of <a class="link" href="bibliography.html#N1962_anchor">[N1962]</a> or other references
|
||
listed in the <a class="link" href="bibliography.html" title="Bibliography">Bibliography</a>
|
||
(even if exception safety guarantees have long been part of C++ STL
|
||
documentation).
|
||
</p></div>
|
||
<div id="ftn.boost_contract.contract_programming_overview.assertions.f2" class="footnote"><p><a href="#boost_contract.contract_programming_overview.assertions.f2" class="para"><sup class="para">[8] </sup></a>
|
||
<span class="bold"><strong>Rationale:</strong></span> 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 <a class="link" href="bibliography.html#N1962_anchor">[N1962]</a> or
|
||
other references listed in the <a class="link" href="bibliography.html" title="Bibliography">Bibliography</a>.
|
||
</p></div>
|
||
<div id="ftn.boost_contract.contract_programming_overview.assertions.f3" class="footnote"><p><a href="#boost_contract.contract_programming_overview.assertions.f3" class="para"><sup class="para">[9] </sup></a>
|
||
<span class="bold"><strong>Rationale:</strong></span> <code class="computeroutput"><a class="link" href="../BOOST_CO_idm45028039741520.html" title="Macro BOOST_CONTRACT_DISABLE_THREADS">BOOST_CONTRACT_DISABLE_THREADS</a></code>
|
||
is named after <code class="computeroutput"><span class="identifier">BOOST_DISABLE_THREADS</span></code>.
|
||
</p></div>
|
||
<div id="ftn.boost_contract.contract_programming_overview.benefits_and_costs.f0" class="footnote"><p><a href="#boost_contract.contract_programming_overview.benefits_and_costs.f0" class="para"><sup class="para">[10] </sup></a>
|
||
Of course, if contracts are ill-written then contract programming is
|
||
of little use. However, it is less likely to have a bug in both the
|
||
function body and the contract than in the function body alone. For
|
||
example, consider the validation of a result in postconditions. Validating
|
||
the return value might seem redundant, but in this case we actually
|
||
want that redundancy. When programmers write a function, there is a
|
||
certain probability that they make a mistake in implementing the function
|
||
body. When programmers specify the result of the function in the postconditions,
|
||
there is also a certain probability that they make a mistake in writing
|
||
the contract. However, the probability that programmers make a mistake
|
||
twice (in both the body <span class="emphasis"><em>and</em></span> the contract) is in
|
||
general lower than the probability that the mistake is made only once
|
||
(in either the body <span class="emphasis"><em>or</em></span> the contract).
|
||
</p></div>
|
||
<div id="ftn.boost_contract.contract_programming_overview.destructor_calls.f0" class="footnote"><p><a href="#boost_contract.contract_programming_overview.destructor_calls.f0" class="para"><sup class="para">[11] </sup></a>
|
||
<span class="bold"><strong>Rationale:</strong></span> Postconditions for
|
||
destructors are not part of <a class="link" href="bibliography.html#N1962_anchor">[N1962]</a>
|
||
or other references listed in the <a class="link" href="bibliography.html" title="Bibliography">Bibliography</a>
|
||
(but with respect to <a class="link" href="bibliography.html#Meyer97_anchor">[Meyer97]</a>
|
||
it should be noted that Eiffel does not support static data members
|
||
and that might by why destructors do not have postconditions
|
||
in Eiffel). However, in principle there could be uses for destructor
|
||
postconditions so this library supports postconditions for destructors
|
||
(e.g., a class that counts object instances could use destructor
|
||
postconditions to assert that an instance counter stored in a
|
||
static data member is decreased by <code class="computeroutput"><span class="number">1</span></code>
|
||
because the object has been destructed).
|
||
</p></div>
|
||
<div id="ftn.boost_contract.contract_programming_overview.constant_correctness.f0" class="footnote"><p><a href="#boost_contract.contract_programming_overview.constant_correctness.f0" class="para"><sup class="para">[12] </sup></a>
|
||
Note that this is true when using C-style <code class="computeroutput"><span class="identifier">assert</span></code>
|
||
as well.
|
||
</p></div>
|
||
<div id="ftn.boost_contract.contract_programming_overview.specifications_vs__implementation.f0" class="footnote"><p><a href="#boost_contract.contract_programming_overview.specifications_vs__implementation.f0" class="para"><sup class="para">[13] </sup></a>
|
||
<span class="bold"><strong>Rationale:</strong></span> Out of curiosity, if C++ <a href="http://www.open-std.org/jtc1/sc22/wg21/docs/cwg_defects.html#45" target="_top">defect
|
||
45</a> 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++).
|
||
</p></div>
|
||
<div id="ftn.boost_contract.contract_programming_overview.on_contract_failures.f0" class="footnote"><p><a href="#boost_contract.contract_programming_overview.on_contract_failures.f0" class="para"><sup class="para">[14] </sup></a>
|
||
<span class="bold"><strong>Rationale:</strong></span> 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.
|
||
</p></div>
|
||
<div id="ftn.boost_contract.contract_programming_overview.on_contract_failures.f1" class="footnote"><p><a href="#boost_contract.contract_programming_overview.on_contract_failures.f1" class="para"><sup class="para">[15] </sup></a>
|
||
<span class="bold"><strong>Rationale:</strong></span> This customizable failure handling
|
||
mechanism is similar to the one used by C++ <code class="computeroutput"><span class="identifier">std</span><span class="special">::</span><span class="identifier">terminate</span></code>
|
||
and also to the one proposed in <a class="link" href="bibliography.html#N1962_anchor">[N1962]</a>.
|
||
</p></div>
|
||
<div id="ftn.boost_contract.contract_programming_overview.feature_summary.f4" class="footnote">
|
||
<p><a href="#boost_contract.contract_programming_overview.feature_summary.f4" class="para"><sup class="para">[16] </sup></a>
|
||
For example, the following pseudocode attempts to emulate old values
|
||
in <a class="link" href="bibliography.html#P0380_anchor">[P0380]</a>:
|
||
</p>
|
||
<pre class="programlisting"><span class="keyword">struct</span> <span class="identifier">scope_exit</span> <span class="special">{</span> <span class="comment">// RAII.</span>
|
||
<span class="keyword">template</span><span class="special"><</span><span class="keyword">typename</span> <span class="identifier">F</span><span class="special">></span>
|
||
<span class="keyword">explicit</span> <span class="identifier">scope_exit</span><span class="special">(</span><span class="identifier">F</span> <span class="identifier">f</span><span class="special">)</span> <span class="special">:</span> <span class="identifier">f_</span><span class="special">(</span><span class="identifier">f</span><span class="special">)</span> <span class="special">{}</span>
|
||
<span class="special">~</span><span class="identifier">scope_exit</span><span class="special">()</span> <span class="special">{</span> <span class="identifier">f_</span><span class="special">();</span> <span class="special">}</span>
|
||
|
||
<span class="identifier">scope_exit</span><span class="special">(</span><span class="identifier">scope_exit</span> <span class="keyword">const</span><span class="special">&)</span> <span class="special">=</span> <span class="keyword">delete</span><span class="special">;</span>
|
||
<span class="identifier">scope_exit</span><span class="special">&</span> <span class="keyword">operator</span><span class="special">=(</span><span class="identifier">scope_exit</span> <span class="keyword">const</span><span class="special">&)</span> <span class="special">=</span> <span class="keyword">delete</span><span class="special">;</span>
|
||
<span class="keyword">private</span><span class="special">:</span>
|
||
<span class="identifier">std</span><span class="special">::</span><span class="identifier">function</span><span class="special"><</span><span class="keyword">void</span> <span class="special">()></span> <span class="identifier">f_</span><span class="special">;</span>
|
||
<span class="special">};</span>
|
||
|
||
<span class="keyword">void</span> <span class="identifier">fswap</span><span class="special">(</span><span class="identifier">file</span><span class="special">&</span> <span class="identifier">x</span><span class="special">,</span> <span class="identifier">file</span><span class="special">&</span> <span class="identifier">y</span><span class="special">)</span>
|
||
<span class="special">[[</span><span class="identifier">expects</span><span class="special">:</span> <span class="identifier">x</span><span class="special">.</span><span class="identifier">closed</span><span class="special">()]]</span>
|
||
<span class="special">[[</span><span class="identifier">expects</span><span class="special">:</span> <span class="identifier">y</span><span class="special">.</span><span class="identifier">closed</span><span class="special">()]]</span>
|
||
<span class="comment">// Cannot use [[ensures]] for postconditions so to emulate old values.</span>
|
||
<span class="special">{</span>
|
||
<span class="identifier">file</span> <span class="identifier">old_x</span> <span class="special">=</span> <span class="identifier">x</span><span class="special">;</span> <span class="comment">// Emulate old values with local copies (not disabled).</span>
|
||
<span class="identifier">file</span> <span class="identifier">old_y</span> <span class="special">=</span> <span class="identifier">y</span><span class="special">;</span>
|
||
<span class="identifier">scope_exit</span> <span class="identifier">ensures</span><span class="special">([&]</span> <span class="special">{</span> <span class="comment">// Check after local objects destroyed.</span>
|
||
<span class="keyword">if</span><span class="special">(</span><span class="identifier">std</span><span class="special">::</span><span class="identifier">uncaught_exceptions</span><span class="special">()</span> <span class="special">==</span> <span class="number">0</span><span class="special">)</span> <span class="special">{</span> <span class="comment">// Check only if no throw.</span>
|
||
<span class="special">[[</span><span class="identifier">assert</span><span class="special">:</span> <span class="identifier">x</span><span class="special">.</span><span class="identifier">closed</span><span class="special">()]]</span>
|
||
<span class="special">[[</span><span class="identifier">assert</span><span class="special">:</span> <span class="identifier">y</span><span class="special">.</span><span class="identifier">closed</span><span class="special">()]]</span>
|
||
<span class="special">[[</span><span class="identifier">assert</span><span class="special">:</span> <span class="identifier">x</span> <span class="special">==</span> <span class="identifier">old_y</span><span class="special">]]</span>
|
||
<span class="special">[[</span><span class="identifier">assert</span><span class="special">:</span> <span class="identifier">y</span> <span class="special">==</span> <span class="identifier">old_x</span><span class="special">]]</span>
|
||
<span class="special">}</span>
|
||
<span class="special">});</span>
|
||
|
||
<span class="identifier">x</span><span class="special">.</span><span class="identifier">open</span><span class="special">();</span>
|
||
<span class="identifier">scope_exit</span> <span class="identifier">close_x</span><span class="special">([&]</span> <span class="special">{</span> <span class="identifier">x</span><span class="special">.</span><span class="identifier">close</span><span class="special">();</span> <span class="special">});</span>
|
||
<span class="identifier">y</span><span class="special">.</span><span class="identifier">open</span><span class="special">();</span>
|
||
<span class="identifier">scope_exit</span> <span class="identifier">close_y</span><span class="special">([&]</span> <span class="special">{</span> <span class="identifier">y</span><span class="special">.</span><span class="identifier">close</span><span class="special">();</span> <span class="special">});</span>
|
||
<span class="identifier">file</span> <span class="identifier">z</span> <span class="special">=</span> <span class="identifier">file</span><span class="special">::</span><span class="identifier">temp</span><span class="special">();</span>
|
||
<span class="identifier">z</span><span class="special">.</span><span class="identifier">open</span><span class="special">;</span>
|
||
<span class="identifier">scope_exit</span> <span class="identifier">close_z</span><span class="special">([&]</span> <span class="special">{</span> <span class="identifier">z</span><span class="special">.</span><span class="identifier">close</span><span class="special">();</span> <span class="special">});</span>
|
||
|
||
<span class="identifier">x</span><span class="special">.</span><span class="identifier">mv</span><span class="special">(</span><span class="identifier">z</span><span class="special">);</span>
|
||
<span class="identifier">y</span><span class="special">.</span><span class="identifier">mv</span><span class="special">(</span><span class="identifier">x</span><span class="special">);</span>
|
||
<span class="identifier">z</span><span class="special">.</span><span class="identifier">mv</span><span class="special">(</span><span class="identifier">y</span><span class="special">);</span>
|
||
<span class="special">}</span>
|
||
</pre>
|
||
<p>
|
||
This requires boiler-plate code to make sure postconditions are correctly
|
||
checked only if the function did not throw an exception and in a <code class="computeroutput"><span class="identifier">scope_exit</span></code> 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, this would require adding even more boiler-plate code using
|
||
<code class="computeroutput"><span class="preprocessor">#ifdef</span></code>, etc.).
|
||
</p>
|
||
</div>
|
||
<div id="ftn.boost_contract.contract_programming_overview.feature_summary.f5" class="footnote">
|
||
<p><a href="#boost_contract.contract_programming_overview.feature_summary.f5" class="para"><sup class="para">[17] </sup></a>
|
||
For example, the following pseudocode attempts to emulation of class
|
||
invariants in <a class="link" href="bibliography.html#P0380_anchor">[P0380]</a>:
|
||
</p>
|
||
<pre class="programlisting"><span class="keyword">template</span><span class="special"><</span><span class="keyword">typename</span> <span class="identifier">T</span><span class="special">></span>
|
||
<span class="keyword">class</span> <span class="identifier">vector</span> <span class="special">{</span>
|
||
<span class="keyword">bool</span> <span class="identifier">invariant</span><span class="special">()</span> <span class="keyword">const</span> <span class="special">{</span> <span class="comment">// Check invariants at...</span>
|
||
<span class="special">[[</span><span class="identifier">assert</span><span class="special">:</span> <span class="identifier">empty</span><span class="special">()</span> <span class="special">==</span> <span class="special">(</span><span class="identifier">size</span><span class="special">()</span> <span class="special">==</span> <span class="number">0</span><span class="special">)]]</span>
|
||
<span class="special">[[</span><span class="identifier">assert</span><span class="special">:</span> <span class="identifier">size</span><span class="special">()</span> <span class="special"><=</span> <span class="identifier">capacity</span><span class="special">()]]</span>
|
||
<span class="keyword">return</span> <span class="keyword">true</span><span class="special">;</span>
|
||
<span class="special">}</span>
|
||
|
||
<span class="keyword">public</span><span class="special">:</span>
|
||
<span class="identifier">vector</span><span class="special">()</span>
|
||
<span class="special">[[</span><span class="identifier">ensures</span><span class="special">:</span> <span class="identifier">invariant</span><span class="special">()]]</span> <span class="comment">// ...constructor exit (only if no throw).</span>
|
||
<span class="special">{</span> <span class="special">...</span> <span class="special">}</span>
|
||
|
||
<span class="special">~</span><span class="identifier">vector</span><span class="special">()</span> <span class="keyword">noexcept</span>
|
||
<span class="special">[[</span><span class="identifier">expects</span><span class="special">:</span> <span class="identifier">invariant</span><span class="special">()]]</span> <span class="comment">// ...destructor entry.</span>
|
||
<span class="special">{</span> <span class="special">...</span> <span class="special">}</span>
|
||
|
||
<span class="keyword">void</span> <span class="identifier">push_back</span><span class="special">(</span><span class="identifier">T</span> <span class="keyword">const</span><span class="special">&</span> <span class="identifier">value</span><span class="special">)</span>
|
||
<span class="special">[[</span><span class="identifier">expects</span><span class="special">:</span> <span class="identifier">invariant</span><span class="special">()]]</span> <span class="comment">// ...public function entry.</span>
|
||
<span class="special">[[</span><span class="identifier">ensures</span><span class="special">:</span> <span class="identifier">invariant</span><span class="special">()]]</span> <span class="comment">// ...public function exit (if no throw).</span>
|
||
<span class="keyword">try</span> <span class="special">{</span>
|
||
<span class="special">...</span> <span class="comment">// Function body.</span>
|
||
<span class="special">}</span> <span class="keyword">catch</span><span class="special">(...)</span> <span class="special">{</span>
|
||
<span class="identifier">invariant</span><span class="special">();</span> <span class="comment">// ...public function exit (if throw).</span>
|
||
<span class="keyword">throw</span><span class="special">;</span>
|
||
<span class="special">}</span>
|
||
|
||
<span class="special">...</span>
|
||
<span class="special">};</span>
|
||
</pre>
|
||
<p>
|
||
This 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). In case the destructor can throw (e.g., it is declared <code class="computeroutput"><span class="keyword">noexcept</span><span class="special">(</span><span class="keyword">false</span><span class="special">)</span></code>),
|
||
the destructor also requires a <code class="computeroutput"><span class="keyword">try</span><span class="special">-</span><span class="keyword">catch</span></code>
|
||
statement similar to the one programmed for <code class="computeroutput"><span class="identifier">push_back</span></code>
|
||
to check class invariants at destructor exit when it throws exceptions.
|
||
Still, an outstanding issue remains to avoid infinite recursion if
|
||
also <code class="computeroutput"><span class="identifier">empty</span></code> and <code class="computeroutput"><span class="identifier">size</span></code> are public functions programmed
|
||
to check class invariants (because <a class="link" href="bibliography.html#P0380_anchor">[P0380]</a>
|
||
does not automatically disable assertions while checking other assertions).
|
||
</p>
|
||
</div>
|
||
<div id="ftn.boost_contract.contract_programming_overview.feature_summary.f6" class="footnote"><p><a href="#boost_contract.contract_programming_overview.feature_summary.f6" class="para"><sup class="para">[18] </sup></a>
|
||
For example, it is not really possible to sketch pseudocode based on
|
||
<a class="link" href="bibliography.html#P0380_anchor">[P0380]</a> that emulates subcontracting
|
||
in the general case.
|
||
</p></div>
|
||
</div>
|
||
</div>
|
||
<table xmlns:rev="http://www.cs.rpi.edu/~gregod/boost/tools/doc/revision" width="100%"><tr>
|
||
<td align="left"></td>
|
||
<td align="right"><div class="copyright-footer">Copyright © 2008-2019 Lorenzo Caminiti<p>
|
||
Distributed under the Boost Software License, Version 1.0 (see accompanying
|
||
file LICENSE_1_0.txt or a copy at <a href="http://www.boost.org/LICENSE_1_0.txt" target="_top">http://www.boost.org/LICENSE_1_0.txt</a>)
|
||
</p>
|
||
</div></td>
|
||
</tr></table>
|
||
<hr>
|
||
<div class="spirit-nav">
|
||
<a accesskey="p" href="getting_started.html"><img src="../../../../../doc/src/images/prev.png" alt="Prev"></a><a accesskey="u" href="../index.html"><img src="../../../../../doc/src/images/up.png" alt="Up"></a><a accesskey="h" href="../index.html"><img src="../../../../../doc/src/images/home.png" alt="Home"></a><a accesskey="n" href="tutorial.html"><img src="../../../../../doc/src/images/next.png" alt="Next"></a>
|
||
</div>
|
||
</body>
|
||
</html>
|