contract_programming_overview.html 130 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686687688689690691692693694695696697698699700701702703704705706707708709710711712713714715716717718719720721722723724725726727728729730731732733734735736737738739740741742743744745746747748749750751752753754755756757758759760761762763764765766767768769770771772773774775776777778779780781782783784785786787788789790791792793794795796797798799800801802803804805806807808809810811812813814815816817818819820821822823824825826827828829830831832833834835836837838839840841842843844845846847848849850851852853854855856857858859860861862863864865866867868869870871872873874875876877878879880881882883884885886887888889890891892893894895896897898899900901902903904905906907908909910911912913914915916917918919920921922923924925926927928929930931932933934935936937938939940941942943944945946947948949950951952953954955956957958959960961962963964965966967968969970971972973974975976977978979980981982983984985986987988989990991992993994995996997998999100010011002100310041005100610071008100910101011101210131014101510161017101810191020102110221023102410251026102710281029103010311032103310341035103610371038103910401041104210431044104510461047104810491050105110521053105410551056105710581059106010611062106310641065106610671068106910701071107210731074107510761077107810791080108110821083108410851086108710881089109010911092109310941095109610971098109911001101110211031104110511061107110811091110111111121113111411151116111711181119112011211122112311241125112611271128112911301131113211331134113511361137113811391140114111421143114411451146114711481149115011511152115311541155115611571158115911601161116211631164116511661167116811691170117111721173117411751176117711781179118011811182118311841185118611871188118911901191119211931194119511961197119811991200120112021203120412051206120712081209121012111212121312141215121612171218121912201221122212231224122512261227122812291230123112321233123412351236123712381239124012411242124312441245124612471248124912501251125212531254125512561257125812591260126112621263126412651266126712681269127012711272127312741275127612771278127912801281128212831284128512861287128812891290129112921293129412951296129712981299130013011302130313041305130613071308130913101311131213131314131513161317131813191320132113221323132413251326132713281329133013311332133313341335133613371338133913401341134213431344134513461347134813491350135113521353135413551356135713581359136013611362136313641365136613671368136913701371137213731374137513761377137813791380138113821383138413851386138713881389139013911392139313941395139613971398139914001401140214031404140514061407140814091410141114121413141414151416141714181419142014211422142314241425142614271428142914301431143214331434143514361437143814391440144114421443144414451446144714481449145014511452145314541455145614571458145914601461146214631464146514661467146814691470147114721473147414751476147714781479148014811482148314841485148614871488148914901491149214931494149514961497149814991500150115021503150415051506150715081509151015111512151315141515151615171518151915201521152215231524152515261527152815291530153115321533153415351536153715381539154015411542154315441545154615471548154915501551155215531554155515561557155815591560156115621563156415651566156715681569157015711572157315741575157615771578157915801581158215831584158515861587158815891590159115921593159415951596159715981599160016011602160316041605160616071608160916101611161216131614161516161617161816191620162116221623162416251626162716281629163016311632163316341635163616371638163916401641164216431644164516461647164816491650165116521653165416551656165716581659166016611662166316641665166616671668166916701671167216731674167516761677167816791680168116821683168416851686168716881689169016911692169316941695169616971698169917001701170217031704170517061707170817091710171117121713171417151716171717181719172017211722172317241725172617271728172917301731173217331734173517361737173817391740174117421743174417451746174717481749175017511752175317541755175617571758175917601761176217631764176517661767176817691770177117721773177417751776177717781779178017811782178317841785178617871788178917901791179217931794179517961797179817991800180118021803180418051806180718081809181018111812181318141815181618171818181918201821182218231824182518261827182818291830183118321833183418351836183718381839184018411842184318441845184618471848184918501851185218531854185518561857185818591860186118621863186418651866186718681869187018711872187318741875187618771878187918801881188218831884188518861887188818891890189118921893189418951896189718981899190019011902190319041905190619071908190919101911191219131914191519161917191819191920192119221923192419251926192719281929193019311932193319341935193619371938193919401941194219431944194519461947194819491950195119521953195419551956195719581959196019611962196319641965196619671968196919701971197219731974197519761977197819791980198119821983198419851986198719881989199019911992199319941995199619971998199920002001200220032004200520062007200820092010201120122013201420152016201720182019202020212022202320242025202620272028202920302031203220332034203520362037203820392040204120422043204420452046204720482049205020512052205320542055205620572058205920602061206220632064206520662067206820692070207120722073207420752076207720782079208020812082208320842085208620872088208920902091209220932094209520962097209820992100210121022103210421052106210721082109211021112112211321142115211621172118211921202121212221232124212521262127212821292130213121322133213421352136213721382139214021412142214321442145
  1. <html>
  2. <head>
  3. <meta http-equiv="Content-Type" content="text/html; charset=US-ASCII">
  4. <title>Contract Programming Overview</title>
  5. <link rel="stylesheet" href="../../../../../doc/src/boostbook.css" type="text/css">
  6. <meta name="generator" content="DocBook XSL Stylesheets V1.79.1">
  7. <link rel="home" href="../index.html" title="Chapter&#160;1.&#160;Boost.Contract 1.0.0">
  8. <link rel="up" href="../index.html" title="Chapter&#160;1.&#160;Boost.Contract 1.0.0">
  9. <link rel="prev" href="getting_started.html" title="Getting Started">
  10. <link rel="next" href="tutorial.html" title="Tutorial">
  11. </head>
  12. <body bgcolor="white" text="black" link="#0000FF" vlink="#840084" alink="#0000FF">
  13. <table cellpadding="2" width="100%"><tr>
  14. <td valign="top"><img alt="Boost C++ Libraries" width="277" height="86" src="../../../../../boost.png"></td>
  15. <td align="center"><a href="../../../../../index.html">Home</a></td>
  16. <td align="center"><a href="../../../../../libs/libraries.htm">Libraries</a></td>
  17. <td align="center"><a href="http://www.boost.org/users/people.html">People</a></td>
  18. <td align="center"><a href="http://www.boost.org/users/faq.html">FAQ</a></td>
  19. <td align="center"><a href="../../../../../more/index.htm">More</a></td>
  20. </tr></table>
  21. <hr>
  22. <div class="spirit-nav">
  23. <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>
  24. </div>
  25. <div class="section">
  26. <div class="titlepage"><div><div><h2 class="title" style="clear: both">
  27. <a name="boost_contract.contract_programming_overview"></a><a class="link" href="contract_programming_overview.html" title="Contract Programming Overview">Contract
  28. Programming Overview</a>
  29. </h2></div></div></div>
  30. <div class="toc"><dl class="toc">
  31. <dt><span class="section"><a href="contract_programming_overview.html#boost_contract.contract_programming_overview.assertions">Assertions</a></span></dt>
  32. <dt><span class="section"><a href="contract_programming_overview.html#boost_contract.contract_programming_overview.benefits_and_costs">Benefits
  33. and Costs</a></span></dt>
  34. <dt><span class="section"><a href="contract_programming_overview.html#boost_contract.contract_programming_overview.function_calls">Function
  35. Calls</a></span></dt>
  36. <dt><span class="section"><a href="contract_programming_overview.html#boost_contract.contract_programming_overview.public_function_calls">Public
  37. Function Calls</a></span></dt>
  38. <dt><span class="section"><a href="contract_programming_overview.html#boost_contract.contract_programming_overview.constructor_calls">Constructor
  39. Calls</a></span></dt>
  40. <dt><span class="section"><a href="contract_programming_overview.html#boost_contract.contract_programming_overview.destructor_calls">Destructor
  41. Calls</a></span></dt>
  42. <dt><span class="section"><a href="contract_programming_overview.html#boost_contract.contract_programming_overview.constant_correctness">Constant-Correctness</a></span></dt>
  43. <dt><span class="section"><a href="contract_programming_overview.html#boost_contract.contract_programming_overview.specifications_vs__implementation">Specifications
  44. vs. Implementation</a></span></dt>
  45. <dt><span class="section"><a href="contract_programming_overview.html#boost_contract.contract_programming_overview.on_contract_failures">On
  46. Contract Failures</a></span></dt>
  47. <dt><span class="section"><a href="contract_programming_overview.html#boost_contract.contract_programming_overview.feature_summary">Feature
  48. Summary</a></span></dt>
  49. </dl></div>
  50. <div class="blockquote"><blockquote class="blockquote"><p>
  51. <span class="emphasis"><em><span class="quote">&#8220;<span class="quote">It is absurd to make elaborate security checks on debugging
  52. runs, when no trust is put in the results, and then remove them in production
  53. runs, when an erroneous result could be expensive or disastrous. What would
  54. we think of a sailing enthusiast who wears his life-jacket when training
  55. on dry land but takes it off as soon as he goes to sea?</span>&#8221;</span></em></span>
  56. </p></blockquote></div>
  57. <div class="blockquote"><blockquote class="blockquote"><p>
  58. <span class="emphasis"><em>-- Charles Antony Richard Hoare (see <a class="link" href="bibliography.html#Hoare73_anchor">[Hoare73]</a>)</em></span>
  59. </p></blockquote></div>
  60. <p>
  61. This section gives an overview of contract programming (see <a class="link" href="bibliography.html#Meyer97_anchor">[Meyer97]</a>,
  62. <a class="link" href="bibliography.html#Mitchell02_anchor">[Mitchell02]</a>, and <a class="link" href="bibliography.html#N1613_anchor">[N1613]</a>
  63. for more extensive introductions to contract programming). Readers that already
  64. have a basic understanding of contract programming can skip this section and
  65. maybe come back to it after reading the <a class="link" href="tutorial.html" title="Tutorial">Tutorial</a>.
  66. </p>
  67. <div class="note"><table border="0" summary="Note">
  68. <tr>
  69. <td rowspan="2" align="center" valign="top" width="25"><img alt="[Note]" src="../../../../../doc/src/images/note.png"></td>
  70. <th align="left">Note</th>
  71. </tr>
  72. <tr><td align="left" valign="top"><p>
  73. The objective of this library is not to convince programmers to use contract
  74. programming. It is assumed that programmes understand the benefits and trade-offs
  75. associated with contract programming and they have already decided to use
  76. this methodology in their code. Then, this library aims to be the best and
  77. more complete contract programming library for C++ (without using programs
  78. and tools external to the C++ language and its preprocessor).
  79. </p></td></tr>
  80. </table></div>
  81. <div class="section">
  82. <div class="titlepage"><div><div><h3 class="title">
  83. <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>
  84. </h3></div></div></div>
  85. <p>
  86. Contract programming is characterized by the following assertion mechanisms:
  87. </p>
  88. <div class="itemizedlist"><ul class="itemizedlist" style="list-style-type: disc; ">
  89. <li class="listitem">
  90. <span class="emphasis"><em>Preconditions</em></span>: These are logical conditions that
  91. programmers expect to be true when a function is called (e.g., to check
  92. constraints on function arguments). Operations that logically have no
  93. preconditions (i.e., that are always well-defined for the entire domain
  94. of their inputs) are also referred to as having a <span class="emphasis"><em>wide contract</em></span>.
  95. This is in contrast to operations that have preconditions which are also
  96. referred to as having a <span class="emphasis"><em>narrow contract</em></span> (note that
  97. operations with truly narrow contracts are also expected to never throw
  98. exceptions because the implementation body of these operations is always
  99. expected to succeed after its preconditions are checked to be true).
  100. <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>
  101. </li>
  102. <li class="listitem">
  103. <span class="emphasis"><em>Postconditions</em></span>: These are logical conditions that
  104. programmers expect to be true when a function exits without throwing
  105. an exception (e.g., to check the result and any side effect that a function
  106. might have). Postconditions can access the function return value (for
  107. non-void functions) and also <span class="emphasis"><em>old values</em></span> (which are
  108. the values that expressions had before the function implementation was
  109. executed).
  110. </li>
  111. <li class="listitem">
  112. <span class="emphasis"><em>Exception guarantees</em></span>: These are logical conditions
  113. that programmers except to be true when a function exits throwing an
  114. exception. Exception guarantees can access old values (but not the function
  115. 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>
  116. </li>
  117. <li class="listitem">
  118. <span class="emphasis"><em>Class invariants</em></span>: These are logical conditions that
  119. programmers expect to be true after a constructor exits without throwing
  120. an exception, before and after the execution of every non-static public
  121. function (even if they throw exceptions), before the destructor is executed
  122. (and also after the destructor is executed but only when the destructor
  123. throws an exception). Class invariants define valid states for all objects
  124. of a given class. It is possible to specify a different set of class
  125. invariants for volatile public functions, namely <span class="emphasis"><em>volatile class
  126. invariants</em></span>. It is also possible to specify <span class="emphasis"><em>static
  127. class invariants</em></span> which are excepted to be true before and
  128. after the execution of any constructor, destructor (even if it does not
  129. 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>
  130. </li>
  131. <li class="listitem">
  132. <span class="emphasis"><em>Subcontracting</em></span>: This indicates that preconditions
  133. cannot be strengthen, while postconditions and class invariants cannot
  134. be weaken when a public function in a derived class overrides public
  135. functions in one or more of its base classes (this is formally defined
  136. according to the <a href="http://en.wikipedia.org/wiki/Liskov_substitution_principle" target="_top">substitution
  137. principle</a>).
  138. </li>
  139. </ul></div>
  140. <p>
  141. The actual function implementation code, that remains outside of these contract
  142. assertions, is often referred to as the <span class="emphasis"><em>function body</em></span>
  143. in contract programming.
  144. </p>
  145. <p>
  146. Class invariants can also be used to specify <span class="emphasis"><em>basic</em></span> exception
  147. safety guarantees for an object (because they are checked at exit of public
  148. functions even when those throw exceptions). Contract assertions for exception
  149. guarantees can be used to specify <span class="emphasis"><em>strong</em></span> exception safety
  150. guarantees for a given operation on the same object.
  151. </p>
  152. <p>
  153. It is also a common requirement for contract programming to automatically
  154. disable contract checking while already checking assertions from another
  155. contract (in order to avoid infinite recursion while checking contract assertions).
  156. </p>
  157. <div class="note"><table border="0" summary="Note">
  158. <tr>
  159. <td rowspan="2" align="center" valign="top" width="25"><img alt="[Note]" src="../../../../../doc/src/images/note.png"></td>
  160. <th align="left">Note</th>
  161. </tr>
  162. <tr><td align="left" valign="top"><p>
  163. This library implements this requirement but in order to globally disable
  164. assertions while checking another assertion some kind of global arbitrating
  165. variable needs to be used by this library implementation. This library
  166. will automatically protect such a global variable from race conditions
  167. in multi-threated programs, but this will effectively introduce a global
  168. lock in the program (the <code class="computeroutput"><a class="link" href="../BOOST_CO_idm45394999743888.html" title="Macro BOOST_CONTRACT_DISABLE_THREADS">BOOST_CONTRACT_DISABLE_THREADS</a></code>
  169. macro can be defined to disable this global lock but at the risk of incurring
  170. 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>
  171. </p></td></tr>
  172. </table></div>
  173. <p>
  174. In general, it is recommended to specify different contract conditions using
  175. separate assertion statements and not to group them together into a single
  176. condition using logical operators (<code class="computeroutput"><span class="special">&amp;&amp;</span></code>,
  177. <code class="computeroutput"><span class="special">||</span></code>, etc.). This is because when
  178. contract conditions are programmed together in a single assertion using logical
  179. operators, it might not be clear which condition actually failed in case
  180. the entire assertion fails at run-time.
  181. </p>
  182. <h5>
  183. <a name="boost_contract.contract_programming_overview.assertions.h0"></a>
  184. <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
  185. Assertions</a>
  186. </h5>
  187. <p>
  188. A limited form of contract programming (typically some form of precondition
  189. 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>
  190. is common practice for many programmers but it suffers of the following limitations:
  191. </p>
  192. <div class="itemizedlist"><ul class="itemizedlist" style="list-style-type: disc; ">
  193. <li class="listitem">
  194. <code class="computeroutput"><span class="identifier">assert</span></code> does not distinguish
  195. between preconditions and postconditions. In well-tested production code,
  196. postconditions can usually be disabled trusting the correctness of the
  197. implementation while preconditions might still need to remain enabled
  198. because of possible changes in the calling code (e.g., postconditions
  199. of a given library could be disabled after testing while keeping the
  200. library preconditions enabled given that future changes in the user code
  201. that calls the library cannot be anticipated). Using <code class="computeroutput"><span class="identifier">assert</span></code>
  202. it is not possible to selectively disable only postconditions and all
  203. assertions must be disabled at once.
  204. </li>
  205. <li class="listitem">
  206. <code class="computeroutput"><span class="identifier">assert</span></code> requires to manually
  207. program extra code to correctly check postconditions (specifically to
  208. handle functions with multiple return statements, to not check postconditions
  209. when functions throw exceptions, and to implement old values).
  210. </li>
  211. <li class="listitem">
  212. <code class="computeroutput"><span class="identifier">assert</span></code> requires to manually
  213. program extra code to check class invariants (extra member functions,
  214. try blocks, etc.).
  215. </li>
  216. <li class="listitem">
  217. <code class="computeroutput"><span class="identifier">assert</span></code> does not support
  218. subcontracting.
  219. </li>
  220. <li class="listitem">
  221. <code class="computeroutput"><span class="identifier">assert</span></code> calls are usually
  222. scattered within function implementations thus the asserted conditions
  223. are not immediately visible in their entirety by programmers (as they
  224. are instead when the assertions appear in the function declaration or
  225. at least at the very top of the function definition).
  226. </li>
  227. </ul></div>
  228. <p>
  229. Contract programming does not suffer of these limitations.
  230. </p>
  231. </div>
  232. <div class="section">
  233. <div class="titlepage"><div><div><h3 class="title">
  234. <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
  235. and Costs</a>
  236. </h3></div></div></div>
  237. <h5>
  238. <a name="boost_contract.contract_programming_overview.benefits_and_costs.h0"></a>
  239. <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>
  240. </h5>
  241. <p>
  242. 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
  243. can be used as the basic tool to write <span class="quote">&#8220;<span class="quote">correct</span>&#8221;</span> software.
  244. <a class="link" href="bibliography.html#Stroustrup94_anchor">[Stroustrup94]</a> discusses the key
  245. importance of class invariants plus advantages and disadvantages of preconditions
  246. and postconditions.
  247. </p>
  248. <p>
  249. The following is a short summary of benefits associated with contract programming
  250. inspired mainly by <a class="link" href="bibliography.html#N1613_anchor">[N1613]</a>:
  251. </p>
  252. <div class="itemizedlist"><ul class="itemizedlist" style="list-style-type: disc; ">
  253. <li class="listitem">
  254. Preconditions and postconditions: Using function preconditions and postconditions,
  255. programmers can give a precise semantic description of what a function
  256. requires at its entry and what it ensures at its exit (if it does not
  257. throw an exception). In particular, using postcondition old values, contract
  258. programming provides a mechanism that allows programmers to compare values
  259. of an expression before and after the function body execution. This mechanism
  260. is powerful enough to enable programmers to express many correctness
  261. constraints within the code itself, constraints that would otherwise
  262. have to be captured at best only informally by documentation.
  263. </li>
  264. <li class="listitem">
  265. Class invariants: Using class invariants, programmers can describe what
  266. to expect from a class and the logic dependencies between the class members.
  267. It is the job of the constructor to ensure that the class invariants
  268. are satisfied when the object is first created. Then the implementation
  269. of the member functions can be largely simplified as they can be written
  270. knowing that the class invariants are satisfied because contract programming
  271. checks them before and after the execution of every public function.
  272. Finally, the destructor makes sure that the class invariants held for
  273. the entire life of the object checking the class invariants one last
  274. time before the object is destructed. Class invariants can also be used
  275. as a criteria for good abstractions: If it is not possible to specify
  276. an invariant, it might be an indication that the design abstraction maybe
  277. be poor and it should not have been made into a class (maybe a namespace
  278. would have sufficed instead).
  279. </li>
  280. <li class="listitem">
  281. Self-documenting code: Contracts are part of the source code, they are
  282. checked at run-time so they are always up-to-date with the code itself.
  283. Therefore program specifications, as documented by the contracts, can
  284. be trusted to always be up-to-date with the implementation.
  285. </li>
  286. <li class="listitem">
  287. Easier debugging: Contract programming can provide a powerful debugging
  288. facility because, if contracts are well-written, bugs will cause contract
  289. assertions to fail exactly where the problem first occurs instead than
  290. at some later stage of the program execution in an apparently unrelated
  291. (and often hard to debug) manner. Note that a precondition failure points
  292. to a bug in the function caller, a postcondition failure points instead
  293. 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>
  294. </li>
  295. <li class="listitem">
  296. Easier testing: Contract programming facilitates testing because a contract
  297. naturally specifies what a test should check. For example, preconditions
  298. of a function state which inputs cause the function to fail and postconditions
  299. state which outputs are produced by the function on successful exit (contract
  300. programming should be seen as a tool to complement and guide, but obviously
  301. not to replace, testing).
  302. </li>
  303. <li class="listitem">
  304. Formal design: Contract programming can serve to reduce the gap between
  305. designers and programmers by providing a precise and unambiguous specification
  306. language in terms of contract assertions. Moreover, contracts can make
  307. code reviews easier by clarifying some of the semantics and usage of
  308. the code.
  309. </li>
  310. <li class="listitem">
  311. Formalize inheritance: Contract programming formalizes the virtual function
  312. overriding mechanism using subcontracting as justified by the <a href="http://en.wikipedia.org/wiki/Liskov_substitution_principle" target="_top">substitution
  313. principle</a>. This keeps the base class programmers in control as
  314. overriding functions always have to fully satisfy the contracts of their
  315. base classes.
  316. </li>
  317. <li class="listitem">
  318. Replace defensive programming: Contract programming assertions can replace
  319. <a href="http://en.wikipedia.org/wiki/Defensive_programming" target="_top">defensive
  320. programming</a> checks localizing these checks within the contracts
  321. and making the code more readable.
  322. </li>
  323. </ul></div>
  324. <p>
  325. Of course, not all formal contract specifications can be asserted in C++.
  326. For example, in C++ is it not possible to assert the validity of an iterator
  327. range in the general case (because the only way to check if two iterators
  328. form a valid range is to keep incrementing the first iterator until it reaches
  329. the second iterator, but if the iterator range is invalid then such a code
  330. would render undefined behaviour or run forever instead of failing an assertion).
  331. Nevertheless, a large amount of contract assertions can be successfully programmed
  332. in C++ as illustrated by the numerous examples in this documentation and
  333. 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
  334. be programmed in C++ using this library).
  335. </p>
  336. <h5>
  337. <a name="boost_contract.contract_programming_overview.benefits_and_costs.h1"></a>
  338. <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>
  339. </h5>
  340. <p>
  341. In general, contract programming benefits come at the cost of performance
  342. as discussed in detail by both <a class="link" href="bibliography.html#Stroustrup94_anchor">[Stroustrup94]</a>
  343. and <a class="link" href="bibliography.html#Meyer97_anchor">[Meyer97]</a>. While performance trade-offs
  344. should be carefully considered depending on the specific application domain,
  345. software quality cannot be sacrificed: It is difficult to see value in software
  346. that quickly and efficiently provides incorrect results.
  347. </p>
  348. <p>
  349. The run-time performances are negatively impacted by contract programming
  350. mainly because of extra time require to:
  351. </p>
  352. <div class="itemizedlist"><ul class="itemizedlist" style="list-style-type: disc; ">
  353. <li class="listitem">
  354. Check the asserted conditions.
  355. </li>
  356. <li class="listitem">
  357. Copy old values when these are used in postconditions or exception guarantees.
  358. </li>
  359. <li class="listitem">
  360. Call additional functors that check preconditions, postconditions, exception
  361. guarantees, class invariants, etc. (these can add up to many extra calls
  362. especially when using subcontracting).
  363. </li>
  364. </ul></div>
  365. <div class="note"><table border="0" summary="Note">
  366. <tr>
  367. <td rowspan="2" align="center" valign="top" width="25"><img alt="[Note]" src="../../../../../doc/src/images/note.png"></td>
  368. <th align="left">Note</th>
  369. </tr>
  370. <tr><td align="left" valign="top"><p>
  371. In general, contracts introduce at least three extra functor calls to check
  372. preconditions, postconditions, and exception guarantees for any given non-member
  373. function call. Public functions introduce also two more function calls
  374. to check class invariants (at entry and at exit). For subcontracting, these
  375. extra calls (some of which become virtual calls) are repeated for the number
  376. of functions being overridden from the base classes (possibly deep in the
  377. inheritance tree). In addition to that, this library introduces a number
  378. of function calls internal to its implementation in order to properly check
  379. the contracts.
  380. </p></td></tr>
  381. </table></div>
  382. <p>
  383. To mitigate the run-time performance impact, programmers can selectively
  384. disable run-time checking of some of the contract assertions. Programmers
  385. will have to decide based on the performance trade-offs required by their
  386. 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
  387. Contract Checking</a>):
  388. </p>
  389. <div class="itemizedlist"><ul class="itemizedlist" style="list-style-type: disc; ">
  390. <li class="listitem">
  391. Always write contracts to clarify the semantics of the design embedding
  392. the specifications directly in the code and making the code self-documenting.
  393. </li>
  394. <li class="listitem">
  395. Check preconditions, postconditions, class invariants, and maybe even
  396. exception guarantees during initial testing.
  397. </li>
  398. <li class="listitem">
  399. Check only preconditions (and maybe class invariants, but not postconditions
  400. and exception guarantees) during release testing and for the final release.
  401. </li>
  402. </ul></div>
  403. <p>
  404. This approach is usually reasonable because in well-tested production code,
  405. validating the function body implementation using postconditions is rarely
  406. needed since the function has shown itself to be <span class="quote">&#8220;<span class="quote">correct</span>&#8221;</span> during
  407. testing. On the other hand, checking function arguments using preconditions
  408. is always needed because of changes that can be made to the calling code
  409. (without having to necessarily re-test and re-release the called code). Furthermore,
  410. postconditions and also exception guarantees, with related old value copies,
  411. are often computationally more expensive to check than preconditions and
  412. class invariants.
  413. </p>
  414. </div>
  415. <div class="section">
  416. <div class="titlepage"><div><div><h3 class="title">
  417. <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
  418. Calls</a>
  419. </h3></div></div></div>
  420. <h5>
  421. <a name="boost_contract.contract_programming_overview.function_calls.h0"></a>
  422. <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
  423. Functions</a>
  424. </h5>
  425. <p>
  426. A call to a non-member function with a contract executes the following steps
  427. (see <code class="computeroutput"><a class="link" href="../boost/contract/function.html" title="Function function">boost::contract::function</a></code>):
  428. </p>
  429. <div class="orderedlist"><ol class="orderedlist" type="1">
  430. <li class="listitem">
  431. Check function preconditions.
  432. </li>
  433. <li class="listitem">
  434. Execute the function body.
  435. </li>
  436. <li class="listitem">
  437. If the body did not throw an exception, check function postconditions.
  438. </li>
  439. <li class="listitem">
  440. Else, check function exception guarantees.
  441. </li>
  442. </ol></div>
  443. <h5>
  444. <a name="boost_contract.contract_programming_overview.function_calls.h1"></a>
  445. <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
  446. and Protected Functions</a>
  447. </h5>
  448. <p>
  449. Private and protected functions do not have to satisfy class invariants because
  450. these functions are part of the class implementation and not of the class
  451. public interface. Furthermore, the <a href="http://en.wikipedia.org/wiki/Liskov_substitution_principle" target="_top">substitution
  452. principle</a> does not apply to private and protected functions because
  453. these functions are not accessible to the user at the calling site where
  454. the <a href="http://en.wikipedia.org/wiki/Liskov_substitution_principle" target="_top">substitution
  455. principle</a> applies.
  456. </p>
  457. <p>
  458. Therefore, calls to private and protected functions with contracts execute
  459. the same steps as the ones indicated above for non-member functions (checking
  460. only preconditions and postconditions, without checking class invariants
  461. and without subcontracting).
  462. </p>
  463. </div>
  464. <div class="section">
  465. <div class="titlepage"><div><div><h3 class="title">
  466. <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
  467. Function Calls</a>
  468. </h3></div></div></div>
  469. <h5>
  470. <a name="boost_contract.contract_programming_overview.public_function_calls.h0"></a>
  471. <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
  472. Public Functions</a>
  473. </h5>
  474. <p>
  475. Let's consider a public function in a derived class that overrides public
  476. virtual functions declared by its public base classes (because of C++ multiple
  477. inheritance, the function could override from more than one of its base classes).
  478. We refer to the function in the derived class as the <span class="emphasis"><em>overriding
  479. function</em></span>, and to the set of base classes containing all the <span class="emphasis"><em>overridden
  480. functions</em></span> as <span class="emphasis"><em>overridden bases</em></span>.
  481. </p>
  482. <p>
  483. When subcontracting, overridden functions are searched (at compile-time)
  484. deeply in all public branches of the inheritance tree (i.e., not just the
  485. derived class' direct public parents are inspected, but also all its public
  486. grandparents, etc.). In case of multiple inheritance, this search also extends
  487. (at compile-time) widely to all public trees of the multiple inheritance
  488. forest (multiple public base classes are searched following their order of
  489. declaration in the derived class' inheritance list). As usual with C++ multiple
  490. inheritance, this search could result in multiple overridden functions and
  491. therefore in subcontracting from multiple public base classes. Note that
  492. only public base classes are considered for subcontracting because private
  493. and protected base classes are not accessible to the user at the calling
  494. site where the <a href="http://en.wikipedia.org/wiki/Liskov_substitution_principle" target="_top">substitution
  495. principle</a> applies.
  496. </p>
  497. <p>
  498. A call to the overriding public function with a contract executes the following
  499. steps (see <code class="computeroutput"><a class="link" href="../boost/contract/public_f_idm45394998885120.html" title="Function template public_function">boost::contract::public_function</a></code>):
  500. </p>
  501. <div class="orderedlist"><ol class="orderedlist" type="1">
  502. <li class="listitem">
  503. 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>
  504. 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>
  505. 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>
  506. non-static invariants.
  507. </li>
  508. <li class="listitem">
  509. Check preconditions of overridden public functions from all overridden
  510. bases in <a class="link" href="contract_programming_overview.html#or_anchor"><code class="literal"><span class="emphasis"><em>OR</em></span></code></a>
  511. 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>
  512. else check the overriding function preconditions in the derived class.
  513. </li>
  514. <li class="listitem">
  515. Execute the overriding function body.
  516. </li>
  517. <li class="listitem">
  518. 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>
  519. 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>
  520. 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>
  521. non-static invariants (even if the body threw an exception).
  522. </li>
  523. <li class="listitem">
  524. If the body did not throw an exception, check postconditions of overridden
  525. 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>
  526. 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>
  527. then check the overriding function postconditions in the derived class.
  528. </li>
  529. <li class="listitem">
  530. Else, check exception guarantees of overridden public functions from
  531. 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>
  532. 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>
  533. then check the overriding function exception guarantees in the derived
  534. class.
  535. </li>
  536. </ol></div>
  537. <p>
  538. 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>
  539. volatile class invariants instead. Preconditions and postconditions of volatile
  540. public functions and volatile class invariants access the object as <code class="computeroutput"><span class="keyword">volatile</span></code>.
  541. </p>
  542. <p>
  543. Class invariants are checked before preconditions and postconditions so programming
  544. precondition and postcondition assertions can be simplified assuming that
  545. class invariants are satisfied already (e.g., if class invariants assert
  546. that a pointer cannot be null then preconditions and postconditions can safety
  547. dereference that pointer without additional checking). Similarly, static
  548. class invariants are checked before non-static class invariants so programming
  549. non-static class invariant (volatile and non) can be simplified assuming
  550. that static class invariants are satisfied already. Furthermore, subcontracting
  551. checks contracts of public base classes before checking the derived class
  552. contracts so programming derived class contract assertions can be simplified
  553. by assuming that public base class contracts are satisfied already.
  554. </p>
  555. <div class="note"><table border="0" summary="Note">
  556. <tr>
  557. <td rowspan="2" align="center" valign="top" width="25"><img alt="[Note]" src="../../../../../doc/src/images/note.png"></td>
  558. <th align="left">Note</th>
  559. </tr>
  560. <tr><td align="left" valign="top">
  561. <p>
  562. <a name="and_anchor"></a><a name="or_anchor"></a>In this documentation
  563. <a class="link" href="contract_programming_overview.html#and_anchor"><code class="literal"><span class="emphasis"><em>AND</em></span></code></a>
  564. and <a class="link" href="contract_programming_overview.html#or_anchor"><code class="literal"><span class="emphasis"><em>OR</em></span></code></a>
  565. indicate the logic <span class="emphasis"><em>and</em></span> and <span class="emphasis"><em>or</em></span>
  566. operations evaluated in <span class="emphasis"><em>short-circuit</em></span>. For example:
  567. <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>
  568. <code class="computeroutput"><span class="identifier">q</span></code> is true if and only if
  569. 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>
  570. is never evaluated when <code class="computeroutput"><span class="identifier">p</span></code>
  571. 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>
  572. <code class="computeroutput"><span class="identifier">q</span></code> is true if and only if
  573. 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>
  574. is never evaluated when <code class="computeroutput"><span class="identifier">p</span></code>
  575. is true.
  576. </p>
  577. <p>
  578. As indicated by the steps above and in accordance with the <a href="http://en.wikipedia.org/wiki/Liskov_substitution_principle" target="_top">substitution
  579. 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>
  580. while class invariants, postconditions, and exceptions guarantees are checked
  581. in <a class="link" href="contract_programming_overview.html#and_anchor"><code class="literal"><span class="emphasis"><em>AND</em></span></code></a>
  582. with preconditions, class invariants, postconditions, and exceptions guarantees
  583. of base classes respectively.
  584. </p>
  585. </td></tr>
  586. </table></div>
  587. <h5>
  588. <a name="boost_contract.contract_programming_overview.public_function_calls.h1"></a>
  589. <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
  590. Public Functions</a>
  591. </h5>
  592. <p>
  593. A call to a non-static public function with a contract (that does not override
  594. functions from any of its public base classes) executes the following steps
  595. (see <code class="computeroutput"><a class="link" href="../boost/contract/public_f_idm45394998885120.html" title="Function template public_function">boost::contract::public_function</a></code>):
  596. </p>
  597. <div class="orderedlist"><ol class="orderedlist" type="1">
  598. <li class="listitem">
  599. 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>
  600. non-static invariants (but none of the invariants from base classes).
  601. </li>
  602. <li class="listitem">
  603. Check function preconditions (but none of the preconditions from functions
  604. in base classes).
  605. </li>
  606. <li class="listitem">
  607. Execute the function body.
  608. </li>
  609. <li class="listitem">
  610. 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>
  611. non-static invariants (even if the body threw an exception, but none
  612. of the invariants from base classes).
  613. </li>
  614. <li class="listitem">
  615. If the body did not throw an exception, check function postconditions
  616. (but none of the postconditions from functions in base classes).
  617. </li>
  618. <li class="listitem">
  619. Else, check function exception guarantees (but none of the exception
  620. guarantees from functions in base classes).
  621. </li>
  622. </ol></div>
  623. <p>
  624. 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>
  625. volatile class invariants instead. Preconditions and postconditions of volatile
  626. functions and volatile class invariants access the object as <code class="computeroutput"><span class="keyword">volatile</span></code>.
  627. </p>
  628. <p>
  629. Class invariants are checked because this function is part of the class public
  630. interface. However, none of the contracts of the base classes are checked
  631. because this function does not override any functions from any of the public
  632. base classes (so the <a href="http://en.wikipedia.org/wiki/Liskov_substitution_principle" target="_top">substitution
  633. principle</a> does not require to subcontract in this case).
  634. </p>
  635. <h5>
  636. <a name="boost_contract.contract_programming_overview.public_function_calls.h2"></a>
  637. <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
  638. Public Functions</a>
  639. </h5>
  640. <p>
  641. A call to a static public function with a contract executes the following
  642. steps (see <code class="computeroutput"><a class="link" href="../boost/contract/public_f_idm45394998885120.html" title="Function template public_function">boost::contract::public_function</a></code>):
  643. </p>
  644. <div class="orderedlist"><ol class="orderedlist" type="1">
  645. <li class="listitem">
  646. Check static class invariants (but not the non-static invariants and
  647. none of the invariants from base classes).
  648. </li>
  649. <li class="listitem">
  650. Check function preconditions (but none of the preconditions from functions
  651. in base classes).
  652. </li>
  653. <li class="listitem">
  654. Execute the function body.
  655. </li>
  656. <li class="listitem">
  657. Check static class invariants (even if the body threw an exception, but
  658. not the non-static invariants and none of the invariants from base classes).
  659. </li>
  660. <li class="listitem">
  661. If the body did not throw an exception, check function postconditions
  662. (but none of the postconditions from functions in base classes).
  663. </li>
  664. <li class="listitem">
  665. Else, check function exception guarantees (but none of the exception
  666. guarantees from functions in base classes).
  667. </li>
  668. </ol></div>
  669. <p>
  670. Class invariants are checked because this function is part of the class public
  671. interface, but only static class invariants can be checked (because this
  672. is a static function so it cannot access the object that would instead be
  673. required to check non-static class invariants, volatile or not). Furthermore,
  674. static functions cannot override any function so the <a href="http://en.wikipedia.org/wiki/Liskov_substitution_principle" target="_top">substitution
  675. principle</a> does not apply and they do not subcontract.
  676. </p>
  677. <p>
  678. Preconditions and postconditions of static functions and static class invariants
  679. cannot access the object (because they are checked from <code class="computeroutput"><span class="keyword">static</span></code>
  680. member functions).
  681. </p>
  682. </div>
  683. <div class="section">
  684. <div class="titlepage"><div><div><h3 class="title">
  685. <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
  686. Calls</a>
  687. </h3></div></div></div>
  688. <p>
  689. A call to a constructor with a contract executes the following steps (see
  690. <code class="computeroutput"><a class="link" href="../boost/contract/constructor_precondition.html" title="Class template constructor_precondition">boost::contract::constructor_precondition</a></code>
  691. and <code class="computeroutput"><a class="link" href="../boost/contract/constructor.html" title="Function template constructor">boost::contract::constructor</a></code>):
  692. </p>
  693. <div class="orderedlist"><ol class="orderedlist" type="1">
  694. <li class="listitem">
  695. Check constructor preconditions (but these cannot access the object because
  696. the object is not constructed yet).
  697. </li>
  698. <li class="listitem">
  699. Execute the constructor member initialization list (if present).
  700. <div class="orderedlist"><ol class="orderedlist" type="a"><li class="listitem">
  701. Construct any base class (public or not) according with C++ construction
  702. mechanism and also check the contracts of these base constructors
  703. (according with steps similar to the ones listed here).
  704. </li></ol></div>
  705. </li>
  706. <li class="listitem">
  707. Check static class invariants (but not the non-static or volatile class
  708. invariants, because the object is not constructed yet).
  709. </li>
  710. <li class="listitem">
  711. Execute the constructor body.
  712. </li>
  713. <li class="listitem">
  714. Check static class invariants (even if the body threw an exception).
  715. </li>
  716. <li class="listitem">
  717. If the body did not throw an exception:
  718. <div class="orderedlist"><ol class="orderedlist" type="a">
  719. <li class="listitem">
  720. 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>
  721. volatile class invariants (because the object is now successfully
  722. constructed).
  723. </li>
  724. <li class="listitem">
  725. Check constructor postconditions (but these cannot access the object
  726. 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
  727. before the execution of the constructor body).
  728. </li>
  729. </ol></div>
  730. </li>
  731. <li class="listitem">
  732. Else, check constructor exception guarantees (but these cannot access
  733. 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
  734. before the execution of the constructor body, plus they can only access
  735. class' static members because the object has not been successfully constructed
  736. given the constructor body threw an exception in this case).
  737. </li>
  738. </ol></div>
  739. <p>
  740. Constructor preconditions are checked before executing the member initialization
  741. list so programming these initializations can be simplified assuming the
  742. constructor preconditions are satisfied (e.g., constructor arguments can
  743. be validated by the constructor preconditions before they are used to initialize
  744. base classes and data members).
  745. </p>
  746. <p>
  747. As indicated in step 2.a. above, C++ object construction mechanism will automatically
  748. check base class contracts when these bases are initialized (no explicit
  749. subcontracting behaviour is required here).
  750. </p>
  751. </div>
  752. <div class="section">
  753. <div class="titlepage"><div><div><h3 class="title">
  754. <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
  755. Calls</a>
  756. </h3></div></div></div>
  757. <p>
  758. A call to a destructor with a contract executes the following steps (see
  759. <code class="computeroutput"><a class="link" href="../boost/contract/destructor.html" title="Function template destructor">boost::contract::destructor</a></code>):
  760. </p>
  761. <div class="orderedlist"><ol class="orderedlist" type="1">
  762. <li class="listitem">
  763. 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>
  764. non-static <a class="link" href="contract_programming_overview.html#and_anchor"><code class="literal"><span class="emphasis"><em>AND</em></span></code></a>
  765. volatile class invariants.
  766. </li>
  767. <li class="listitem">
  768. Execute the destructor body (destructors have no parameters and they
  769. can be called at any time after object construction so they have no preconditions).
  770. </li>
  771. <li class="listitem">
  772. Check static class invariants (even if the body threw an exception).
  773. </li>
  774. <li class="listitem">
  775. If the body did not throw an exception:
  776. <div class="orderedlist"><ol class="orderedlist" type="a">
  777. <li class="listitem">
  778. Check destructor postconditions (but these can only access class'
  779. 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
  780. 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>
  781. </li>
  782. <li class="listitem">
  783. Destroy any base class (public or not) according with C++ destruction
  784. mechanism and also check the contracts of these base destructors
  785. (according with steps similar to the ones listed here).
  786. </li>
  787. </ol></div>
  788. </li>
  789. <li class="listitem">
  790. Else (even if destructors should rarely, if ever, be allowed to throw
  791. exceptions in C++):
  792. <div class="orderedlist"><ol class="orderedlist" type="a">
  793. <li class="listitem">
  794. 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>
  795. volatile class invariants (because the object was not successfully
  796. destructed so it still exists and should satisfy its invariants).
  797. </li>
  798. <li class="listitem">
  799. Check destructor exception guarantees.
  800. </li>
  801. </ol></div>
  802. </li>
  803. </ol></div>
  804. <p>
  805. As indicated in step 4.b. above, C++ object destruction mechanism will automatically
  806. check base class contracts when the destructor exits without throwing an
  807. exception (no explicit subcontracting behaviour is required here).
  808. </p>
  809. <div class="note"><table border="0" summary="Note">
  810. <tr>
  811. <td rowspan="2" align="center" valign="top" width="25"><img alt="[Note]" src="../../../../../doc/src/images/note.png"></td>
  812. <th align="left">Note</th>
  813. </tr>
  814. <tr><td align="left" valign="top"><p>
  815. Given that C++ allows destructors to throw, this library handles the case
  816. when the destructor body throws an exception as indicated above. However,
  817. in order to comply with STL exception safety guarantees and good C++ programming
  818. practices, programmers should implement destructor bodies to rarely, if
  819. ever, throw exceptions (in fact destructors are implicitly declared <code class="computeroutput"><span class="keyword">noexcept</span></code> in C++11).
  820. </p></td></tr>
  821. </table></div>
  822. </div>
  823. <div class="section">
  824. <div class="titlepage"><div><div><h3 class="title">
  825. <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>
  826. </h3></div></div></div>
  827. <p>
  828. Contracts should not be allowed to modify the program state because they
  829. are only responsible to check (and not to change) the program state in order
  830. to verify its compliance with the specifications. Therefore, contracts should
  831. only access objects, function arguments, function return values, old values,
  832. and all other program variables in <code class="computeroutput"><span class="keyword">const</span></code>
  833. context (via <code class="computeroutput"><span class="keyword">const</span><span class="special">&amp;</span></code>,
  834. <code class="computeroutput"><span class="keyword">const</span><span class="special">*</span>
  835. <span class="keyword">const</span></code>, <code class="computeroutput"><span class="keyword">const</span>
  836. <span class="keyword">volatile</span></code>, etc.).
  837. </p>
  838. <p>
  839. Whenever possible (e.g., class invariants and postcondition old values),
  840. this library automatically enforces this <span class="emphasis"><em>constant-correctness constraint</em></span>
  841. at compile-time using <code class="computeroutput"><span class="keyword">const</span></code>.
  842. However, this library cannot automatically enforce this constraint in all
  843. cases (for preconditions and postconditions of mutable member functions,
  844. 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
  845. Lambda Functions</a> for ways of using this library that enforce the constant-correctness
  846. constraint at compile-time (but at the cost of significant boiler-plate code
  847. to be programmed manually so not recommended in general).
  848. </p>
  849. <div class="note"><table border="0" summary="Note">
  850. <tr>
  851. <td rowspan="2" align="center" valign="top" width="25"><img alt="[Note]" src="../../../../../doc/src/images/note.png"></td>
  852. <th align="left">Note</th>
  853. </tr>
  854. <tr><td align="left" valign="top"><p>
  855. In general, it is the responsibility of the programmers to code assertions
  856. 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>
  857. </p></td></tr>
  858. </table></div>
  859. </div>
  860. <div class="section">
  861. <div class="titlepage"><div><div><h3 class="title">
  862. <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
  863. vs. Implementation</a>
  864. </h3></div></div></div>
  865. <p>
  866. Contracts are part of the program specification and not of its implementation.
  867. Therefore, contracts should ideally be programmed within C++ declarations,
  868. and not within definitions.
  869. </p>
  870. <p>
  871. In general, this library cannot satisfy this requirement. However, even when
  872. contracts are programmed together with the body in the function definition,
  873. it is still fairly easy for users to identify and read just the contract
  874. portion of the function definition (because the contract code must always
  875. 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
  876. Body Implementation</a> for ways of using this library to program contract
  877. specifications outside of the body implementation (but at the cost of writing
  878. one extra function for any given function so not recommended in general).
  879. </p>
  880. <p>
  881. Furthermore, contracts are most useful when they assert conditions only using
  882. public members (in most cases, the need for using non-public members to check
  883. contracts, especially in preconditions, indicates an error in the class design).
  884. For example, the caller of a public function cannot in general make sure
  885. that the function preconditions are satisfied if the precondition assertions
  886. use private members that are not callable by the caller (therefore, a failure
  887. in the preconditions will not necessarily indicate a bug in the caller given
  888. that the caller was made unable to fully check the preconditions in the first
  889. place). However, given that C++ provides programmers ways around access level
  890. restrictions (<code class="computeroutput"><span class="keyword">friend</span></code>, function
  891. pointers, etc.), this library leaves it up to programmers to make sure that
  892. only public members are used in contract assertions (especially in preconditions).
  893. (<a class="link" href="bibliography.html#N1962_anchor">[N1962]</a> follows the same approach not
  894. restricting contracts to only use public members, Eiffel instead generates
  895. a compile-time error if preconditions are asserted using non-public members.)
  896. <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>
  897. </p>
  898. </div>
  899. <div class="section">
  900. <div class="titlepage"><div><div><h3 class="title">
  901. <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
  902. Contract Failures</a>
  903. </h3></div></div></div>
  904. <p>
  905. If preconditions, postconditions, exception guarantees, or class invariants
  906. are either checked to be false or their evaluation throws an exception at
  907. run-time then this library will call specific <span class="emphasis"><em>failure handler functions</em></span>.
  908. <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>
  909. </p>
  910. <p>
  911. By default, these failure handler functions print a message to the standard
  912. error <code class="computeroutput"><span class="identifier">std</span><span class="special">::</span><span class="identifier">cerr</span></code> (with detailed information about the
  913. 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>.
  914. 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>,
  915. <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>,
  916. <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>,
  917. <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>,
  918. etc. programmers can define their own failure handler functions that can
  919. take any user-specified action (throw an exception, exit the program with
  920. 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
  921. 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>
  922. </p>
  923. <div class="note"><table border="0" summary="Note">
  924. <tr>
  925. <td rowspan="2" align="center" valign="top" width="25"><img alt="[Note]" src="../../../../../doc/src/images/note.png"></td>
  926. <th align="left">Note</th>
  927. </tr>
  928. <tr><td align="left" valign="top"><p>
  929. In C++ there are a number of issues with programming contract failure handlers
  930. that throw exceptions instead of terminating the program. Specifically,
  931. destructors check class invariants so they will throw if programmers change
  932. class invariant failure handlers to throw instead of terminating the program,
  933. but in general destructors should not throw in C++ (to comply with STL
  934. exception safety, C++11 implicit <code class="computeroutput"><span class="keyword">noexcept</span></code>
  935. declarations for destructors, etc.). Furthermore, programming a failure
  936. handler that throws on exception guarantee failures results in throwing
  937. an exception (the one reporting the contract failure) while there is already
  938. an active exception (the one that caused the exception guarantees to be
  939. checked in the first place), and this will force C++ to terminate the program
  940. anyway.
  941. </p></td></tr>
  942. </table></div>
  943. <p>
  944. Therefore, it is recommended to terminate the program at least for contract
  945. failures from destructors and exception guarantees (if not in all other cases
  946. of contract failures as it is done by default by this library). The contract
  947. failure handler functions programmed using this library have information
  948. about the failed contract (preconditions, postconditions, etc.) and the operation
  949. that was checking the contract (constructor, destructor, etc.) so programmers
  950. can granularly distinguish all cases and decide when it is appropriate to
  951. terminate, throw, or take some other user-specific action.
  952. </p>
  953. </div>
  954. <div class="section">
  955. <div class="titlepage"><div><div><h3 class="title">
  956. <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
  957. Summary</a>
  958. </h3></div></div></div>
  959. <p>
  960. The contract programming features supported by this library are largely based
  961. on <a class="link" href="bibliography.html#N1962_anchor">[N1962]</a> and on the Eiffel programming
  962. language.
  963. </p>
  964. <p>
  965. The following table compares contract programming features among this library,
  966. <a class="link" href="bibliography.html#N1962_anchor">[N1962]</a> (unfortunately the C++ standard
  967. committee rejected this proposal commenting on a lack of interest in adding
  968. contract programming to C++ at that time, even if <a class="link" href="bibliography.html#N1962_anchor">[N1962]</a>
  969. itself is sound), a more recent proposal <a class="link" href="bibliography.html#P0380_anchor">[P0380]</a>
  970. (which was accepted in the C++20 standard but unfortunately only supports
  971. preconditions and postconditions, while does not support class invariants,
  972. old values, and subcontracting), the Eiffel and D programming languages.
  973. Some of the items listed in this summary table will become clear in detail
  974. after reading the remaining sections of this documentation.
  975. </p>
  976. <div class="informaltable"><table class="table">
  977. <colgroup>
  978. <col>
  979. <col>
  980. <col>
  981. <col>
  982. <col>
  983. <col>
  984. </colgroup>
  985. <thead><tr>
  986. <th>
  987. <p>
  988. Feature
  989. </p>
  990. </th>
  991. <th>
  992. <p>
  993. This Library
  994. </p>
  995. </th>
  996. <th>
  997. <p>
  998. <a class="link" href="bibliography.html#N1962_anchor">[N1962]</a> Proposal (not accepted
  999. in C++)
  1000. </p>
  1001. </th>
  1002. <th>
  1003. <p>
  1004. C++20 (see <a class="link" href="bibliography.html#P0380_anchor">[P0380]</a>)
  1005. </p>
  1006. </th>
  1007. <th>
  1008. <p>
  1009. ISE Eiffel 5.4 (see <a class="link" href="bibliography.html#Meyer97_anchor">[Meyer97]</a>)
  1010. </p>
  1011. </th>
  1012. <th>
  1013. <p>
  1014. D (see <a class="link" href="bibliography.html#Bright04_anchor">[Bright04]</a>)
  1015. </p>
  1016. </th>
  1017. </tr></thead>
  1018. <tbody>
  1019. <tr>
  1020. <td>
  1021. <p>
  1022. <span class="emphasis"><em>Keywords and specifiers</em></span>
  1023. </p>
  1024. </td>
  1025. <td>
  1026. <p>
  1027. Specifiers: <code class="computeroutput"><span class="identifier">precondition</span></code>,
  1028. <code class="computeroutput"><span class="identifier">postcondition</span></code>,
  1029. <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
  1030. appear in user code so their names can be referred to or changed
  1031. using <code class="computeroutput"><a class="link" href="../BOOST_CONTRACT_INVARIANT.html" title="Macro BOOST_CONTRACT_INVARIANT">BOOST_CONTRACT_INVARIANT</a></code>,
  1032. <code class="computeroutput"><a class="link" href="../BOOST_CO_idm45394998621472.html" title="Macro BOOST_CONTRACT_STATIC_INVARIANT">BOOST_CONTRACT_STATIC_INVARIANT</a></code>,
  1033. and <code class="computeroutput"><a class="link" href="../BOOST_CO_idm45394999732400.html" title="Macro BOOST_CONTRACT_BASES_TYPEDEF">BOOST_CONTRACT_BASES_TYPEDEF</a></code>
  1034. macros respectively to avoid name clashes.
  1035. </p>
  1036. </td>
  1037. <td>
  1038. <p>
  1039. Keywords: <code class="computeroutput"><span class="identifier">precondition</span></code>,
  1040. <code class="computeroutput"><span class="identifier">postcondition</span></code>,
  1041. <code class="computeroutput"><span class="identifier">oldof</span></code>, and <code class="computeroutput"><span class="identifier">invariant</span></code>.
  1042. </p>
  1043. </td>
  1044. <td>
  1045. <p>
  1046. 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>.
  1047. </p>
  1048. </td>
  1049. <td>
  1050. <p>
  1051. Keywords: <code class="literal">require</code>, <code class="literal">require else</code>,
  1052. <code class="literal">ensure</code>, <code class="literal">ensure then</code>, <code class="literal">old</code>,
  1053. <code class="literal">result</code>, <code class="literal">do</code>, and <code class="literal">invariant</code>.
  1054. </p>
  1055. </td>
  1056. <td>
  1057. <p>
  1058. Keywords: <code class="literal">in</code>, <code class="literal">out</code>, <code class="literal">do</code>,
  1059. <code class="literal">assert</code>, and <code class="literal">invariant</code>.
  1060. </p>
  1061. </td>
  1062. </tr>
  1063. <tr>
  1064. <td>
  1065. <p>
  1066. <span class="emphasis"><em>On contract failures</em></span>
  1067. </p>
  1068. </td>
  1069. <td>
  1070. <p>
  1071. Print an error to <code class="computeroutput"><span class="identifier">std</span><span class="special">::</span><span class="identifier">cerr</span></code>
  1072. and call <code class="computeroutput"><span class="identifier">std</span><span class="special">::</span><span class="identifier">terminate</span></code> (but can be customized
  1073. to throw exceptions, exit with an error code, etc.).
  1074. </p>
  1075. </td>
  1076. <td>
  1077. <p>
  1078. Call <code class="computeroutput"><span class="identifier">std</span><span class="special">::</span><span class="identifier">terminate</span></code> (but can be customized
  1079. to throw exceptions, exit with an error code, etc.).
  1080. </p>
  1081. </td>
  1082. <td>
  1083. <p>
  1084. Call <code class="computeroutput"><span class="identifier">std</span><span class="special">::</span><span class="identifier">abort</span></code> (but can be customized
  1085. to throw exceptions, exit with an error code, etc.).
  1086. </p>
  1087. </td>
  1088. <td>
  1089. <p>
  1090. Throw exceptions.
  1091. </p>
  1092. </td>
  1093. <td>
  1094. <p>
  1095. Throw exceptions.
  1096. </p>
  1097. </td>
  1098. </tr>
  1099. <tr>
  1100. <td>
  1101. <p>
  1102. <span class="emphasis"><em>Return values in postconditions</em></span>
  1103. </p>
  1104. </td>
  1105. <td>
  1106. <p>
  1107. Yes, captured by or passed as a parameter to (for virtual functions)
  1108. the postcondition functor.
  1109. </p>
  1110. </td>
  1111. <td>
  1112. <p>
  1113. 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>.
  1114. </p>
  1115. </td>
  1116. <td>
  1117. <p>
  1118. Yes, <code class="computeroutput"><span class="special">[[</span><span class="identifier">ensures</span>
  1119. </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>.
  1120. </p>
  1121. </td>
  1122. <td>
  1123. <p>
  1124. Yes, <code class="literal">result</code> keyword.
  1125. </p>
  1126. </td>
  1127. <td>
  1128. <p>
  1129. 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>.
  1130. </p>
  1131. </td>
  1132. </tr>
  1133. <tr>
  1134. <td>
  1135. <p>
  1136. <span class="emphasis"><em>Old values in postconditions</em></span>
  1137. </p>
  1138. </td>
  1139. <td>
  1140. <p>
  1141. Yes, <code class="computeroutput"><a class="link" href="../BOOST_CONTRACT_OLDOF.html" title="Macro BOOST_CONTRACT_OLDOF">BOOST_CONTRACT_OLDOF</a></code>
  1142. 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>
  1143. (but copied before preconditions unless <code class="computeroutput"><span class="special">.</span><span class="identifier">old</span><span class="special">(...)</span></code>
  1144. 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
  1145. 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>
  1146. 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>
  1147. skips old value copies selectively based on old expression type
  1148. requirements (on compilers that do not support <code class="computeroutput"><span class="keyword">if</span>
  1149. <span class="keyword">constexpr</span></code>).
  1150. </p>
  1151. </td>
  1152. <td>
  1153. <p>
  1154. Yes, <code class="computeroutput"><span class="identifier">oldof</span></code> keyword
  1155. (copied right after preconditions). (Never skipped, not even in
  1156. templates for non-copyable types.)
  1157. </p>
  1158. </td>
  1159. <td>
  1160. <p>
  1161. No.
  1162. </p>
  1163. </td>
  1164. <td>
  1165. <p>
  1166. Yes, <code class="literal">old</code> keyword (copied right after preconditions).
  1167. (Never skipped, but all types are copyable in Eiffel.)
  1168. </p>
  1169. </td>
  1170. <td>
  1171. <p>
  1172. No.
  1173. </p>
  1174. </td>
  1175. </tr>
  1176. <tr>
  1177. <td>
  1178. <p>
  1179. <span class="emphasis"><em>Class invariants</em></span>
  1180. </p>
  1181. </td>
  1182. <td>
  1183. <p>
  1184. Yes, checked at constructor exit, at destructor entry and throw,
  1185. and at public function entry, exit, and throw. Same for volatile
  1186. class invariants. Static class invariants checked at entry, exit,
  1187. and throw for constructors, destructors, and any (also <code class="computeroutput"><span class="keyword">static</span></code>) public function.
  1188. </p>
  1189. </td>
  1190. <td>
  1191. <p>
  1192. Yes, checked at constructor exit, at destructor entry and throw,
  1193. and at public function entry, exit, and throw. (Volatile and static
  1194. class invariants not supported.)
  1195. </p>
  1196. </td>
  1197. <td>
  1198. <p>
  1199. No.
  1200. </p>
  1201. </td>
  1202. <td>
  1203. <p>
  1204. Yes, checked at constructor exit, and around public functions.
  1205. (Volatile and static class invariants do not apply to Eiffel.)
  1206. </p>
  1207. </td>
  1208. <td>
  1209. <p>
  1210. Yes, checked at constructor exit, at destructor entry, and around
  1211. public functions. However, invariants cannot call public functions
  1212. (to avoid infinite recursion because D does not disable contracts
  1213. while checking other contracts). (Volatile and static class invariants
  1214. not supported, <code class="computeroutput"><span class="keyword">volatile</span></code>
  1215. was deprecated all together in D.)
  1216. </p>
  1217. </td>
  1218. </tr>
  1219. <tr>
  1220. <td>
  1221. <p>
  1222. <span class="emphasis"><em>Subcontracting</em></span>
  1223. </p>
  1224. </td>
  1225. <td>
  1226. <p>
  1227. 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>,
  1228. <code class="computeroutput"><a class="link" href="../BOOST_CONTRACT_OVERRIDE.html" title="Macro BOOST_CONTRACT_OVERRIDE">BOOST_CONTRACT_OVERRIDE</a></code>,
  1229. and <code class="computeroutput"><a class="link" href="../boost/contract/virtual_.html" title="Class virtual_">boost::contract::virtual_</a></code>
  1230. are used to declare base classes, overrides and virtual public
  1231. functions respectively).
  1232. </p>
  1233. </td>
  1234. <td>
  1235. <p>
  1236. Yes, also supports subcontracting for multiple inheritance, but
  1237. 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>
  1238. </p>
  1239. </td>
  1240. <td>
  1241. <p>
  1242. No.
  1243. </p>
  1244. </td>
  1245. <td>
  1246. <p>
  1247. Yes.
  1248. </p>
  1249. </td>
  1250. <td>
  1251. <p>
  1252. Yes.
  1253. </p>
  1254. </td>
  1255. </tr>
  1256. <tr>
  1257. <td>
  1258. <p>
  1259. <span class="emphasis"><em>Contracts for pure virtual functions</em></span>
  1260. </p>
  1261. </td>
  1262. <td>
  1263. <p>
  1264. Yes (programmed via out-of-line functions as always in C++ with
  1265. pure virtual function definitions).
  1266. </p>
  1267. </td>
  1268. <td>
  1269. <p>
  1270. Yes.
  1271. </p>
  1272. </td>
  1273. <td>
  1274. <p>
  1275. No (because no subcontracting).
  1276. </p>
  1277. </td>
  1278. <td>
  1279. <p>
  1280. Yes (contracts for abstract functions).
  1281. </p>
  1282. </td>
  1283. <td>
  1284. <p>
  1285. No.
  1286. </p>
  1287. </td>
  1288. </tr>
  1289. <tr>
  1290. <td>
  1291. <p>
  1292. <span class="emphasis"><em>Arbitrary code in contracts</em></span>
  1293. </p>
  1294. </td>
  1295. <td>
  1296. <p>
  1297. Yes (but users are generally recommended to only program assertions
  1298. using <code class="computeroutput"><a class="link" href="../BOOST_CONTRACT_ASSERT.html" title="Macro BOOST_CONTRACT_ASSERT">BOOST_CONTRACT_ASSERT</a></code>
  1299. and if-guard statements within contracts to avoid introducing bugs
  1300. and expensive code in contracts, and also to only use public functions
  1301. to program preconditions).
  1302. </p>
  1303. </td>
  1304. <td>
  1305. <p>
  1306. No, assertions only (use of only public functions to program preconditions
  1307. is recommended but not prescribed).
  1308. </p>
  1309. </td>
  1310. <td>
  1311. <p>
  1312. No, assertions only (in addition contracts of public, protected,
  1313. and private members can only use other public, public/protected,
  1314. and public/protected/private members respectively).
  1315. </p>
  1316. </td>
  1317. <td>
  1318. <p>
  1319. No, assertions only (in addition only public members can be used
  1320. in preconditions).
  1321. </p>
  1322. </td>
  1323. <td>
  1324. <p>
  1325. Yes.
  1326. </p>
  1327. </td>
  1328. </tr>
  1329. <tr>
  1330. <td>
  1331. <p>
  1332. <span class="emphasis"><em>Constant-correctness</em></span>
  1333. </p>
  1334. </td>
  1335. <td>
  1336. <p>
  1337. No, enforced only for class invariants and old values (making also
  1338. preconditions and postconditions constant-correct is possible but
  1339. requires users to program a fare amount of boiler-plate code).
  1340. </p>
  1341. </td>
  1342. <td>
  1343. <p>
  1344. Yes.
  1345. </p>
  1346. </td>
  1347. <td>
  1348. <p>
  1349. Yes (side effects in contracts lead to undefined behaviour).
  1350. </p>
  1351. </td>
  1352. <td>
  1353. <p>
  1354. Yes.
  1355. </p>
  1356. </td>
  1357. <td>
  1358. <p>
  1359. No, enforced only for class invariants.
  1360. </p>
  1361. </td>
  1362. </tr>
  1363. <tr>
  1364. <td>
  1365. <p>
  1366. <span class="emphasis"><em>Contracts in specifications</em></span>
  1367. </p>
  1368. </td>
  1369. <td>
  1370. <p>
  1371. No, in function definitions instead (unless programmers manually
  1372. write an extra function for any given function).
  1373. </p>
  1374. </td>
  1375. <td>
  1376. <p>
  1377. Yes (in function declarations).
  1378. </p>
  1379. </td>
  1380. <td>
  1381. <p>
  1382. Yes (in function declarations).
  1383. </p>
  1384. </td>
  1385. <td>
  1386. <p>
  1387. Yes.
  1388. </p>
  1389. </td>
  1390. <td>
  1391. <p>
  1392. Yes.
  1393. </p>
  1394. </td>
  1395. </tr>
  1396. <tr>
  1397. <td>
  1398. <p>
  1399. <span class="emphasis"><em>Function code ordering</em></span>
  1400. </p>
  1401. </td>
  1402. <td>
  1403. <p>
  1404. Preconditions, postconditions, exception guarantees, body.
  1405. </p>
  1406. </td>
  1407. <td>
  1408. <p>
  1409. Preconditions, postconditions, body.
  1410. </p>
  1411. </td>
  1412. <td>
  1413. <p>
  1414. Preconditions, postconditions, body.
  1415. </p>
  1416. </td>
  1417. <td>
  1418. <p>
  1419. Preconditions, body, postconditions.
  1420. </p>
  1421. </td>
  1422. <td>
  1423. <p>
  1424. Preconditions, postconditions, body.
  1425. </p>
  1426. </td>
  1427. </tr>
  1428. <tr>
  1429. <td>
  1430. <p>
  1431. <span class="emphasis"><em>Disable assertion checking within assertions checking
  1432. (to avoid infinite recursion when checking contracts)</em></span>
  1433. </p>
  1434. </td>
  1435. <td>
  1436. <p>
  1437. Yes, but use <code class="computeroutput"><a class="link" href="../BOOST_CO_idm45394999685184.html" title="Macro BOOST_CONTRACT_PRECONDITIONS_DISABLE_NO_ASSERTION">BOOST_CONTRACT_PRECONDITIONS_DISABLE_NO_ASSERTION</a></code>
  1438. to disable no assertion while checking preconditions (see also
  1439. <code class="computeroutput"><a class="link" href="../BOOST_CO_idm45394999679376.html" title="Macro BOOST_CONTRACT_ALL_DISABLE_NO_ASSERTION">BOOST_CONTRACT_ALL_DISABLE_NO_ASSERTION</a></code>).
  1440. <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
  1441. lock, see <code class="computeroutput"><a class="link" href="../BOOST_CO_idm45394999743888.html" title="Macro BOOST_CONTRACT_DISABLE_THREADS">BOOST_CONTRACT_DISABLE_THREADS</a></code>.)
  1442. </p>
  1443. </td>
  1444. <td>
  1445. <p>
  1446. Yes for class invariants and postconditions, but preconditions
  1447. disable no assertion.
  1448. </p>
  1449. </td>
  1450. <td>
  1451. <p>
  1452. No.
  1453. </p>
  1454. </td>
  1455. <td>
  1456. <p>
  1457. Yes.
  1458. </p>
  1459. </td>
  1460. <td>
  1461. <p>
  1462. No.
  1463. </p>
  1464. </td>
  1465. </tr>
  1466. <tr>
  1467. <td>
  1468. <p>
  1469. <span class="emphasis"><em>Nested member function calls</em></span>
  1470. </p>
  1471. </td>
  1472. <td>
  1473. <p>
  1474. 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>
  1475. </p>
  1476. </td>
  1477. <td>
  1478. <p>
  1479. Disable nothing.
  1480. </p>
  1481. </td>
  1482. <td>
  1483. <p>
  1484. Disable nothing.
  1485. </p>
  1486. </td>
  1487. <td>
  1488. <p>
  1489. Disable all contract assertions.
  1490. </p>
  1491. </td>
  1492. <td>
  1493. <p>
  1494. Disable nothing.
  1495. </p>
  1496. </td>
  1497. </tr>
  1498. <tr>
  1499. <td>
  1500. <p>
  1501. <span class="emphasis"><em>Disable contract checking</em></span>
  1502. </p>
  1503. </td>
  1504. <td>
  1505. <p>
  1506. Yes, contract checking can be skipped at run-time by defining combinations
  1507. of the <code class="computeroutput"><a class="link" href="../BOOST_CO_idm45394999662416.html" title="Macro BOOST_CONTRACT_NO_PRECONDITIONS">BOOST_CONTRACT_NO_PRECONDITIONS</a></code>,
  1508. <code class="computeroutput"><a class="link" href="../BOOST_CO_idm45394999656032.html" title="Macro BOOST_CONTRACT_NO_POSTCONDITIONS">BOOST_CONTRACT_NO_POSTCONDITIONS</a></code>,
  1509. <code class="computeroutput"><a class="link" href="../BOOST_CO_idm45394999622032.html" title="Macro BOOST_CONTRACT_NO_INVARIANTS">BOOST_CONTRACT_NO_INVARIANTS</a></code>,
  1510. <code class="computeroutput"><a class="link" href="../BOOST_CO_idm45394999637264.html" title="Macro BOOST_CONTRACT_NO_ENTRY_INVARIANTS">BOOST_CONTRACT_NO_ENTRY_INVARIANTS</a></code>,
  1511. and <code class="computeroutput"><a class="link" href="../BOOST_CO_idm45394999629648.html" title="Macro BOOST_CONTRACT_NO_EXIT_INVARIANTS">BOOST_CONTRACT_NO_EXIT_INVARIANTS</a></code>
  1512. macros (completely removing contract code from compiled object
  1513. 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
  1514. Contract Compilation</a>).
  1515. </p>
  1516. </td>
  1517. <td>
  1518. <p>
  1519. Yes (contract code also removed from compiled object code, but
  1520. details are compiler-implementation specific).
  1521. </p>
  1522. </td>
  1523. <td>
  1524. <p>
  1525. Yes (contract code also removed from compiled object code, but
  1526. details are compiler-implementation specific).
  1527. </p>
  1528. </td>
  1529. <td>
  1530. <p>
  1531. Yes, but only predefined combinations of preconditions, postconditions,
  1532. and class invariants can be disabled (contract code also removed
  1533. from compiled object code).
  1534. </p>
  1535. </td>
  1536. <td>
  1537. <p>
  1538. Yes.
  1539. </p>
  1540. </td>
  1541. </tr>
  1542. <tr>
  1543. <td>
  1544. <p>
  1545. <span class="emphasis"><em>Assertion levels</em></span>
  1546. </p>
  1547. </td>
  1548. <td>
  1549. <p>
  1550. Yes, predefined default, audit, and axiom, in addition programmers
  1551. can also define their own levels.
  1552. </p>
  1553. </td>
  1554. <td>
  1555. <p>
  1556. No (but a previous revision of this proposal considered adding
  1557. assertion levels under the name of "assertion ordering").
  1558. </p>
  1559. </td>
  1560. <td>
  1561. <p>
  1562. Yes, predefined default, audit, and axiom.
  1563. </p>
  1564. </td>
  1565. <td>
  1566. <p>
  1567. No.
  1568. </p>
  1569. </td>
  1570. <td>
  1571. <p>
  1572. No.
  1573. </p>
  1574. </td>
  1575. </tr>
  1576. </tbody>
  1577. <tbody class="footnotes"><tr><td colspan="6">
  1578. <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>
  1579. <span class="bold"><strong>Rationale:</strong></span> The authors of <a class="link" href="bibliography.html#N1962_anchor">[N1962]</a> decided to forbid derived
  1580. classes from subcontracting preconditions because they found
  1581. 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:
  1582. [boost] [contract] diff n1962</a>). Still, it should be noted
  1583. that even in <a class="link" href="bibliography.html#N1962_anchor">[N1962]</a> if a
  1584. derived class overrides two functions with preconditions coming
  1585. from two different base classes via multiple inheritance, the
  1586. overriding function contract will check preconditions from its
  1587. 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>
  1588. (so even in <a class="link" href="bibliography.html#N1962_anchor">[N1962]</a> preconditions
  1589. can indirectly subcontract when multiple inheritance is used).
  1590. Furthermore, subcontracting preconditions is soundly defined
  1591. by the <a href="http://en.wikipedia.org/wiki/Liskov_substitution_principle" target="_top">substitution
  1592. principle</a> so this library allows to subcontract preconditions
  1593. as Eiffel does (users can always avoid using this feature if
  1594. they have no need for it). (This is essentially the only feature
  1595. on which this library deliberately differs from <a class="link" href="bibliography.html#N1962_anchor">[N1962]</a>.)
  1596. </p></div>
  1597. <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>
  1598. <span class="bold"><strong>Rationale:</strong></span> Technically, it can
  1599. be shown that an invalid argument can reach the function body
  1600. when assertion checking is disabled while checking preconditions
  1601. (that is why <a class="link" href="bibliography.html#N1962_anchor">[N1962]</a> does
  1602. not disable any assertion while checking preconditions, see
  1603. <a href="http://lists.boost.org/Archives/boost/2010/04/164862.php" target="_top">Re:
  1604. [boost] [contract] diff n1962</a>). However, this can only
  1605. happen while checking contracts when an invalid argument passed
  1606. to the body, which should results in the body either throwing
  1607. an exception or returning an incorrect result, will in turn fail
  1608. the contract assertion being checked by the caller of the body
  1609. and invoke the related contract failure handler as desired in
  1610. the first place. Furthermore, not disabling assertions while
  1611. checking preconditions (like <a class="link" href="bibliography.html#N1962_anchor">[N1962]</a>
  1612. does) makes it possible to have infinite recursion while checking
  1613. preconditions. Therefore, this library by default disables assertion
  1614. checking also while checking preconditions (like Eiffel does),
  1615. but it also provides the <code class="computeroutput"><a class="link" href="../BOOST_CO_idm45394999685184.html" title="Macro BOOST_CONTRACT_PRECONDITIONS_DISABLE_NO_ASSERTION">BOOST_CONTRACT_PRECONDITIONS_DISABLE_NO_ASSERTION</a></code>
  1616. configuration macro so users can change this behaviour to match
  1617. <a class="link" href="bibliography.html#N1962_anchor">[N1962]</a> if needed.
  1618. </p></div>
  1619. <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>
  1620. <span class="bold"><strong>Rationale:</strong></span> Older versions of
  1621. this library defined a data member in the user class that was
  1622. automatically used to disable checking of class invariants within
  1623. nested member function calls (similarly to Eiffel). This feature
  1624. was required by older revisions of <a class="link" href="bibliography.html#N1962_anchor">[N1962]</a>
  1625. but it is no longer required by <a class="link" href="bibliography.html#N1962_anchor">[N1962]</a>
  1626. (because it seems to be motivated purely by optimization reasons
  1627. while similar performances can be achieved by disabling invariants
  1628. for release builds). Furthermore, in multi-threaded programs
  1629. this feature would introduce a lock that synchronizes all member
  1630. functions calls for a given object. Therefore, this feature was
  1631. removed in the current revision of this library.
  1632. </p></div>
  1633. </td></tr></tbody>
  1634. </table></div>
  1635. <p>
  1636. The authors of this library consulted the following references that implement
  1637. contract programming for C++ (but usually for only a limited set of features,
  1638. or using preprocessing tools other than the C++ preprocessor and external
  1639. to the language itself) and for other languages (see <a class="link" href="bibliography.html" title="Bibliography">Bibliography</a>
  1640. for a complete list of all references consulted during the design and development
  1641. of this library):
  1642. </p>
  1643. <div class="informaltable"><table class="table">
  1644. <colgroup>
  1645. <col>
  1646. <col>
  1647. <col>
  1648. </colgroup>
  1649. <thead><tr>
  1650. <th>
  1651. <p>
  1652. Reference
  1653. </p>
  1654. </th>
  1655. <th>
  1656. <p>
  1657. Language
  1658. </p>
  1659. </th>
  1660. <th>
  1661. <p>
  1662. Notes
  1663. </p>
  1664. </th>
  1665. </tr></thead>
  1666. <tbody>
  1667. <tr>
  1668. <td>
  1669. <p>
  1670. <a class="link" href="bibliography.html#Bright04b_anchor">[Bright04b]</a>
  1671. </p>
  1672. </td>
  1673. <td>
  1674. <p>
  1675. Digital Mars C++
  1676. </p>
  1677. </td>
  1678. <td>
  1679. <p>
  1680. The Digital Mars C++ compiler extends C++ adding contract programming
  1681. language support (among many other features).
  1682. </p>
  1683. </td>
  1684. </tr>
  1685. <tr>
  1686. <td>
  1687. <p>
  1688. <a class="link" href="bibliography.html#Maley99_anchor">[Maley99]</a>
  1689. </p>
  1690. </td>
  1691. <td>
  1692. <p>
  1693. C++
  1694. </p>
  1695. </td>
  1696. <td>
  1697. <p>
  1698. This supports contract programming including subcontracting but
  1699. with limitations (e.g., programmers need to manually build an inheritance
  1700. tree using artificial template parameters), it does not use macros
  1701. but programmers are required to write by hand a significant amount
  1702. of boiler-plate code. (The authors have found this work very inspiring
  1703. when developing initial revisions of this library especially for
  1704. its attempt to support subcontracting.)
  1705. </p>
  1706. </td>
  1707. </tr>
  1708. <tr>
  1709. <td>
  1710. <p>
  1711. <a class="link" href="bibliography.html#Lindrud04_anchor">[Lindrud04]</a>
  1712. </p>
  1713. </td>
  1714. <td>
  1715. <p>
  1716. C++
  1717. </p>
  1718. </td>
  1719. <td>
  1720. <p>
  1721. This supports class invariants and old values but it does not support
  1722. subcontracting (contracts are specified within definitions instead
  1723. of declarations and assertions are not constant-correct).
  1724. </p>
  1725. </td>
  1726. </tr>
  1727. <tr>
  1728. <td>
  1729. <p>
  1730. <a class="link" href="bibliography.html#Tandin04_anchor">[Tandin04]</a>
  1731. </p>
  1732. </td>
  1733. <td>
  1734. <p>
  1735. C++
  1736. </p>
  1737. </td>
  1738. <td>
  1739. <p>
  1740. Interestingly, these contract macros automatically generate Doxygen
  1741. 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
  1742. are not supported (plus contracts are specified within definitions
  1743. instead of declarations and assertions are not constant-correct).
  1744. </p>
  1745. </td>
  1746. </tr>
  1747. <tr>
  1748. <td>
  1749. <p>
  1750. <a class="link" href="bibliography.html#Nana_anchor">[Nana]</a>
  1751. </p>
  1752. </td>
  1753. <td>
  1754. <p>
  1755. GCC C++
  1756. </p>
  1757. </td>
  1758. <td>
  1759. <p>
  1760. This uses macros but it only works on GCC (and maybe Clang, but
  1761. it does not work on MSVC, etc.). It does not support subcontracting.
  1762. It requires extra care to program postconditions for functions
  1763. with multiple return statements. It seems that it might not check
  1764. class invariants when functions throw exceptions (unless the <code class="computeroutput"><span class="identifier">END</span></code> macro does that...). (In
  1765. addition, it provides tools for logging and integration with GDB.)
  1766. </p>
  1767. </td>
  1768. </tr>
  1769. <tr>
  1770. <td>
  1771. <p>
  1772. <a class="link" href="bibliography.html#C2_anchor">[C2]</a>
  1773. </p>
  1774. </td>
  1775. <td>
  1776. <p>
  1777. C++
  1778. </p>
  1779. </td>
  1780. <td>
  1781. <p>
  1782. This uses an external preprocessing tool (the authors could no
  1783. longer find this project's code to evaluate it).
  1784. </p>
  1785. </td>
  1786. </tr>
  1787. <tr>
  1788. <td>
  1789. <p>
  1790. <a class="link" href="bibliography.html#iContract_anchor">[iContract]</a>
  1791. </p>
  1792. </td>
  1793. <td>
  1794. <p>
  1795. Java
  1796. </p>
  1797. </td>
  1798. <td>
  1799. <p>
  1800. This uses an external preprocessing tool.
  1801. </p>
  1802. </td>
  1803. </tr>
  1804. <tr>
  1805. <td>
  1806. <p>
  1807. <a class="link" href="bibliography.html#Jcontract_anchor">[Jcontract]</a>
  1808. </p>
  1809. </td>
  1810. <td>
  1811. <p>
  1812. Java
  1813. </p>
  1814. </td>
  1815. <td>
  1816. <p>
  1817. This uses an external preprocessing tool.
  1818. </p>
  1819. </td>
  1820. </tr>
  1821. <tr>
  1822. <td>
  1823. <p>
  1824. <a class="link" href="bibliography.html#CodeContracts_anchor">[CodeContracts]</a>
  1825. </p>
  1826. </td>
  1827. <td>
  1828. <p>
  1829. .NET
  1830. </p>
  1831. </td>
  1832. <td>
  1833. <p>
  1834. Microsoft contract programming for .NET programming languages.
  1835. </p>
  1836. </td>
  1837. </tr>
  1838. <tr>
  1839. <td>
  1840. <p>
  1841. <a class="link" href="bibliography.html#SpecSharp_anchor">[SpecSharp]</a>
  1842. </p>
  1843. </td>
  1844. <td>
  1845. <p>
  1846. C#
  1847. </p>
  1848. </td>
  1849. <td>
  1850. <p>
  1851. This is a C# extension with contract programming language support.
  1852. </p>
  1853. </td>
  1854. </tr>
  1855. <tr>
  1856. <td>
  1857. <p>
  1858. <a class="link" href="bibliography.html#Chrome_anchor">[Chrome]</a>
  1859. </p>
  1860. </td>
  1861. <td>
  1862. <p>
  1863. Object Pascal
  1864. </p>
  1865. </td>
  1866. <td>
  1867. <p>
  1868. This is the .NET version of Object Pascal and it has language support
  1869. for contract programming.
  1870. </p>
  1871. </td>
  1872. </tr>
  1873. <tr>
  1874. <td>
  1875. <p>
  1876. <a class="link" href="bibliography.html#SPARKAda_anchor">[SPARKAda]</a>
  1877. </p>
  1878. </td>
  1879. <td>
  1880. <p>
  1881. Ada
  1882. </p>
  1883. </td>
  1884. <td>
  1885. <p>
  1886. This is an Ada-like programming language with support for contract
  1887. programming.
  1888. </p>
  1889. </td>
  1890. </tr>
  1891. </tbody>
  1892. <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>
  1893. <span class="bold"><strong>Rationale:</strong></span> Older versions of
  1894. this library also automatically generated Doxygen documentation
  1895. from contract definition macros. This functionality was abandoned
  1896. for a number of reasons: This library no longer uses macros to
  1897. program contracts; even before that, the implementation of this
  1898. library macros became too complex and the Doxygen preprocessor
  1899. was no longer able to expand them; the Doxygen documentation
  1900. was just a repeat of the contract code (so programmers could
  1901. directly look at contracts in the source code); Doxygen might
  1902. not necessarily be the documentation tool used by all C++ programmers.
  1903. </p></div></td></tr></tbody>
  1904. </table></div>
  1905. <p>
  1906. To the best knowledge of the authors, this the only library that fully supports
  1907. all contract programming features for C++ (without using preprocessing tools
  1908. external to the language itself). In general:
  1909. </p>
  1910. <div class="itemizedlist"><ul class="itemizedlist" style="list-style-type: disc; ">
  1911. <li class="listitem">
  1912. Implementing preconditions and postconditions in C++ is not difficult
  1913. (e.g., using some kind of RAII object).
  1914. </li>
  1915. <li class="listitem">
  1916. Implementing postcondition old values is also not too difficult (usually
  1917. requiring programmers to copy old values into local variables), but it
  1918. is already somewhat more difficult to ensure such copies are not performed
  1919. 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>
  1920. </li>
  1921. <li class="listitem">
  1922. Implementing class invariants is more involved (especially if done automatically,
  1923. without requiring programmers to manually invoke extra functions to check
  1924. 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
  1925. to not consider static and volatile functions not supporting static and
  1926. volatile invariants respectively.
  1927. </li>
  1928. <li class="listitem">
  1929. Implementing subcontracting involves a significant amount of complexity
  1930. and it seems to not be properly supported by any C++ library other than
  1931. this one (especially when handling multiple inheritance, correctly copying
  1932. postcondition old values across all overridden contracts deep in the
  1933. inheritance tree, and correctly reporting the return value to the postconditions
  1934. 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>
  1935. </li>
  1936. </ul></div>
  1937. </div>
  1938. <div class="footnotes">
  1939. <br><hr style="width:100; text-align:left;margin-left: 0">
  1940. <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>
  1941. The nomenclature of wide and narrow contracts has gained some popularity
  1942. in recent years in the C++ community (appearing in a number of more
  1943. recent proposals to add contract programming to the C++ standard, see
  1944. <a class="link" href="bibliography.html" title="Bibliography">Bibliography</a>). This
  1945. nomenclature is perfectly reasonable but it is not often used in this
  1946. document just because the authors usually prefer to explicitly say
  1947. "this operation has no preconditions..." or "this operation
  1948. has preconditions..." (this is just a matter of taste).
  1949. </p></div>
  1950. <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>
  1951. <span class="bold"><strong>Rationale:</strong></span> Contract assertions for
  1952. exception guarantees were first introduced by this library, they are
  1953. not part of <a class="link" href="bibliography.html#N1962_anchor">[N1962]</a> or other references
  1954. listed in the <a class="link" href="bibliography.html" title="Bibliography">Bibliography</a>
  1955. (even if exception safety guarantees have long been part of C++ STL
  1956. documentation).
  1957. </p></div>
  1958. <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>
  1959. <span class="bold"><strong>Rationale:</strong></span> Static and volatile class
  1960. invariants were first introduced by this library (simply to reflect
  1961. the fact that C++ supports also static and volatile public functions),
  1962. they are not part of <a class="link" href="bibliography.html#N1962_anchor">[N1962]</a> or
  1963. other references listed in the <a class="link" href="bibliography.html" title="Bibliography">Bibliography</a>.
  1964. </p></div>
  1965. <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>
  1966. <span class="bold"><strong>Rationale:</strong></span> <code class="computeroutput"><a class="link" href="../BOOST_CO_idm45394999743888.html" title="Macro BOOST_CONTRACT_DISABLE_THREADS">BOOST_CONTRACT_DISABLE_THREADS</a></code>
  1967. is named after <code class="computeroutput"><span class="identifier">BOOST_DISABLE_THREADS</span></code>.
  1968. </p></div>
  1969. <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>
  1970. Of course, if contracts are ill-written then contract programming is
  1971. of little use. However, it is less likely to have a bug in both the
  1972. function body and the contract than in the function body alone. For
  1973. example, consider the validation of a result in postconditions. Validating
  1974. the return value might seem redundant, but in this case we actually
  1975. want that redundancy. When programmers write a function, there is a
  1976. certain probability that they make a mistake in implementing the function
  1977. body. When programmers specify the result of the function in the postconditions,
  1978. there is also a certain probability that they make a mistake in writing
  1979. the contract. However, the probability that programmers make a mistake
  1980. twice (in both the body <span class="emphasis"><em>and</em></span> the contract) is in
  1981. general lower than the probability that the mistake is made only once
  1982. (in either the body <span class="emphasis"><em>or</em></span> the contract).
  1983. </p></div>
  1984. <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>
  1985. <span class="bold"><strong>Rationale:</strong></span> Postconditions for
  1986. destructors are not part of <a class="link" href="bibliography.html#N1962_anchor">[N1962]</a>
  1987. or other references listed in the <a class="link" href="bibliography.html" title="Bibliography">Bibliography</a>
  1988. (but with respect to <a class="link" href="bibliography.html#Meyer97_anchor">[Meyer97]</a>
  1989. it should be noted that Eiffel does not support static data members
  1990. and that might by why destructors do not have postconditions
  1991. in Eiffel). However, in principle there could be uses for destructor
  1992. postconditions so this library supports postconditions for destructors
  1993. (e.g., a class that counts object instances could use destructor
  1994. postconditions to assert that an instance counter stored in a
  1995. static data member is decreased by <code class="computeroutput"><span class="number">1</span></code>
  1996. because the object has been destructed).
  1997. </p></div>
  1998. <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>
  1999. Note that this is true when using C-style <code class="computeroutput"><span class="identifier">assert</span></code>
  2000. as well.
  2001. </p></div>
  2002. <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>
  2003. <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
  2004. 45</a> had not been fixed, this library could have been implemented
  2005. to generate a compile-time error when precondition assertions use non-public
  2006. members more similarly to Eiffel's implementation (but still, not necessary
  2007. the best approach for C++).
  2008. </p></div>
  2009. <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>
  2010. <span class="bold"><strong>Rationale:</strong></span> If the evaluation of a contract
  2011. assertion throws an exception, the assertion cannot be checked to be true
  2012. so the only safe thing to assume is that the assertion failed (indeed the
  2013. contract assertion checking failed) and call the contract failure handler
  2014. in this case also.
  2015. </p></div>
  2016. <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>
  2017. <span class="bold"><strong>Rationale:</strong></span> This customizable failure handling
  2018. 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>
  2019. and also to the one proposed in <a class="link" href="bibliography.html#N1962_anchor">[N1962]</a>.
  2020. </p></div>
  2021. <div id="ftn.boost_contract.contract_programming_overview.feature_summary.f4" class="footnote">
  2022. <p><a href="#boost_contract.contract_programming_overview.feature_summary.f4" class="para"><sup class="para">[16] </sup></a>
  2023. For example, the following pseudocode attempts to emulate old values
  2024. in <a class="link" href="bibliography.html#P0380_anchor">[P0380]</a>:
  2025. </p>
  2026. <pre class="programlisting"><span class="keyword">struct</span> <span class="identifier">scope_exit</span> <span class="special">{</span> <span class="comment">// RAII.</span>
  2027. <span class="keyword">template</span><span class="special">&lt;</span><span class="keyword">typename</span> <span class="identifier">F</span><span class="special">&gt;</span>
  2028. <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>
  2029. <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>
  2030. <span class="identifier">scope_exit</span><span class="special">(</span><span class="identifier">scope_exit</span> <span class="keyword">const</span><span class="special">&amp;)</span> <span class="special">=</span> <span class="keyword">delete</span><span class="special">;</span>
  2031. <span class="identifier">scope_exit</span><span class="special">&amp;</span> <span class="keyword">operator</span><span class="special">=(</span><span class="identifier">scope_exit</span> <span class="keyword">const</span><span class="special">&amp;)</span> <span class="special">=</span> <span class="keyword">delete</span><span class="special">;</span>
  2032. <span class="keyword">private</span><span class="special">:</span>
  2033. <span class="identifier">std</span><span class="special">::</span><span class="identifier">function</span><span class="special">&lt;</span><span class="keyword">void</span> <span class="special">()&gt;</span> <span class="identifier">f_</span><span class="special">;</span>
  2034. <span class="special">};</span>
  2035. <span class="keyword">void</span> <span class="identifier">fswap</span><span class="special">(</span><span class="identifier">file</span><span class="special">&amp;</span> <span class="identifier">x</span><span class="special">,</span> <span class="identifier">file</span><span class="special">&amp;</span> <span class="identifier">y</span><span class="special">)</span>
  2036. <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>
  2037. <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>
  2038. <span class="comment">// Cannot use [[ensures]] for postconditions so to emulate old values.</span>
  2039. <span class="special">{</span>
  2040. <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>
  2041. <span class="identifier">file</span> <span class="identifier">old_y</span> <span class="special">=</span> <span class="identifier">y</span><span class="special">;</span>
  2042. <span class="identifier">scope_exit</span> <span class="identifier">ensures</span><span class="special">([&amp;]</span> <span class="special">{</span> <span class="comment">// Check after local objects destroyed.</span>
  2043. <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>
  2044. <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>
  2045. <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>
  2046. <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>
  2047. <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>
  2048. <span class="special">}</span>
  2049. <span class="special">});</span>
  2050. <span class="identifier">x</span><span class="special">.</span><span class="identifier">open</span><span class="special">();</span>
  2051. <span class="identifier">scope_exit</span> <span class="identifier">close_x</span><span class="special">([&amp;]</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>
  2052. <span class="identifier">y</span><span class="special">.</span><span class="identifier">open</span><span class="special">();</span>
  2053. <span class="identifier">scope_exit</span> <span class="identifier">close_y</span><span class="special">([&amp;]</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>
  2054. <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>
  2055. <span class="identifier">z</span><span class="special">.</span><span class="identifier">open</span><span class="special">;</span>
  2056. <span class="identifier">scope_exit</span> <span class="identifier">close_z</span><span class="special">([&amp;]</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>
  2057. <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>
  2058. <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>
  2059. <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>
  2060. <span class="special">}</span>
  2061. </pre>
  2062. <p>
  2063. This requires boiler-plate code to make sure postconditions are correctly
  2064. 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
  2065. other local objects have been destroyed (because some of these destructors
  2066. contribute to establishing the postconditions). Still, it never disables
  2067. old value copies (not even if postconditions are disabled in release
  2068. builds, this would require adding even more boiler-plate code using
  2069. <code class="computeroutput"><span class="preprocessor">#ifdef</span></code>, etc.).
  2070. </p>
  2071. </div>
  2072. <div id="ftn.boost_contract.contract_programming_overview.feature_summary.f5" class="footnote">
  2073. <p><a href="#boost_contract.contract_programming_overview.feature_summary.f5" class="para"><sup class="para">[17] </sup></a>
  2074. For example, the following pseudocode attempts to emulation of class
  2075. invariants in <a class="link" href="bibliography.html#P0380_anchor">[P0380]</a>:
  2076. </p>
  2077. <pre class="programlisting"><span class="keyword">template</span><span class="special">&lt;</span><span class="keyword">typename</span> <span class="identifier">T</span><span class="special">&gt;</span>
  2078. <span class="keyword">class</span> <span class="identifier">vector</span> <span class="special">{</span>
  2079. <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>
  2080. <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>
  2081. <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">&lt;=</span> <span class="identifier">capacity</span><span class="special">()]]</span>
  2082. <span class="keyword">return</span> <span class="keyword">true</span><span class="special">;</span>
  2083. <span class="special">}</span>
  2084. <span class="keyword">public</span><span class="special">:</span>
  2085. <span class="identifier">vector</span><span class="special">()</span>
  2086. <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>
  2087. <span class="special">{</span> <span class="special">...</span> <span class="special">}</span>
  2088. <span class="special">~</span><span class="identifier">vector</span><span class="special">()</span> <span class="keyword">noexcept</span>
  2089. <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>
  2090. <span class="special">{</span> <span class="special">...</span> <span class="special">}</span>
  2091. <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">&amp;</span> <span class="identifier">value</span><span class="special">)</span>
  2092. <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>
  2093. <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>
  2094. <span class="keyword">try</span> <span class="special">{</span>
  2095. <span class="special">...</span> <span class="comment">// Function body.</span>
  2096. <span class="special">}</span> <span class="keyword">catch</span><span class="special">(...)</span> <span class="special">{</span>
  2097. <span class="identifier">invariant</span><span class="special">();</span> <span class="comment">// ...public function exit (if throw).</span>
  2098. <span class="keyword">throw</span><span class="special">;</span>
  2099. <span class="special">}</span>
  2100. <span class="special">...</span>
  2101. <span class="special">};</span>
  2102. </pre>
  2103. <p>
  2104. This requires boiler-plate code to manually invoke the function that
  2105. checks the invariants (note that invariants are checked at public function
  2106. exit regardless of exceptions being thrown while postconditions are
  2107. 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>),
  2108. the destructor also requires a <code class="computeroutput"><span class="keyword">try</span><span class="special">-</span><span class="keyword">catch</span></code>
  2109. statement similar to the one programmed for <code class="computeroutput"><span class="identifier">push_back</span></code>
  2110. to check class invariants at destructor exit when it throws exceptions.
  2111. Still, an outstanding issue remains to avoid infinite recursion if
  2112. also <code class="computeroutput"><span class="identifier">empty</span></code> and <code class="computeroutput"><span class="identifier">size</span></code> are public functions programmed
  2113. to check class invariants (because <a class="link" href="bibliography.html#P0380_anchor">[P0380]</a>
  2114. does not automatically disable assertions while checking other assertions).
  2115. </p>
  2116. </div>
  2117. <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>
  2118. For example, it is not really possible to sketch pseudocode based on
  2119. <a class="link" href="bibliography.html#P0380_anchor">[P0380]</a> that emulates subcontracting
  2120. in the general case.
  2121. </p></div>
  2122. </div>
  2123. </div>
  2124. <table xmlns:rev="http://www.cs.rpi.edu/~gregod/boost/tools/doc/revision" width="100%"><tr>
  2125. <td align="left"></td>
  2126. <td align="right"><div class="copyright-footer">Copyright &#169; 2008-2019 Lorenzo Caminiti<p>
  2127. Distributed under the Boost Software License, Version 1.0 (see accompanying
  2128. 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>)
  2129. </p>
  2130. </div></td>
  2131. </tr></table>
  2132. <hr>
  2133. <div class="spirit-nav">
  2134. <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>
  2135. </div>
  2136. </body>
  2137. </html>