Boost-Commit :

Date view	Thread view	Subject view	Author view

Subject: [Boost-commit] svn:boost r74227 - in sandbox/contract/libs/contract/doc/html2: . contract__
From: lorcaminiti_at_[hidden]
Date: 2011-09-04 13:37:17

Author: lcaminiti
Date: 2011-09-04 13:37:15 EDT (Sun, 04 Sep 2011)
New Revision: 74227
URL: http://svn.boost.org/trac/boost/changeset/74227

Log:
Upd docs.
Added:
   sandbox/contract/libs/contract/doc/html2/
   sandbox/contract/libs/contract/doc/html2/contract__/
   sandbox/contract/libs/contract/doc/html2/contract__/Examples.html (contents, props changed)
   sandbox/contract/libs/contract/doc/html2/contract__/bibliography.html (contents, props changed)
   sandbox/contract/libs/contract/doc/html2/contract__/grammar.html (contents, props changed)
   sandbox/contract/libs/contract/doc/html2/contract__/release_notes.html (contents, props changed)
   sandbox/contract/libs/contract/doc/html2/index.html (contents, props changed)

Added: sandbox/contract/libs/contract/doc/html2/contract__/Examples.html
==============================================================================
--- (empty file)
+++ sandbox/contract/libs/contract/doc/html2/contract__/Examples.html 2011-09-04 13:37:15 EDT (Sun, 04 Sep 2011)
@@ -0,0 +1,4470 @@
+<html>
+<head>
+<meta http-equiv="Content-Type" content="text/html; charset=US-ASCII">
+<title>Appendix: Examples</title>
+<link rel="stylesheet" href="../../../../../doc/src/boostbook.css" type="text/css">
+<meta name="generator" content="DocBook XSL Stylesheets V1.76.1">
+<link rel="home" href="../index.html" title="Contract++ 0.4.x">
+<link rel="up" href="../index.html" title="Contract++ 0.4.x">
+<link rel="prev" href="../index.html" title="Contract++ 0.4.x">
+<link rel="next" href="grammar.html" title="Appendix: Grammar">
+</head>
+<body bgcolor="white" text="black" link="#0000FF" vlink="#840084" alink="#0000FF">
+<table cellpadding="2" width="100%"><tr>
+<td valign="top"><img alt="Boost C++ Libraries" width="277" height="86" src="../../../../../boost.png"></td>
+<td align="center">Home</td>
+<td align="center">Libraries</td>
+<td align="center">People</td>
+<td align="center">FAQ</td>
+<td align="center">More</td>
+</tr></table>
+<hr>
+<div class="spirit-nav">
+<a accesskey="p" href="../index.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="grammar.html"><img src="../../../../../doc/src/images/next.png" alt="Next"></a>
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h2 class="title" style="clear: both">
+<a name="contract__.examples"></a><a class="link" href="examples.html" title="Appendix: Examples">Appendix: Examples</a>
+</h2></div></div></div>
+<div class="toc"><dl>
+<dt><a href="examples.html#contract__.examples.n1962_vector">[N1962] Vector: Comparison
+ with C++ proposal syntax</a></dt>
+<dt><a href="examples.html#contract__.examples.__n1962___circle__subcontracting">[N1962]
+ Circle: Subcontracting</a></dt>
+<dt><a href="examples.html#contract__.examples.__n1962___factorial__recursion_and_importance_ordering">[N1962]
+ Factorial: Recursion and importance ordering</a></dt>
+<dt><a href="examples.html#contract__.examples.__n1962___equal__operators">[N1962]
+ Equal: Operators</a></dt>
+<dt><a href="examples.html#contract__.examples.__n1962___sum__separated_body_definition">[N1962]
+ Sum: Separated body definition</a></dt>
+<dt><a href="examples.html#contract__.examples.__n1962___square_root__default_parameters">[N1962]
+ Square Root: Default parameters</a></dt>
+<dt><a href="examples.html#contract__.examples.__n1962___block__block_invariants">[N1962]
+ Block: Block invariants</a></dt>
+<dt><a href="examples.html#contract__.examples.n2081_add">[N2081] Add: Generic addition
+ algorithm</a></dt>
+<dt><a href="examples.html#contract__.examples.__n2081___advance__concept_based_iterator_overloading__emulated_using_tags_">[N2081]
+ Advance: Concept-based iterator overloading (emulated using tags)</a></dt>
+<dt><a href="examples.html#contract__.examples.__n2081___find__generic_find_algorithm">[N2081]
+ Find: Generic find algorithm</a></dt>
+<dt><a href="examples.html#contract__.examples.__n2081___apply__overloaded_invocation_of_functors">[N2081]
+ Apply: Overloaded invocation of functors</a></dt>
+<dt><a href="examples.html#contract__.examples.__n2081___for_each__generic_for_each_algorithm">[N2081]
+ For Each: Generic for-each algorithm</a></dt>
+<dt><a href="examples.html#contract__.examples.__n2081___transform__generic_binary_transformation_algorithm">[N2081]
+ Transform: Generic binary transformation algorithm</a></dt>
+<dt><a href="examples.html#contract__.examples.__n2081___count__generic_count_algorithm">[N2081]
+ Count: Generic count algorithm</a></dt>
+<dt><a href="examples.html#contract__.examples.__n2081___convert__conversion_between_two_types">[N2081]
+ Convert: Conversion between two types</a></dt>
+<dt><a href="examples.html#contract__.examples.__n2081___equal__generic_equality_comparison">[N2081]
+ Equal: Generic equality comparison</a></dt>
+<dt><a href="examples.html#contract__.examples.__n2081___less_equal__generic_less_than_or_equal_to_comparison">[N2081]
+ Less Equal: Generic less-than or equal-to comparison</a></dt>
+<dt><a href="examples.html#contract__.examples.__n2081___de_ref__generic_iterator_dereferencing">[N2081]
+ De-Ref: Generic iterator dereferencing</a></dt>
+<dt><a href="examples.html#contract__.examples.__n2081___min__generic_minimum_algorithm">[N2081]
+ Min: Generic minimum algorithm</a></dt>
+<dt><a href="examples.html#contract__.examples.meyer97_stack4">[Meyer97] Stack4:
+ Comparison with Eiffel syntax</a></dt>
+<dt><a href="examples.html#contract__.examples.__meyer97___stack3__error_codes_instead_of_preconditions">[Meyer97]
+ Stack3: Error codes instead of preconditions</a></dt>
+<dt><a href="examples.html#contract__.examples.meyer97_gcd">[Meyer97] GCD: Loop
+ variant and comparison with Eiffel syntax</a></dt>
+<dt><a href="examples.html#contract__.examples.__meyer97___max_array__nested_loop_variants">[Meyer97]
+ Max Array: Nested loop variants</a></dt>
+<dt><a href="examples.html#contract__.examples.__mitchell02___name_list__relaxing_subcontracts">[Mitchell02]
+ Name List: Relaxing subcontracts</a></dt>
+<dt><a href="examples.html#contract__.examples.__mitchell02___dictionary__simple_key_value_map">[Mitchell02]
+ Dictionary: Simple key-value map</a></dt>
+<dt><a href="examples.html#contract__.examples.__mitchell02___courier__subcontracting_and_static_class_invariants">[Mitchell02]
+ Courier: Subcontracting and static class invariants</a></dt>
+<dt><a href="examples.html#contract__.examples.__mitchell02___stack__simple_stack_dispenser">[Mitchell02]
+ Stack: Simple stack dispenser</a></dt>
+<dt><a href="examples.html#contract__.examples.__mitchell02___simple_queue__simple_queue_dispenser">[Mitchell02]
+ Simple Queue: Simple queue dispenser</a></dt>
+<dt><a href="examples.html#contract__.examples.__mitchell02___customer_manager__contracts_instead_of_defensive_programming">[Mitchell02]
+ Customer Manager: Contracts instead of Defensive Programming</a></dt>
+<dt><a href="examples.html#contract__.examples.__mitchell02___observer__contracts_for_pure_virtual_functions">[Mitchell02]
+ Observer: Contracts for pure virtual functions</a></dt>
+<dt><a href="examples.html#contract__.examples.mitchell02_counter">[Mitchell02]
+ Counter: Subcontracting and virtual specifiers (final, override, new, and pure)</a></dt>
+<dt><a href="examples.html#contract__.examples.__stroustrup97___string__throw_when_contract_is_broken">[Stroustrup97]
+ String: Throw when contract is broken</a></dt>
+<dt><a href="examples.html#contract__.examples.cline90_vector">[Cline90] Vector:
+ Comparison with A++ proposal syntax</a></dt>
+<dt><a href="examples.html#contract__.examples.__cline90___vector_stack__subcontracting_from_abstract_data_type">[Cline90]
+ Vector-Stack: Subcontracting from Abstract Data Type</a></dt>
+<dt><a href="examples.html#contract__.examples.__cline90___stack__a_very_simple_stack">[Cline90]
+ Stack: A very simple stack</a></dt>
+<dt><a href="examples.html#contract__.examples.__cline90___calendar__a_very_simple_calendar">[Cline90]
+ Calendar: A very simple calendar</a></dt>
+</dl></div>
+
+ This section lists quite a few examples programmed using this library and taken
+ from a number of different sources (which are referenced in the example title):
+ 
+<div class="itemizedlist"><ul class="itemizedlist" type="disc">
+<li class="listitem">
+ <a class="link" href="bibliography.html" title="Bibliography">[N1962]</a> contains examples
+ from the proposal to add Contract Programming submitted to the C++ standard
+ committee (not accepted into the standard).
+ </li>
+<li class="listitem">
+ <a class="link" href="bibliography.html" title="Bibliography">[N2081]</a> contains examples
+ from the proposal to add Concept Programming submitted to the C++ standard
+ committee (not accepted into the standard). These examples have been extended
+ here to specify both compile-time and run-time interface requirements using
+ concepts and contracts respectively.
+ </li>
+<li class="listitem">
+ <a class="link" href="bibliography.html" title="Bibliography">[Meyer97]</a> and <a class="link" href="bibliography.html" title="Bibliography">[Mitchell02]</a>
+ contain examples using the Eiffel programming language.
+ </li>
+<li class="listitem">
+ <a class="link" href="bibliography.html" title="Bibliography">[Cline90]</a> contains examples
+ from a very early proposal called Annotated C++ (A++) to extend C++ with
+ Contract Programming (A++ was never actually implemented).
+ </li>
+<li class="listitem">
+ <a class="link" href="bibliography.html" title="Bibliography">[Stroustrup97]</a> contains
+ one example that shows the importance of class invariants and how to configure
+ this library to throw exceptions instead of terminating the program when
+ a contract is broken.
+ </li>
+</ul></div>
+
+ The followings are among the most interesting examples:
+ 
+<div class="itemizedlist"><ul class="itemizedlist" type="disc">
+<li class="listitem">
+ Comparison with syntax from C++ Contract and Concept Programming proposals
+ (see <a class="link" href="examples.html#contract__.examples.n1962_vector" title="[N1962] Vector: Comparison with C++ proposal syntax">here</a>) and
+ with a user-defined concept (see <a class="link" href="examples.html#contract__.examples.n2081_add" title="[N2081] Add: Generic addition algorithm">here</a>).
+ </li>
+<li class="listitem">
+ Subcontracting and C++0x-like virtual specifiers <code class="computeroutput">final</code>,
+ <code class="computeroutput">override</code>, and <code class="computeroutput">new</code> (see <a class="link" href="examples.html#contract__.examples.mitchell02_counter" title="[Mitchell02] Counter: Subcontracting and virtual specifiers (final, override, new, and pure)">here</a>).
+ </li>
+<li class="listitem">
+ Comparison with Eiffel syntax (see <a class="link" href="examples.html#contract__.examples.meyer97_stack4" title="[Meyer97] Stack4: Comparison with Eiffel syntax">here</a>)
+ and for loop variants (see <a class="link" href="examples.html#contract__.examples.meyer97_gcd" title="[Meyer97] GCD: Loop variant and comparison with Eiffel syntax">here</a>).
+ </li>
+<li class="listitem">
+ Comparison with A++ syntax (see <a class="link" href="examples.html#contract__.examples.cline90_vector" title="[Cline90] Vector: Comparison with A++ proposal syntax">here</a>).
+ </li>
+</ul></div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.examples.n1962_vector"></a><a class="link" href="examples.html#contract__.examples.n1962_vector" title="[N1962] Vector: Comparison with C++ proposal syntax">[N1962] Vector: Comparison
+ with C++ proposal syntax</a>
+</h3></div></div></div>
+<div class="informaltable"><table class="table">
+<colgroup>
+<col>
+<col>
+</colgroup>
+<thead><tr>
+<th>
+ 
+ ISO C++ (this library)
+ 
+ </th>
+<th>
+ 
+ C++ Proposals (<a class="link" href="bibliography.html" title="Bibliography">[N1962]</a>,
+ <a class="link" href="bibliography.html" title="Bibliography">[N2081]</a>, etc)
+ 
+ </th>
+</tr></thead>
+<tbody><tr>
+<td>
+ 
+
+
+<pre xmlns:rev="http://www.cs.rpi.edu/~gregod/boost/tools/doc/revision" class="table-programlisting">#include <contract.hpp>
+#include <boost/utility.hpp> // For boost::prior().
+#include <boost/concept_check.hpp>
+#include <iterator>
+#include <vector>
+
+// Tools (forward declared, see actual declarations at the bottom).
+
+template< class Iter, class T >
+bool all_equals ( Iter first, Iter last, const T& val ) ;
+
+template< class Iter, class Size >
+bool equal_distance ( Iter first, Iter last, Size size ) ;
+
+// New vector interface (with contracts).
+
+CONTRACT_CLASS(
+template( class T, class Alloc, default std::allocator<T> )
+class (vector) // No base classes so no subcontracting for this example.
+) {
+ CONTRACT_CLASS_INVARIANT_TPL( // At very beginning of the class declaration.
+ empty() == (size() == 0),
+ int(size()) == std::distance(begin(), end()),
+ int(size()) == std::distance(rbegin(), rend()),
+ size() <= capacity(),
+ capacity() <= max_size()
+ ) // No static or volatile class invariants for this example.
+
+public:
+ typedef typename std::vector<T, Alloc>::allocator_type allocator_type;
+ typedef typename std::vector<T, Alloc>::pointer pointer;
+ typedef typename std::vector<T, Alloc>::const_pointer const_pointer;
+ typedef typename std::vector<T, Alloc>::reference reference;
+ typedef typename std::vector<T, Alloc>::const_reference const_reference;
+ typedef typename std::vector<T, Alloc>::value_type value_type;
+ typedef typename std::vector<T, Alloc>::iterator iterator;
+ typedef typename std::vector<T, Alloc>::const_iterator const_iterator;
+ typedef typename std::vector<T, Alloc>::size_type size_type;
+ typedef typename std::vector<T, Alloc>::difference_type difference_type;
+ typedef typename std::vector<T, Alloc>::reverse_iterator reverse_iterator;
+ typedef typename std::vector<T, Alloc>::const_reverse_iterator
+ const_reverse_iterator;
+
+ CONTRACT_CONSTRUCTOR_TPL(
+ public (vector) ( void ) // Must always specify the access level (public).
+ initialize( vect_() ) // Member initializers.
+ postcondition( empty() == false )
+ ) {}
+
+ CONTRACT_CONSTRUCTOR_TPL(
+ public explicit (vector) ( (const Alloc&) al )
+ initialize( vect_(al) )
+ postcondition( empty(), al == get_allocator() )
+ ) {}
+
+ CONTRACT_CONSTRUCTOR_TPL(
+ public explicit (vector) ( (size_type) count )
+ initialize( vect_(count) )
+ postcondition( size() == count, all_equals(begin(), end(), T()) )
+ ) {}
+
+ CONTRACT_CONSTRUCTOR_TPL(
+ public (vector) ( (size_type) count, (const T&) val )
+ initialize( vect_(count, val) )
+ postcondition( size() == count, all_equals(begin(), end(), val) )
+ ) {}
+
+ CONTRACT_CONSTRUCTOR_TPL(
+ public (vector) ( (size_type) count, (const T&) val, (const Alloc&) al )
+ initialize( vect_(count, val, al) )
+ postcondition(
+ size() == count,
+ all_equals(begin(), end(), val),
+ al == get_allocator()
+ )
+ ) {}
+
+ CONTRACT_CONSTRUCTOR_TPL(
+ public template( class InIt ) requires( boost::InputIterator<InIt> ) // Concept.
+ (vector) ( (InIt) first, (InIt) last )
+ initialize( vect_(first, last) )
+ postcondition( equal_distance(first, last, size()) )
+ ) {}
+
+ CONTRACT_CONSTRUCTOR_TPL(
+ public template( class InIt ) requires( boost::InputIterator<InIt> )
+ (vector) ( (InIt) first, (InIt) last, (const Alloc&) al )
+ initialize( vect_(first, last, al) )
+ postcondition(
+ equal_distance(first, last, size()),
+ al == get_allocator()
+ )
+ ) {}
+
+ CONTRACT_CONSTRUCTOR_TPL(
+ public (vector) ( (const vector&) right )
+ initialize( vect_(right.vect_) )
+ postcondition( right == *this )
+ ) {}
+
+ CONTRACT_FUNCTION_TPL( // Operator symbol followed by (arbitrary) name `copy`.
+ public (vector&) operator(=)(copy) ( (const vector&) right )
+ postcondition(
+ auto result = return,
+ right == *this,
+ result == *this
+ )
+ ) {
+ return vect_ = right.vect_;
+ }
+
+ CONTRACT_DESTRUCTOR_TPL( // Contract destructor so to check class
+ public virtual (~vector) ( void ) // invariants when object is destroyed.
+ ) {}
+
+ CONTRACT_FUNCTION_TPL(
+ // No required wrapping parenthesis for keyword types like `void`, `bool`, etc.
+ public void (reserve) ( (size_type) count )
+ precondition( count < max_size() )
+ postcondition( capacity() >= count )
+ ) {
+ vect_.reserve(count);
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public (size_type) (capacity) ( void ) const // Constant member.
+ postcondition( auto result = return, result >= size() ) // With result.
+ ) {
+ return vect_.capacity();
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public (iterator) (begin) ( void )
+ postcondition(
+ auto result = return,
+ if(empty()) ( result == end() ) // If-guarded assertion.
+ )
+ ) {
+ return vect_.begin();
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public (const_iterator) (begin) ( void ) const // Overload above member.
+ postcondition( auto result = return, if(empty()) ( result == end() ) )
+ ) {
+ return vect_.begin();
+ }
+
+ CONTRACT_FUNCTION_TPL( // Contract members even if no pre/post
+ public (iterator) (end) ( void ) // conditions so to check class invariants.
+ ) {
+ return vect_.end();
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public (const_iterator) (end) ( void ) const
+ ) {
+ return vect_.end();
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public (reverse_iterator) (rbegin) ( void )
+ postcondition( auto result = return, if(empty()) ( result == rend() ) )
+ ) {
+ return vect_.rbegin();
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public (const_reverse_iterator) (rbegin) ( void ) const
+ postcondition( auto result = return, if(empty()) ( result == rend() ) )
+ ) {
+ return vect_.rbegin();
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public (reverse_iterator) (rend) ( void )
+ ) {
+ return vect_.rend();
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public (const_reverse_iterator) (rend) ( void ) const
+ ) {
+ return vect_.rend();
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public void (resize) ( (size_type) newsize )
+ postcondition(
+ auto old_size = CONTRACT_OLDOF size(), // Old value (as before body).
+ size() == newsize,
+ if(newsize > old_size) ( // Version 1: Within an `if`.
+ all_equals(begin() + old_size, end(), T())
+ ) // Omitted optional `else( ... )`.
+ )
+ ) {
+ vect_.resize(newsize);
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public void (resize) ( (size_type) newsize, (T) val )
+ postcondition(
+ (size_type) old_size = CONTRACT_OLDOF size(), // Specify old type.
+ size() == newsize,
+ newsize > old_size ? // Version 2: With ternary operator.
+ all_equals(begin() + old_size, end(), val) : true
+ )
+ ) {
+ vect_.resize(newsize, val);
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public (size_type) (size) ( void ) const
+ postcondition( auto result = return, result <= capacity() )
+ ) {
+ return vect_.size();
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public (size_type) (max_size) ( void ) const
+ postcondition( auto result = return, result >= capacity() )
+ ) {
+ return vect_.max_size();
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public bool (empty) ( void ) const
+ postcondition( auto result = return, result == (size() == 0) )
+ ) {
+ return vect_.empty();
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public (Alloc) (get_allocator) ( void ) const
+ ) {
+ return vect_.get_allocator();
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public (reference) (at) ( (size_type) off )
+ precondition( off < size() )
+ ) {
+ return vect_.at(off);
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public (const_reference) (at) ( (size_type) off ) const
+ precondition( off < size() )
+ ) {
+ return vect_.at(off);
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public (reference) operator([])(at) ( (size_type) off )
+ precondition( off < size() )
+ ) {
+ return vect_[off];
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public (const_reference) operator([])(at) ( (size_type) off ) const
+ precondition( off < size() )
+ ) {
+ return vect_[off];
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public (reference) (front) ( void )
+ precondition( bool(!empty()) ) // bool for leading non alphanumeric `!`.
+ ) {
+ return vect_.front();
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public (const_reference) (front) ( void ) const
+ precondition( empty() == false ) // Or, `== false` instead of `!`.
+ ) {
+ return vect_.front();
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public (reference) (back) ( void )
+ precondition( empty() == false )
+ ) {
+ return vect_.back();
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public (const_reference) (back) ( void ) const
+ precondition( empty() == false )
+ ) {
+ return vect_.back();
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public void (push_back) ( (const T&) val )
+ precondition( size() < max_size() )
+ postcondition(
+ auto old_size = CONTRACT_OLDOF size(),
+ auto old_capacity = CONTRACT_OLDOF capacity(),
+ back() == val,
+ size() == old_size + 1,
+ capacity() >= old_capacity
+ )
+ ) {
+ vect_.push_back(val);
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public void (pop_back) ( void )
+ precondition( empty() == false )
+ postcondition(
+ auto old_size = CONTRACT_OLDOF size(),
+ size() == old_size - 1
+ )
+ ) {
+ vect_.pop_back();
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public template( class InIt ) requires( boost::InputIterator<InIt> )
+ void (assign) ( (InIt) first, (InIt) last )
+ // Precondition: [first, last) is not a sub-range of [begin(), end()).
+ postcondition( equal_distance(first, last, size()) )
+ ) {
+ vect_.assign(first, last);
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public void (assign) ( (size_type) count, (const T&) val )
+ precondition( count <= max_size() )
+ postcondition( all_equals(begin(), end(), val) )
+ ) {
+ vect_.assign(count, val);
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public (iterator) (insert) ( (iterator) pos, (const T&) val )
+ precondition( size() < max_size() )
+ postcondition(
+ auto result = return,
+ auto old_size = CONTRACT_OLDOF size(),
+ val == *result,
+ size() == old_size + 1
+ // if(capacity() > oldof capacity()): [begin(), end()] invalid
+ // else: [pos, end()) invalid
+ )
+ ) {
+ return vect_.insert(pos, val);
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public void (insert) ( (iterator) pos, (size_type) count, (const T&) val )
+ precondition( size() + count < max_size() )
+ postcondition(
+ auto old_size = CONTRACT_OLDOF size(),
+ auto old_capacity = CONTRACT_OLDOF capacity(),
+ auto old_pos = CONTRACT_OLDOF pos,
+ size() == old_size + count,
+ capacity() >= old_capacity,
+ if(capacity() == old_capacity) (
+ all_equals(boost::prior(old_pos),
+ boost::prior(old_pos) + count, val)
+ // [pos, end()) invalid
+ ) // else: [begin(), end()) invalid
+ )
+ ) {
+ vect_.insert(pos, count, val);
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public template( class InIt )
+ void (insert) ( (iterator) pos, (InIt) first, (InIt) last )
+ precondition(
+ // [first, last) not a sub-range of [begin(), end())
+ size() + std::distance(first, last) < max_size()
+ )
+ postcondition(
+ auto old_size = CONTRACT_OLDOF size(),
+ auto old_capacity = CONTRACT_OLDOF capacity(),
+ size() == old_size + std::distance(first, last),
+ capacity() >= old_capacity
+ )
+ ) {
+ vect_.insert(pos, first, last);
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public (iterator) (erase) ( (iterator) pos )
+ precondition(
+ empty() == false,
+ pos != end()
+ )
+ postcondition(
+ auto result = return,
+ auto old_size = CONTRACT_OLDOF size(),
+ size() == old_size = 1,
+ if(empty()) ( result == end() )
+ // [pos, end()) invalid
+ )
+ ) {
+ return vect_.erase();
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public (iterator) (erase) ( (iterator) first, (iterator) last )
+ precondition( size() >= std::distance(first, last) )
+ postcondition(
+ auto result = return,
+ auto old_size = CONTRACT_OLDOF size(),
+ size() == old_size - std::distance(first, last),
+ if(empty()) ( result == end() )
+ // [first, last) invalid
+ )
+ ) {
+ return vect_.erase(first, last);
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public void (clear) ( void )
+ postcondition( empty() )
+ ) {
+ vect_.clear();
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public void (swap) ( (vector&) right )
+ postcondition(
+ auto old_self = CONTRACT_OLDOF *this,
+ auto old_right = CONTRACT_OLDOF right,
+ old_self == right,
+ old_right == *this
+ )
+ ) {
+ vect_.swap(right);
+ }
+
+private:
+ std::vector<T, Alloc> vect_;
+};
+
+CONTRACT_FUNCTION_TPL(
+template( class Iter, class T )
+ requires(
+ boost::ForwardIterator<Iter>,
+ boost::EqualityComparable<T> // For simplicity, assume T comparable.
+ )
+bool (all_equals) ( (Iter) first, (Iter) last, (const T&) val )
+) {
+ for(Iter i = first; i < last; ++i) if(*i != val) return false;
+ return true;
+}
+
+CONTRACT_FUNCTION_TPL(
+template( class Iter, class Size )
+ requires(
+ // Could use internal tagging mechanism to pass even input iterators.
+ boost::ForwardIterator<Iter>,
+ // IDENTITY_TYPE to handle unwrapped commas within macro parameters.
+ typename CONTRACT_IDENTITY_TYPE((boost::Convertible<Size, int>))
+ )
+bool (equal_distance) ( (Iter) first, (Iter) last, (Size) size )
+) {
+ return int(size) == std::distance(first, last);
+}
+
+CONTRACT_FUNCTION_TPL(
+template( class T ) requires( boost::EqualityComparable<T> )
+bool operator(==)(equal) ( (const vector<T>&) left, (const vector<T>&) right )
+ postcondition(
+ auto result = return,
+ if(result) (
+ left.size() == right.size()
+ // left and right values are all equal to each other.
+ )
+ )
+) {
+ if(left.size() != right.size()) return false;
+ for(typename vector<T>::const_iterator
+ l = left.begin(), r = right.begin(); l != left.end(); ++l, ++r)
+ if(*l != *r) return false;
+ return true;
+}
+</pre>
+
+ 
+ </td>
+<td>
+ 
+
+
+<pre xmlns:rev="http://www.cs.rpi.edu/~gregod/boost/tools/doc/revision" class="table-programlisting">// Extra spacing and newlines used to visually align with this library code.
+#include <boost/utility.hpp>
+#include <concepts>
+#include <iterator>
+#include <vector>
+
+
+
+template< class Iter, class T >
+bool all_equals ( Iter first, Iter last, const T& val ) ;
+
+template< class Iter, class Size >
+bool equal_distance ( Iter first, Iter last, Size size ) ;
+
+
+
+
+template< class T, class Alloc = std::allocator<T> >
+class vector
+{
+ invariant {
+ empty() == (size() == 0);
+ int(size()) == std::distance(begin(), end());
+ int(size()) == std::distance(rbegin(), rend());
+ size() <= capacity();
+ capacity() <= max_size();
+ }
+
+public:
+ typedef typename std::vector<T, Alloc>::allocator_type allocator_type;
+ typedef typename std::vector<T, Alloc>::pointer pointer;
+ typedef typename std::vector<T, Alloc>::const_pointer const_pointer;
+ typedef typename std::vector<T, Alloc>::reference reference;
+ typedef typename std::vector<T, Alloc>::const_reference const_reference;
+ typedef typename std::vector<T, Alloc>::value_type value_type;
+ typedef typename std::vector<T, Alloc>::iterator iterator;
+ typedef typename std::vector<T, Alloc>::const_iterator const_iterator;
+ typedef typename std::vector<T, Alloc>::size_type size_type;
+ typedef typename std::vector<T, Alloc>::difference_type difference_type;
+ typedef typename std::vector<T, Alloc>::reverse_iterator reverse_iterator;
+ typedef typename std::vector<T, Alloc>::const_reverse_iterator
+ const_reverse_iterator;
+
+ // `public:` and `void` used to visually align with this library code.
+ public: vector ( void )
+ : vect_()
+ postcondition { empty() == false; }
+ {}
+
+
+ public: explicit vector ( const Alloc& al )
+ : vect_(al)
+ postcondition { empty(); al == get_allocator(); }
+ {}
+
+
+ public: explicit vector ( size_type count )
+ : vect_(count)
+ postcondition { size() == count; all_equals(begin(), end(), T()); }
+ {}
+
+
+ public: vector ( size_type count, const T& val )
+ : vect_(count, val)
+ postcondition { size() == count; all_equals(begin(), end(), val); }
+ {}
+
+
+ public: vector ( size_type count, const T& val, const Alloc& al )
+ : vect_(count, val, al)
+ postcondition {
+ size() == count;
+ all_equals(begin(), end(), val);
+ al == get_allocator();
+ }
+ {}
+
+
+ public: template< class InIt > requires std::InputIterator<InIt>
+ vector ( InIt first, InIt last )
+ : vect_(first, last)
+ postcondition { equal_distance(first, last, size()); }
+ {}
+
+
+ public: template< class InIt > requires std::InputIterator<InIt>
+ vector ( InIt first, InIt last, const Alloc& al )
+ : vect_(first, last, al)
+ postcondition {
+ equal_distance(first, last, size());
+ al == get_allocator();
+ }
+ {}
+
+
+ public: vector ( const vector& right )
+ : vect_(right.vect_)
+ postcondition { right == *this; }
+ {}
+
+
+ public: vector& operator= ( const vector& right )
+ postcondition(result) {
+
+ right == *this;
+ result == *this;
+ }
+ {
+ return vect_ = right.vect_;
+ }
+
+
+ public: virtual ~vector ( void )
+ {}
+
+
+
+ public: void reserve ( size_type count )
+ precondition { count < max_size(); }
+ postcondition { capacity() >= count; }
+ {
+ vect_.reserve(count);
+ }
+
+
+ public: size_type capacity ( void ) const
+ postcondition(result) { result >= size(); }
+ {
+ return vect_.capacity();
+ }
+
+
+ public: iterator begin ( void )
+ postcondition {
+
+ if(empty()) result == end();
+ }
+ {
+ return vect_.begin();
+ }
+
+
+ public: const_iterator begin ( void ) const
+ postcondition(result) { if(empty()) result == end(); }
+ {
+ return vect_.begin();
+ }
+
+
+ public: iterator end ( void )
+ {
+ return vect_.end();
+ }
+
+
+ public: const_iterator end ( void ) const
+ {
+ return vect_.end();
+ }
+
+
+ public: reverse_iterator rbegin ( void )
+ postcondition(result) { if(empty()) result == rend(); }
+ {
+ return vect_.rbegin();
+ }
+
+
+ public: const_reverse_iterator rbegin ( void ) const
+ postcondition(result) { if(empty()) result == rend(); }
+ {
+ return vect_.rbegin();
+ }
+
+
+ public: reverse_iterator rend ( void )
+ {
+ return vect_.rend();
+ }
+
+
+ public: const_reverse_iterator rend ( void ) const
+ {
+ return vect_.rend();
+ }
+
+
+ public: void resize ( size_type newsize )
+ postcondition {
+
+ size() == newsize;
+ if(newsize > oldof size()) {
+ all_equals(begin() + oldof size(), end(), T());
+ }
+ }
+ {
+ vect_.resize(newsize);
+ }
+
+
+ public: void resize ( size_type newsize, T val )
+ postcondition {
+
+ size() == newsize;
+ newsize > oldof size() ?
+ all_equals(begin() + oldof size(), end(), val) : true;
+ }
+ {
+ vect_.resize(newsize, val);
+ }
+
+
+ public: size_type size ( void ) const
+ postcondition(result) { result <= capacity(); }
+ {
+ return vect_.size();
+ }
+
+
+ public: size_type max_size ( void ) const
+ postcondition(result) { result >= capacity(); }
+ {
+ return vect_.max_size();
+ }
+
+
+ public: bool empty ( void ) const
+ postcondition(result) { result == (size() == 0); }
+ {
+ return vect_.empty();
+ }
+
+
+ public: Alloc get_allocator ( void ) const
+ {
+ return vect_.get_allocator();
+ }
+
+
+ public: reference at ( size_type off )
+ precondition { off < size(); }
+ {
+ return vect_.at(off);
+ }
+
+
+ public: const_reference at ( size_type off ) const
+ precondition { off < size(); }
+ {
+ return vect_.at(off);
+ }
+
+
+ public: reference operator[] ( size_type off )
+ precondition { off < size(); }
+ {
+ return vect_[off];
+ }
+
+
+ public: const_reference operator[] ( size_type off ) const
+ precondition { off < size(); }
+ {
+ return vect_[off];
+ }
+
+
+ public: reference front ( void )
+ precondition { !empty(); }
+ {
+ return vect_.front();
+ }
+
+
+ public: const_reference front ( void ) const
+ precondition { empty() == false; }
+ {
+ return vect_.front();
+ }
+
+
+ public: reference back ( void )
+ precondition { empty() == false; }
+ {
+ return vect_.back();
+ }
+
+
+ public: const_reference back ( void ) const
+ precondition { empty() == false; }
+ {
+ return vect_.back();
+ }
+
+
+ public void push_back ( const T& val )
+ precondition { size() < max_size() }
+ postcondition {
+
+
+ back() == val;
+ size() == oldof size() + 1;
+ capacity() >= oldof capacity()
+ }
+ {
+ vect_.push_back(val);
+ }
+
+
+ public: void pop_back ( void )
+ precondition { empty() == false; }
+ postcondition {
+
+ size() == oldof size() - 1;
+ }
+ {
+ vect_.pop_back();
+ }
+
+
+ public: template< class InIt > requires std::InputIterator<InIt>
+ void assign ( InIt first, InIt last )
+
+ postcondition { equal_distance(first, last, size()); }
+ {
+ vect_.assign(first, last);
+ }
+
+
+ public: void assign ( size_type count, const T& val )
+ precondition { count <= max_size(); }
+ postcondition { all_equals(begin(), end(), val); }
+ {
+ vect_.assign(count, val);
+ }
+
+
+ public: iterator insert ( iterator pos, const T& val )
+ precondition { size() < max_size(); }
+ postcondition(result) {
+
+
+ val == *result;
+ size() == oldof size() + 1;
+
+
+ }
+ {
+ return vect_.insert(pos, val);
+ }
+
+
+ public: void insert ( iterator pos, size_type count, const T& val )
+ precondition { size() + count < max_size(); }
+ postcondition {
+
+
+
+ size() == oldof size() + count;
+ capacity() >= oldof capacity();
+ if(capacity() == oldof capacity()) {
+ all_equals(boost::prior(oldof pos),
+ boost::prior(oldof pos) + count, val);
+
+ }
+ }
+ {
+ vect_.insert(pos, count, val);
+ }
+
+
+ public: template< class InIt >
+ void insert ( iterator pos, InIt first, InIt last )
+ precondition {
+
+ size() + std::distance(first, last) < max_size();
+ }
+ postcondition {
+
+
+ size() == oldof size() + std::distance(first, last);
+ capacity() >= oldof capacity();
+ }
+ {
+ vect_.insert(pos, first, last);
+ }
+
+
+ public: iterator erase ( iterator pos )
+ precondition {
+ empty() == false;
+ pos != end();
+ }
+ postcondition(result) {
+
+
+ size() == oldod size() = 1;
+ if(empty()) result == end();
+
+ }
+ {
+ return vect_.erase();
+ }
+
+
+ public: iterator erase ( iterator first, iterator last )
+ precondition { size() >= std::distance(first, lasst); }
+ postcondition(result) {
+
+
+ size() == oldof size() - std::distance(first, last);
+ if(empty()) result == end();
+
+ }
+ {
+ return vect_.erase(first, last);
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public void (clear) ( void )
+ postcondition( empty() )
+ ) {
+ vect_.clear();
+ }
+
+
+ public: void swap ( vector& right )
+ postcondition {
+
+
+ oldof *this == right;
+ oldof right == *this;
+ }
+ {
+ vect_.swap(right);
+ }
+
+private:
+ std::vector<T, Alloc> vect_;
+};
+
+
+template< class Iter, class T >
+ requires
+ boost::ForwardIterator<Iter>,
+ boost::EqualityComparable<T>
+
+bool all_equals ( Iter first, Iter last, const T& val )
+{
+ for(Iter i = first; i < last; ++i) if(*i != val) return false;
+ return true;
+}
+
+
+template< class Iter, class Size >
+ requires
+
+ boost::ForwardIterator<Iter>,
+
+ typename CONTRACT_IDENTITY_TYPE((boost::Convertible<Size, int>))
+
+bool equal_distance ( Iter first, Iter last, Size size )
+{
+ return int(size) == std::distance(first, last);
+}
+
+
+template< class T > requires boost::EqualityComparable<T>
+bool operator== ( const vector<T>& left, const vector<T>& right )
+ postcondition(result) {
+
+ if(result) {
+ left.size() == right.size();
+
+ }
+ }
+{
+ if(left.size() != right.size()) return false;
+ for(typename vector<T>::const_iterator
+ l = left.begin(), r = right.begin(); l != left.end(); ++l, ++r)
+ if(*l != *r) return false;
+ return true;
+}
+</pre>
+
+ 
+ </td>
+</tr></tbody>
+</table></div>
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.examples.__n1962___circle__subcontracting"></a><a class="link" href="examples.html#contract__.examples.__n1962___circle__subcontracting" title="[N1962] Circle: Subcontracting">[N1962]
+ Circle: Subcontracting</a>
+</h3></div></div></div>
+
+
+
+<pre class="programlisting">#include <contract.hpp>
+
+CONTRACT_CLASS(
+class (shape)
+) {
+ CONTRACT_CLASS_INVARIANT( void ) // Must always specify class invariants.
+
+public:
+ CONTRACT_DESTRUCTOR(
+ public virtual (~shape) ( void )
+ ) {}
+
+ CONTRACT_FUNCTION(
+ public virtual int (compute_area) ( void ) const
+ postcondition(
+ auto result = return,
+ result > 0
+ )
+ ) = 0; // Contracts also for pure virtual functions.
+};
+
+CONTRACT_CLASS(
+class (circle) extends( public shape )
+) {
+ CONTRACT_CLASS_INVARIANT( void ) // In AND with base class invariants.
+
+public:
+ int radius() const { return 2; } // For simplicity, hard-code radius.
+
+ CONTRACT_FUNCTION( // Also optional override specifier.
+ public virtual int (compute_area) ( void ) const override
+ // Eventual preconditions in OR with base function preconditions.
+ postcondition( // In AND with base function postconditions.
+ auto result = return,
+ result == PI * radius() * radius()
+ )
+ ) {
+ return PI * radius() * radius();
+ }
+
+private:
+ static const int PI = 3; // Truncated from 3.14...
+};
+</pre>
+
+ 
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.examples.__n1962___factorial__recursion_and_importance_ordering"></a><a class="link" href="examples.html#contract__.examples.__n1962___factorial__recursion_and_importance_ordering" title="[N1962] Factorial: Recursion and importance ordering">[N1962]
+ Factorial: Recursion and importance ordering</a>
+</h3></div></div></div>
+
+
+
+<pre class="programlisting">#include <contract.hpp>
+
+// Assertion importance used to model computational complexity.
+#define O_1 0 // O(1) constant (default).
+#define O_N 1 // O(n) linear.
+#define O_NN 2 // O(n * n) quadratic.
+#define O_NX 3 // O(n^x) polynomial.
+#define O_FACTN 4 // O(n!) factorial.
+#define O_EXPN 5 // O(e^n) exponential.
+
+CONTRACT_FUNCTION(
+int (factorial) ( int n )
+ precondition(
+ n >= 0,
+ n <= 12 // Max function input.
+ )
+ postcondition(
+ auto result = return,
+ result >= 1,
+ if(n < 2) ( // Select assertion.
+ result == 1
+ ) else (
+ // Contracts disable assertions within assertion checking so
+ // this postcondition can recursively call the function without
+ // causing infinite recursion. Moreover, this check adds
+ // significant run-time overhead so assertion importance is used to
+ // allow to selectively disable it.
+ result == n * factorial(n - 1), importance O_FACTN
+ )
+ )
+) {
+ if(n < 2) return 1;
+ else return n * factorial(n - 1);
+}
+</pre>
+
+ 
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.examples.__n1962___equal__operators"></a><a class="link" href="examples.html#contract__.examples.__n1962___equal__operators" title="[N1962] Equal: Operators">[N1962]
+ Equal: Operators</a>
+</h3></div></div></div>
+
+
+
+<pre class="programlisting">// In header: equal.hpp
+#include "equal_not.hpp"
+#include <contract.hpp>
+
+CONTRACT_FUNCTION_TPL(
+template( typename T )
+bool operator(==)(equal) ( (T) l, (T) r )
+ postcondition(
+ auto result = return,
+ result == !(l != r)
+ )
+) {
+ return l.value == r.value;
+}
+</pre>
+
+ 
+
+
+
+<pre class="programlisting">// In header: equal_not.hpp
+#include "equal.hpp"
+#include <contract.hpp>
+
+CONTRACT_FUNCTION_TPL(
+template( typename T )
+bool operator(!=)(not_equal) ( (T) l, (T) r )
+ postcondition(
+ auto result = return,
+ result == !(l == r)
+ )
+) {
+ return l.value != r.value;
+}
+</pre>
+
+ 
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.examples.__n1962___sum__separated_body_definition"></a><a class="link" href="examples.html#contract__.examples.__n1962___sum__separated_body_definition" title="[N1962] Sum: Separated body definition">[N1962]
+ Sum: Separated body definition</a>
+</h3></div></div></div>
+
+
+
+<pre class="programlisting">// In header: sum.hpp
+#include <contract.hpp>
+
+CONTRACT_FUNCTION(
+double (sum)( int count, (double*) array )
+ precondition( count % 4 == 0 )
+) ; // Separate body definition from function declaration (see .cpp file).
+</pre>
+
+ 
+
+
+
+<pre class="programlisting">#include "sum.hpp"
+
+double CONTRACT_FREE_BODY(sum) ( int count, double* array ) {
+ double accum = 0.0;
+ for(int i = 0; i < count; ++i) accum += array[i];
+ return accum;
+}
+</pre>
+
+ 
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.examples.__n1962___square_root__default_parameters"></a><a class="link" href="examples.html#contract__.examples.__n1962___square_root__default_parameters" title="[N1962] Square Root: Default parameters">[N1962]
+ Square Root: Default parameters</a>
+</h3></div></div></div>
+
+
+
+<pre class="programlisting">#include <contract.hpp>
+#include <cmath>
+
+CONTRACT_FUNCTION( // Default value for `precision` parameter.
+double (mysqrt) ( double x, double precision, default double(1e-6) )
+ precondition( x >= 0.0 )
+ postcondition(
+ auto root = return, // Result value named `root`.
+ fabs(root * root - x) <= precision // Equal within precision.
+ )
+) {
+ return sqrt(x);
+}
+</pre>
+
+ 
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.examples.__n1962___block__block_invariants"></a><a class="link" href="examples.html#contract__.examples.__n1962___block__block_invariants" title="[N1962] Block: Block invariants">[N1962]
+ Block: Block invariants</a>
+</h3></div></div></div>
+
+
+
+<pre class="programlisting">#include <contract.hpp>
+#include <iostream>
+
+int main ( ) {
+ for(int i = 0; i < 100; ++i) {
+ CONTRACT_BLOCK_INVARIANT( const( i ) i < 10 ) // Intentionally fails.
+ std::cout << i << std::endl;
+ }
+ return 0;
+}
+</pre>
+
+ 
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.examples.n2081_add"></a><a class="link" href="examples.html#contract__.examples.n2081_add" title="[N2081] Add: Generic addition algorithm">[N2081] Add: Generic addition
+ algorithm</a>
+</h3></div></div></div>
+
+
+
+<pre class="programlisting">#include <contract.hpp>
+#include <boost/concept_check.hpp>
+
+template< typename T >
+class Addable { // User-defined concept.
+ T x;
+ T y;
+ void return_type ( T ); // Used to check addition returns type `T`.
+public:
+ BOOST_CONCEPT_USAGE(Addable) {
+ return_type(x + y); // Check addition `T operator+(T x, T y)`.
+ }
+};
+
+CONTRACT_FUNCTION(
+template( typename T )
+ requires(
+ Addable<T>
+#ifndef CONTRACT_CONFIG_NO_POSTCONDITIONS // Equality only for postconditions.
+ , boost::EqualityComparable<T>
+#endif
+ )
+(T) (add) ( (T) x, (T) y )
+ postcondition( auto result = return, result == x + y )
+) {
+ return x + y;
+}
+</pre>
+
+ 
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.examples.__n2081___advance__concept_based_iterator_overloading__emulated_using_tags_"></a><a class="link" href="examples.html#contract__.examples.__n2081___advance__concept_based_iterator_overloading__emulated_using_tags_" title="[N2081] Advance: Concept-based iterator overloading (emulated using tags)">[N2081]
+ Advance: Concept-based iterator overloading (emulated using tags)</a>
+</h3></div></div></div>
+
+
+
+<pre class="programlisting">#include <contract.hpp>
+#include <boost/mpl/bool.hpp>
+#include <vector>
+#include <list>
+#include <iterator>
+
+namespace aux { // Tag dispatch helpers (in a private namespace).
+
+template< typename InputIterator, typename Distance >
+void myadvance_dispatch ( InputIterator& i, Distance n,
+ std::input_iterator_tag )
+{
+ CONTRACT_LOOP( while(n--) ) {
+ CONTRACT_LOOP_VARIANT( const( n ) n )
+ ++i;
+ }
+}
+
+template< typename BidirectionalIterator, typename Distance >
+void myadvance_dispatch ( BidirectionalIterator& i, Distance n,
+ std::bidirectional_iterator_tag )
+{
+ if(n >= 0) {
+ CONTRACT_LOOP( while(n--) ) {
+ CONTRACT_LOOP_VARIANT( const( n ) n )
+ ++i;
+ }
+ } else {
+#ifndef CONTRACT_CONFIG_NO_LOOP_VARIANTS
+ Distance n_max = n;
+#endif
+ CONTRACT_LOOP( while(n++) ) {
+ CONTRACT_LOOP_VARIANT( const( n_max, n ) n_max - n )
+ --i;
+ }
+ }
+}
+
+template< typename RandomAccessIterator, typename Distance >
+void myadvance_dispatch ( RandomAccessIterator& i, Distance n,
+ std::random_access_iterator_tag )
+{
+ i += n;
+}
+
+} // namespace aux
+
+// Contract helper meta-function.
+template< typename T > struct is_input_iterator : boost::mpl::false_ {};
+template< > struct is_input_iterator<std::input_iterator_tag>
+ : boost::mpl::true_ {};
+
+CONTRACT_FUNCTION(
+template( typename InputIterator, typename Distance )
+void (myadvance) ( (InputIterator&) i, (Distance) n )
+ precondition(
+ // Precondition: All iterators in [i, i + n] non-singular.
+ if(is_input_iterator<typename std::iterator_traits<InputIterator>::
+ iterator_category>::value) (
+ n > 0 // if input iterator, n positive
+ )
+ )
+ postcondition(
+ auto old_i = CONTRACT_OLDOF i,
+ std::distance(old_i, i) == n // iterator advanced of n
+ )
+) {
+ aux::myadvance_dispatch(i, n, std::iterator_traits<InputIterator>::
+ iterator_category());
+}
+</pre>
+
+ 
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.examples.__n2081___find__generic_find_algorithm"></a><a class="link" href="examples.html#contract__.examples.__n2081___find__generic_find_algorithm" title="[N2081] Find: Generic find algorithm">[N2081]
+ Find: Generic find algorithm</a>
+</h3></div></div></div>
+
+
+
+<pre class="programlisting">#include <contract.hpp>
+#include <boost/concept_check.hpp>
+
+CONTRACT_FUNCTION(
+template( typename Iter )
+ requires(
+ boost::InputIterator<Iter>,
+ boost::EqualityComparable<typename
+ boost::InputIterator<Iter>::value_type>
+ )
+(Iter) (myfind) ( (Iter) first, (Iter) last,
+ (typename boost::InputIterator<Iter>::value_type const&) value )
+ precondition( first <= last )
+ postcondition(
+ auto result = return,
+ if(result != last) (
+ value == *result // if result not last, value found
+ )
+ )
+) {
+ CONTRACT_LOOP( while(first != last && *first != value) ) {
+ CONTRACT_LOOP_VARIANT( const( first, last ) std::distance(first, last) )
+ ++first;
+ }
+ return first;
+}
+</pre>
+
+ 
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.examples.__n2081___apply__overloaded_invocation_of_functors"></a><a class="link" href="examples.html#contract__.examples.__n2081___apply__overloaded_invocation_of_functors" title="[N2081] Apply: Overloaded invocation of functors">[N2081]
+ Apply: Overloaded invocation of functors</a>
+</h3></div></div></div>
+
+
+
+<pre class="programlisting">#include <contract.hpp>
+#include <boost/concept_check.hpp>
+
+// Use importance ordering to specify assertion computational complexity.
+#define O_1 0 // O(1) constant (default)
+#define O_BODY 1 // same computation complexity of the body
+
+CONTRACT_FUNCTION( // Invoke unary functors.
+template( typename Result, typename Arg0, typename UnaryOp )
+ requires(
+ typename CONTRACT_IDENTITY_TYPE((
+ boost::UnaryFunction<UnaryOp, Result, Arg0> ))
+#ifndef CONTRACT_CONFIG_NO_POSTCONDITIONS // Equality only for postconditions.
+ , boost::EqualityComparable<Result>
+#endif
+ )
+(Result) (apply) ( (UnaryOp) op, (Arg0) arg0, (Result&) result )
+ postcondition(
+ auto return_value = return,
+ result == op(arg0), importance O_BODY,
+ return_value == result
+ )
+) {
+ return result = op(arg0);
+}
+
+CONTRACT_FUNCTION( // Overload to invoke binary functors.
+template( typename Result, typename Arg0, typename Arg1, typename BinaryOp )
+ requires(
+ typename CONTRACT_INDETITY_TYPE((
+ boost::BinaryFunction<BinaryOp, Result, Arg0, Arg1> ))
+#ifndef CONTRACT_CONFIG_NO_POSTCONDITIONS // Equality only for postconditions.
+ , boost::EqualityComparable<Result>
+#endif
+ )
+(Result) (apply) ( (BinaryOp) op, (Arg0) arg0, (Arg1) arg1, (Result&) result )
+ postcondition(
+ auto return_value = return,
+ result == op(arg0, arg1), importance O_BODY,
+ return_value == result
+ )
+) {
+ return result = op(arg0, arg1);
+}
+</pre>
+
+ 
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.examples.__n2081___for_each__generic_for_each_algorithm"></a><a class="link" href="examples.html#contract__.examples.__n2081___for_each__generic_for_each_algorithm" title="[N2081] For Each: Generic for-each algorithm">[N2081]
+ For Each: Generic for-each algorithm</a>
+</h3></div></div></div>
+
+
+
+<pre class="programlisting">#include <contract.hpp>
+#include <boost/concept_check.hpp>
+
+CONTRACT_FUNCTION(
+template( typename Iter, typename Func )
+ requires(
+ boost::InputIterator<Iter>
+ typename CONTRACT_INDENTITY_TYPE(( boost::UnaryFunction<Func, void,
+ typename boost::InputIterator<Iter>::value_type> ))
+#ifndef CONTRACT_CONFIG_NO_POSTCONDITIONS // Equality only for postconditions.
+ , boost::EqualityComparable<Func>
+#endif
+ )
+(Func) (my_for_each) ( (Iter) first, (Iter) last, (Func) func )
+ precondition( first <= last )
+ postcondition( auto result = return, result == func )
+) {
+ CONTRACT_LOOP( while(first < last) ) { // OK: Iter is InputIterator.
+ CONTRACT_LOOP_VARIANT( const( first, last ) std::distance(first, last) )
+ func(*first); // OK: func is UnaryFunction.
+ ++first; // OK: Iter is InputIterator.
+ }
+ return func;
+}
+</pre>
+
+ 
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.examples.__n2081___transform__generic_binary_transformation_algorithm"></a><a class="link" href="examples.html#contract__.examples.__n2081___transform__generic_binary_transformation_algorithm" title="[N2081] Transform: Generic binary transformation algorithm">[N2081]
+ Transform: Generic binary transformation algorithm</a>
+</h3></div></div></div>
+
+
+
+<pre class="programlisting">#define CONTRACT_CONFIG_FUNCTION_ARITY_MAX 6 // Support 5 function parameters.
+#include <contract.hpp>
+#include <boost/concept_check.hpp>
+#include <algorithm>
+
+CONTRACT_FUNCTION(
+template( typename InIter1, typename InIter2, typename OutIter, typename BinOp )
+ requires(
+ boost::InputIterator<InIter1>,
+ boost::InputIterator<InIter2>,
+ typename CONTRACT_IDENTITY_TYPE(( boost::OutputIterator<OutIter,
+ typename boost::InputIterator<InIter1>::value_type > )),
+ typename CONTRACT_IDENTITY_TYPE(( boost::BinaryFunction<BinOp,
+ typename boost::InputIterator<InIter1>::value_type,
+ typename boost::InputIterator<InIter1>::value_type,
+ typename boost::InputIterator<InIter2>::value_type> ))
+#ifndef CONTRACT_CONFIG_NO_POSTCONDITIONS // Equality only for postcondition
+ , boost::EqualityComparable<typename
+ boost::InputIterator<InIter1>::value_type>
+#endif
+ )
+(OutIter) (mytransform) ( (InIter1) first1, (InIter1) last1, (InIter2) first2,
+ (OutIter) result, (BinOp) op )
+ precondition( first1 <= last1 )
+ postcondition( auto return_value = return, return_value == result )
+) {
+ return std::transform(first1, last1, first2, result, op);
+}
+</pre>
+
+ 
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.examples.__n2081___count__generic_count_algorithm"></a><a class="link" href="examples.html#contract__.examples.__n2081___count__generic_count_algorithm" title="[N2081] Count: Generic count algorithm">[N2081]
+ Count: Generic count algorithm</a>
+</h3></div></div></div>
+
+
+
+<pre class="programlisting">#include <contract.hpp>
+#include <boost/concept_check.hpp>
+
+CONTRACT_FUNCTION(
+template( typename Iter )
+ requires(
+ boost::InputIterator<Iter>,
+ boost::EqualityComparable<Iter>,
+ boost::EqualityComparable<typename
+ boost::InputIterator<Iter>::value_type>
+ )
+(typename boost::InputIterator<Iter>::difference_type) (mycount) (
+ (Iter) first, (Iter) last,
+ (typename boost::InputIterator<Iter>::value_type const&) value )
+ // Precondition: [first, last) is valid range.
+ precondition( first <= last )
+ postcondition( auto result = return, result >= 0 )
+) {
+ typename boost::InputIterator<Iter>::difference_type result = 0;
+ CONTRACT_LOOP( while(first != last) ) { // OK: Iter is equality comparable.
+ CONTRACT_LOOP_VARIANT( const( first, last) std::distance(first, last) )
+ if(*first == value) // OK: Value is equality comparable.
+ ++result;
+ ++first; // OK: Iterator is input iterator.
+ }
+ return result; // OK: Input iterator difference is copy constructible.
+}
+</pre>
+
+ 
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.examples.__n2081___convert__conversion_between_two_types"></a><a class="link" href="examples.html#contract__.examples.__n2081___convert__conversion_between_two_types" title="[N2081] Convert: Conversion between two types">[N2081]
+ Convert: Conversion between two types</a>
+</h3></div></div></div>
+
+
+
+<pre class="programlisting">#include <contract.hpp>
+#include <boost/concept_check.hpp>
+
+CONTRACT_FUNCTION(
+template( typename To, typename From )
+ requires(
+ typename CONTRACT_IDENTITY_TYPE(( boost::Convertible<From, To> ))
+ )
+(To) (convert) ( (From const&) from )
+) {
+ return from;
+}
+</pre>
+
+ 
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.examples.__n2081___equal__generic_equality_comparison"></a><a class="link" href="examples.html#contract__.examples.__n2081___equal__generic_equality_comparison" title="[N2081] Equal: Generic equality comparison">[N2081]
+ Equal: Generic equality comparison</a>
+</h3></div></div></div>
+
+
+
+<pre class="programlisting">#include <contract.hpp>
+#include <boost/concept_check.hpp>
+
+CONTRACT_FUNCTION(
+template( typename T )
+ requires( boost::EqualityComparable<T> )
+bool (equal) ( (T const&) left, (T const&) right )
+ postcondition( auto result = return, result == (left == right) )
+) {
+ return left == right;
+}
+</pre>
+
+ 
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.examples.__n2081___less_equal__generic_less_than_or_equal_to_comparison"></a><a class="link" href="examples.html#contract__.examples.__n2081___less_equal__generic_less_than_or_equal_to_comparison" title="[N2081] Less Equal: Generic less-than or equal-to comparison">[N2081]
+ Less Equal: Generic less-than or equal-to comparison</a>
+</h3></div></div></div>
+
+
+
+<pre class="programlisting">#include <contract.hpp>
+#include <boost/concept_check.hpp>
+
+CONTRACT_FUNCTION(
+template( typename T )
+ requires( boost::EqualityComparable<T>, boost::LessThanComparable<T> )
+bool (leq) ( (T) left, (T) right )
+ postcondition(
+ auto result = return,
+ result == (left < right || left == right)
+ )
+) {
+ return left < right || left == right;
+}
+</pre>
+
+ 
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.examples.__n2081___de_ref__generic_iterator_dereferencing"></a><a class="link" href="examples.html#contract__.examples.__n2081___de_ref__generic_iterator_dereferencing" title="[N2081] De-Ref: Generic iterator dereferencing">[N2081]
+ De-Ref: Generic iterator dereferencing</a>
+</h3></div></div></div>
+
+
+
+<pre class="programlisting">#include <contract.hpp>
+#include <boost/concept_check.hpp>
+
+CONTRACT_FUNCTION(
+template( typename Iter )
+ requires(
+ boost::InputIterator<Iter>,
+ boost::CopyConstructible<typename
+ boost::InputIterator<Iter>::value_type>,
+#ifndef CONTRACT_CONFIG_NO_POSTCONDITIONS // Equality only for postconditions.
+ boost::EqualityComparable<typename
+ boost::InputIterator<Iter>::value_type>
+#endif
+ )
+(typename boost::InputIterator<Iter>::value_type) (deref) ( (Iter) i )
+ // Precondition: i is non-singular.
+ postcondition( auto result = return, result == *i )
+) {
+ return *i;
+}
+</pre>
+
+ 
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.examples.__n2081___min__generic_minimum_algorithm"></a><a class="link" href="examples.html#contract__.examples.__n2081___min__generic_minimum_algorithm" title="[N2081] Min: Generic minimum algorithm">[N2081]
+ Min: Generic minimum algorithm</a>
+</h3></div></div></div>
+
+
+
+<pre class="programlisting">#include <contract.hpp>
+#include <boost/concept_check.hpp>
+
+CONTRACT_FUNCTION(
+template( typename T )
+ requires(
+ boost::LessThanComparable<T>
+#ifndef CONTRACT_CONFIG_NO_POSTCONDITIONS // Equality only for postconditions.
+ , boost::EqualityComparable<T>
+#endif
+ )
+(T const&) (min) ( (T const&) x, (T const&) y )
+ postcondition(
+ auto result = return,
+ x < y ? result == x : result == y // Need both `<` and `==`.
+ )
+) {
+ return x < y ? x : y; // OK: T is less than comparable `<`.
+}
+</pre>
+
+ 
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.examples.meyer97_stack4"></a><a class="link" href="examples.html#contract__.examples.meyer97_stack4" title="[Meyer97] Stack4: Comparison with Eiffel syntax">[Meyer97] Stack4:
+ Comparison with Eiffel syntax</a>
+</h3></div></div></div>
+<div class="informaltable"><table class="table">
+<colgroup>
+<col>
+<col>
+</colgroup>
+<thead><tr>
+<th>
+ 
+ ISO C++ (this library)
+ 
+ </th>
+<th>
+ 
+ Eiffel (<a class="link" href="bibliography.html" title="Bibliography">[Meyer97]</a>)
+ 
+ </th>
+</tr></thead>
+<tbody><tr>
+<td>
+ 
+
+
+<pre xmlns:rev="http://www.cs.rpi.edu/~gregod/boost/tools/doc/revision" class="table-programlisting">// In header: stack4.hpp
+#include <contract.hpp>
+
+// Specification.
+
+CONTRACT_CLASS( // Dispenser with LIFO access policy and a fixed max capacity.
+template( typename T )
+class (stack4)
+) {
+ CONTRACT_CLASS_INVARIANT_TPL(
+ count() >= 0, // count non negative
+ count() <= capacity(), // count bounded
+ empty() == (count() == 0) // empty if no elements
+ )
+
+public:
+ // Initialization.
+
+ CONTRACT_CONSTRUCTOR_TPL( // Allocate stack for a maximum of n elements.
+ public explicit (stack4) ( (const int&) n )
+ precondition(
+ n >= 0 // non negative capacity
+ )
+ postcondition(
+ capacity() == n // capacity set
+ )
+ ) ; // Deferred body definition (see bottom).
+
+ CONTRACT_CONSTRUCTOR_TPL( // Deep copy.
+ public (stack4) ( (const stack4&) right )
+ postcondition(
+ capacity() == right.capacity(),
+ count() == right.count()
+ // all items equal right's items one by one
+ )
+ ) ;
+
+ CONTRACT_FUNCTION_TPL( // Deep assignment.
+ public (stack4&) operator(=)(assign) ( (const stack4&) right )
+ postcondition(
+ capacity() == right.capacity(),
+ count() == right.count()
+ // all items equal right's items one by one
+ )
+ ) ;
+
+ CONTRACT_DESTRUCTOR_TPL( // Destroy this stack.
+ public virtual (~stack4) ( void )
+ ) ;
+
+ // Access.
+
+ CONTRACT_FUNCTION_TPL( // Max number of stack elements.
+ public int (capacity) ( void ) const
+ ) ;
+
+ CONTRACT_FUNCTION_TPL( // Number of stack elements.
+ public int (count) ( void ) const
+ ) ;
+
+ CONTRACT_FUNCTION_TPL( // Top element.
+ public (const T&) (item) ( void ) const
+ precondition(
+ empty() == false // not empty (i.e., count > 0)
+ )
+ ) ;
+
+ // Status report.
+
+ CONTRACT_FUNCTION_TPL( // Is stack empty?
+ public bool (empty) ( void ) const
+ postcondition(
+ auto result = return,
+ result == (count() == 0) // empty definition
+ )
+ ) ;
+
+ CONTRACT_FUNCTION_TPL( // Is stack full?
+ public bool (full) ( void ) const
+ postcondition(
+ auto result = return,
+ result == (count() == capacity()) // full definition
+ )
+ ) ;
+
+ // Element change.
+
+ CONTRACT_FUNCTION_TPL( // Add x on top.
+ public void (put) ( (const T&) x )
+ precondition(
+ full() == false // not full
+ )
+ postcondition(
+ auto old_count = CONTRACT_OLDOF count(),
+ empty() == false, // not empty
+ item() == x, // added to top
+ count() == old_count + 1 // one more item
+ )
+ ) ;
+
+ CONTRACT_FUNCTION_TPL( // Remove top item.
+ public void (remove) ( void )
+ precondition(
+ empty() == false // not empty (i.e., count > 0)
+ )
+ postcondition(
+ auto old_count = CONTRACT_OLDOF count(),
+ full() == false, // not full
+ count() == old_count - 1 // one fewer item
+ )
+ ) ;
+
+private:
+ int capacity_;
+ int count_;
+ T* representation_; // Using C-style array.
+};
+
+// Implementation.
+
+template< typename T >
+CONTRACT_CONSTRUCTOR_BODY(stack4<T>, stack4) ( const int& n ) {
+ capacity_ = n;
+ count_ = 0;
+ representation_ = new T[n];
+}
+
+template< typename T >
+CONTRACT_CONSTRUCTOR_BODY(stack4<T>, stack4) ( const stack4& right ) {
+ capacity_ = right.capacity_;
+ count_ = right.count_;
+ representation_ = new T[right.capacity_];
+ for(int i = 0; i < right.count_; ++i)
+ representation_[i] = right.representation_[i];
+}
+
+template< typename T >
+stack4<T>& stack4<T>::CONTRACT_MEMBER_BODY(operator(=)(assign)) (
+ const stack4& right ) {
+ delete[] representation_;
+ capacity_ = right.capacity_;
+ count_ = right.count_;
+ representation_ = new T[right.capacity_];
+ for(int i = 0; i < right.count_; ++i)
+ representation_[i] = right.representation_[i];
+ return *this;
+}
+
+template< typename T >
+CONTRACT_DESTRUCTOR_BODY(stack4<T>, ~stack4) ( void ) {
+ delete[] representation_;
+}
+
+template< typename T >
+int stack4<T>::CONTRACT_MEMBER_BODY(capacity) ( void ) const {
+ return capacity_;
+}
+
+template< typename T >
+int stack4<T>::CONTRACT_MEMBER_BODY(count) ( void ) const {
+ return count_;
+}
+
+template< typename T >
+const T& stack4<T>::CONTRACT_MEMBER_BODY(item) ( void ) const {
+ return representation_[count() - 1];
+}
+
+template< typename T >
+bool stack4<T>::CONTRACT_MEMBER_BODY(empty) ( void ) const {
+ return count() == 0;
+}
+
+template< typename T >
+bool stack4<T>::CONTRACT_MEMBER_BODY(full) ( void ) const {
+ return count() == capacity();
+}
+
+template< typename T >
+void stack4<T>::CONTRACT_MEMBER_BODY(put) ( const T& x ) {
+ representation_[count_++] = x;
+}
+
+template< typename T >
+void stack4<T>::CONTRACT_MEMBER_BODY(remove) ( void ) {
+ --count_;
+}
+</pre>
+
+ 
+ </td>
+<td>
+ 
+
+
+<pre xmlns:rev="http://www.cs.rpi.edu/~gregod/boost/tools/doc/revision" class="table-programlisting">-- Extra spacing and newlines used to visually align with this library code.
+
+
+
+
+indexing
+ destription: "Dispenser with LIFO access policy and a fixed max capacity."
+class interface STACK4[G] creation make
+
+invariant
+ count_non_negative: count >= 0
+ count_bounded: count <= capacity
+ empty_if_no_elements: empty = (count = 0)
+
+
+
+feature -- Initialization.
+
+ -- Allocate stack for a maximum of n elements.
+ make ( n : INTEGER ) is
+ require
+ non_negative_capacity: n >= 0
+
+ ensure
+ capacity_set: capacity = n
+
+ end
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+feature -- Access.
+
+ -- Max number of stack elements.
+ capacity : INTEGER
+
+
+ -- Number of stack elements.
+ count : INTEGER
+
+
+ -- Top element
+ item : G is
+ require
+ not_empty: not empty -- i.e., count > 0
+
+ end
+
+feature -- Status report.
+
+ -- Is stack empty?
+ empty : BOOLEAN is
+ ensure
+
+ empty_definition: result = (count = 0)
+
+ end
+
+ -- Is stack full?
+ full : BOOLEAN is
+ ensure
+
+ full_definition: result = (count = capacity)
+
+ end
+
+feature -- Element change.
+
+ -- Add x on top.
+ put ( x : G ) is
+ require
+ not_full: not full
+
+ ensure
+
+ not_empty: not empty
+ added_to_top: item = x
+ one_more_item: count = old count + 1
+
+ end
+
+ -- Remove top element.
+ remove is
+ require
+ not_empty: not empty -- i.e., count > 0
+
+ ensure
+
+ not_full: not full
+ one_fewer_item: count = old count - 1
+
+ end
+
+
+
+
+
+end -- class interface STACK4
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+</pre>
+
+ 
+ </td>
+</tr></tbody>
+</table></div>
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.examples.__meyer97___stack3__error_codes_instead_of_preconditions"></a><a class="link" href="examples.html#contract__.examples.__meyer97___stack3__error_codes_instead_of_preconditions" title="[Meyer97] Stack3: Error codes instead of preconditions">[Meyer97]
+ Stack3: Error codes instead of preconditions</a>
+</h3></div></div></div>
+
+
+
+<pre class="programlisting">#include "stack4.hpp"
+#include <contract.hpp>
+
+CONTRACT_CLASS( // Dispenser LIFO and max capacity using error codes.
+template( typename T )
+class (stack3)
+) {
+ CONTRACT_CLASS_INVARIANT_TPL( void ) // no class invariant
+
+public:
+ enum Error { // Error codes.
+ NO_ERROR = 0,
+ OVERFLOW_ERROR,
+ UNDERFLOW_ERROR,
+ SIZE_ERROR
+ };
+
+ // Initialization.
+
+ // Create stack for max of n elements, if n < 0 set error (no precondition).
+ CONTRACT_CONSTRUCTOR_TPL(
+ public (stack3) ( (const int&) n, (const T&) none, default T() )
+ initialize( none_(none), representation_(0), error_(NO_ERROR) )
+ postcondition(
+ (n < 0) == (error() == SIZE_ERROR), // error if impossible
+ (n >= 0) == !error(), // no error if possible
+ if(bool(!error())) ( capacity() == n ) // created if no error
+ )
+ ) {
+ if(n >= 0) representation_ = stack4<T>(n);
+ else error_ = SIZE_ERROR;
+ }
+
+ CONTRACT_DESTRUCTOR_TPL( // Destroy stack.
+ public virtual (~stack3) ( void )
+ ) {}
+
+ // Access.
+
+ CONTRACT_FUNCTION_TPL( // Max number of stack elements.
+ public int (capacity) ( void ) const
+ ) {
+ return representation_.capacity();
+ }
+
+ CONTRACT_FUNCTION_TPL( // Number of stack elements.
+ public int (count) ( void ) const
+ ) {
+ return representation_.count();
+ }
+
+ // Top element if present, otherwise set error (no precondition).
+ CONTRACT_FUNCTION_TPL(
+ public (const T&) (item) ( void ) const
+ postcondition(
+ empty() == (error() == UNDERFLOW_ERROR), // error if impossible
+ bool(!empty() == !error()) // no error if possible
+ )
+ ) {
+ if(!empty()) {
+ error_ = NO_ERROR;
+ return representation_.item();
+ } else {
+ error_ = UNDERFLOW_ERROR;
+ return none_;
+ }
+ }
+
+ // Status report.
+
+ CONTRACT_FUNCTION_TPL( // Error indicator set by various operations.
+ public (Error) (error) ( void ) const
+ ) {
+ return error_;
+ }
+
+ CONTRACT_FUNCTION_TPL( // Is stack empty?
+ public bool (empty) ( void ) const
+ ) {
+ return representation_.empty();
+ }
+
+ CONTRACT_FUNCTION_TPL( // Is stack full?
+ public bool (full) ( void ) const
+ ) {
+ return representation_.full();
+ }
+
+ // Element change.
+
+ // Add x to top if capacity left, otherwise set error (no precondition).
+ CONTRACT_FUNCTION_TPL(
+ public void (put) ( (const T&) x )
+ postcondition(
+ auto old_full = CONTRACT_OLDOF full(),
+ auto old_count = CONTRACT_OLDOF count(),
+ old_full == (error() == OVERFLOW_ERROR), // error if impossible
+ bool(!old_full == !error()), // no error if possible
+ if(bool(!error())) (
+ empty() == false, // not empty if no error
+ item() == x, // added to top is no error
+ count() == old_count + 1 // one more item if no error
+ )
+ )
+ ) {
+ if(full()) {
+ error_ = OVERFLOW_ERROR;
+ } else {
+ representation_.put(x);
+ error_ = NO_ERROR;
+ }
+ }
+
+ // Remove top item if possible, otherwise set error to (no precondition).
+ CONTRACT_FUNCTION_TPL(
+ public void (remove) ( void )
+ postcondition(
+ auto old_empty = CONTRACT_OLDOF empty(),
+ auto old_count = CONTRACT_OLDOF count(),
+ old_empty == (error() == UNDERFLOW_ERROR), // error if impossible
+ bool(!old_empty == !error()), // no error if possible
+ if(bool(!error())) (
+ full() == false, // not full is no error
+ count() == old_count - 1 // one fewer item if no error
+ )
+ )
+ ) {
+ if(empty()) {
+ error_ = UNDERFLOW_ERROR;
+ } else {
+ representation_.remove();
+ error_ = NO_ERROR;
+ }
+ }
+
+private:
+ const T none_;
+ stack4<T> representation_;
+ mutable Error error_; // Mutable as changed by logically const members.
+};
+</pre>
+
+ 
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.examples.meyer97_gcd"></a><a class="link" href="examples.html#contract__.examples.meyer97_gcd" title="[Meyer97] GCD: Loop variant and comparison with Eiffel syntax">[Meyer97] GCD: Loop
+ variant and comparison with Eiffel syntax</a>
+</h3></div></div></div>
+<div class="informaltable"><table class="table">
+<colgroup>
+<col>
+<col>
+</colgroup>
+<thead><tr>
+<th>
+ 
+ ISO C++ (this library)
+ 
+ </th>
+<th>
+ 
+ Eiffel (<a class="link" href="bibliography.html" title="Bibliography">[Meyer97]</a>)
+ 
+ </th>
+</tr></thead>
+<tbody><tr>
+<td>
+ 
+
+
+<pre xmlns:rev="http://www.cs.rpi.edu/~gregod/boost/tools/doc/revision" class="table-programlisting">#include <contract.hpp>
+#include <algorithm>
+
+CONTRACT_FUNCTION( // Great common divisor of given positive integers.
+int (gcd) ( int a, int b )
+ precondition(
+ a > 0, b > 0
+ )
+) {
+ int x = a, y = b;
+
+ CONTRACT_LOOP( while(x != y) ) { // Loop contracted with a variant.
+ CONTRACT_BLOCK_INVARIANT( // Block invariant assert loop invariant.
+ const( x ) x > 0, const( y ) y > 0
+ // x and y have the same GCD as a and b.
+ )
+ CONTRACT_LOOP_VARIANT( // Loop variant is a non-negative and
+ const( x, y ) std::max(x, y) // monotonically decreasing expression.
+ )
+
+ if(x > y) x = x - y;
+ else y = y - x;
+ }
+ return x;
+}
+</pre>
+
+ 
+ </td>
+<td>
+ 
+
+
+<pre xmlns:rev="http://www.cs.rpi.edu/~gregod/boost/tools/doc/revision" class="table-programlisting">-- Extra spacing and newlines used to visually align with this library code.
+
+
+-- Greatest common divisor of a and b.
+gcd ( a, b : INTEGER ) : INTEGER is
+ require
+ a > 0; b >0
+ local
+ x, y : INTEGER
+ do
+ from
+ x := a; y := b
+ invariant
+ x > 0; y > 0
+ -- x and y have the same GCD as a and b.
+
+ variant
+ x.max(y)
+ until
+ x = y
+ loop
+ if x > y then x := x - y else y := y - x end
+ end
+ Result := x
+ end
+</pre>
+
+ 
+ </td>
+</tr></tbody>
+</table></div>
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.examples.__meyer97___max_array__nested_loop_variants"></a><a class="link" href="examples.html#contract__.examples.__meyer97___max_array__nested_loop_variants" title="[Meyer97] Max Array: Nested loop variants">[Meyer97]
+ Max Array: Nested loop variants</a>
+</h3></div></div></div>
+
+
+
+<pre class="programlisting">#include <contract.hpp>
+#include <algorithm>
+
+CONTRACT_FUNCTION(
+int (maxarray) ( (int const* const) array, (size_t const&) size )
+ precondition(
+ array, // array allocated
+ size >= 1 // size in range
+ )
+) {
+ int maxnow = array[0];
+ CONTRACT_LOOP( for(size_t i = 0; i < (size - 1); ++i) ) {
+ // Nested loop (with variant) used to assert enclosing loop invariants.
+ CONTRACT_LOOP( for(size_t j = 0; j < i; ++j) ) {
+ CONTRACT_LOOP_VARIANT( const( i, j ) i - j )
+ CONTRACT_BLOCK_INVARIANT( const( maxnow, array, j )
+ maxnow >= array[j] )
+ }
+ // -2 because starts from 0 (not 1) and already done element at 0.
+ CONTRACT_LOOP_VARIANT( const( size, i ) size - i - 2 )
+
+ maxnow = std::max(maxnow, array[i]);
+ }
+ return maxnow;
+}
+</pre>
+
+ 
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.examples.__mitchell02___name_list__relaxing_subcontracts"></a><a class="link" href="examples.html#contract__.examples.__mitchell02___name_list__relaxing_subcontracts" title="[Mitchell02] Name List: Relaxing subcontracts">[Mitchell02]
+ Name List: Relaxing subcontracts</a>
+</h3></div></div></div>
+
+
+
+<pre class="programlisting">// In header: name_list.hpp
+#include <contract.hpp>
+#include <string>
+#include <list>
+
+CONTRACT_CLASS( // List of names.
+class (name_list)
+) {
+ CONTRACT_CLASS_INVARIANT( count() >= 0 ) // non-negative count
+
+public:
+ CONTRACT_CONSTRUCTOR( // Create an empty list.
+ public (name_list) ( void )
+ postcondition( count() == 0 ) // empty list
+ ) ; // Deferred body definition.
+
+ CONTRACT_DESTRUCTOR( // Destroy list.
+ public virtual (~name_list) ( void )
+ ) ;
+
+ CONTRACT_FUNCTION( // Number of names in list.
+ public int (count) ( void ) const
+ // Postcondition non-negative count already in class invariants.
+ ) ;
+
+ CONTRACT_FUNCTION( // Is name in list?
+ public bool (has) ( (std::string const&) name ) const
+ postcondition(
+ auto result = return,
+ if(count() == 0) ( result == false ) // does not have is empty
+ )
+ ) ;
+
+ CONTRACT_FUNCTION( // Add name to list.
+ public virtual void (put) ( (std::string const&) name )
+ precondition(
+ has(name) == false // not already in list
+ )
+ postcondition(
+ auto old_has_name = CONTRACT_OLDOF has(name),
+ auto old_count = CONTRACT_OLDOF count(),
+ // Following if-guard allows to relax subcontracts.
+ if(old_has_name == false) (
+ has(name), // name on list
+ count() == old_count + 1 // number of names increased
+ )
+ )
+ ) ;
+
+private:
+ std::list<std::string> names_;
+
+};
+
+CONTRACT_CLASS( // List of names that allows for duplicates.
+class (relaxed_name_list) extends( public name_list ) // Subcontracting.
+) {
+ CONTRACT_CLASS_INVARIANT( void ) // no subcontracted invariants
+
+public:
+ // Creation.
+
+ CONTRACT_CONSTRUCTOR( // Create an empty list.
+ public (relaxed_name_list) ( void )
+ postcondition( count() == 0 )
+ ) ;
+
+ CONTRACT_DESTRUCTOR( // Destroy list.
+ public virtual (~relaxed_name_list) ( void )
+ ) ;
+
+ // Commands.
+
+ CONTRACT_FUNCTION( // Add name to list.
+ public void (put) ( (std::string const&) name )
+ precondition( // Relax inherited precondition.
+ has(name) // already in list
+ )
+ postcondition(
+ auto old_has_name = CONTRACT_OLDOF has(name),
+ auto old_count = CONTRACT_OLDOF count(),
+ // Inherited postcondition not checked because of its if-guard.
+ if(old_has_name) (
+ count() == old_count // count unchanged if name already in list
+ )
+ )
+ ) ;
+};
+</pre>
+
+ 
+
+
+
+<pre class="programlisting">#include "name_list.hpp"
+#include <algorithm>
+
+// name_list
+
+CONTRACT_CONSTRUCTOR_BODY(name_list, name_list) ( void ) {}
+
+CONTRACT_DESTRUCTOR_BODY(name_list, ~name_list) ( void ) {}
+
+int name_list::CONTRACT_MEMBER_BODY(count) ( void ) const
+ { return names_.size(); }
+
+bool name_list::CONTRACT_MEMBER_BODY(has) ( std::string const& name ) const
+ { return names_.end() != std::find(names_.begin(), names_.end(), name); }
+
+void name_list::CONTRACT_MEMBER_BODY(put) ( std::string const& name )
+ { names_.push_back(name); }
+
+// relaxed_name_list
+
+CONTRACT_CONSTRUCTOR_BODY(relaxed_name_list, relaxed_named_list) ( void ) {}
+
+CONTRACT_DESTRUCTOR_BODY(relaxed_name_list, ~relaxed_named_list) ( void ) {}
+
+void relaxed_name_list::CONTRACT_MEMBER_BODY(put) ( std::string const& name ) {
+ // Must use `BODY` to call base functions (to avoid infinite recursion).
+ if(!has(name)) name_list::CONTRACT_MEMBER_BODY(put)(name);
+}
+</pre>
+
+ 
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.examples.__mitchell02___dictionary__simple_key_value_map"></a><a class="link" href="examples.html#contract__.examples.__mitchell02___dictionary__simple_key_value_map" title="[Mitchell02] Dictionary: Simple key-value map">[Mitchell02]
+ Dictionary: Simple key-value map</a>
+</h3></div></div></div>
+
+
+
+<pre class="programlisting">#include <contract.hpp>
+#include <utility>
+#include <map>
+
+CONTRACT_CLASS( // Simple dictionary.
+template( typename Key, typename Value )
+class (dictionary)
+) {
+ CONTRACT_CLASS_INVARIANT_TPL( count() >= 0 ) // non-negative count
+
+public:
+ // Creation.
+
+ CONTRACT_CONSTRUCTOR_TPL( // Create empty dictionary.
+ public (dictionary) ( void )
+ postcondition( count() == 0 ) // empty
+ ) {}
+
+ CONTRACT_DESTRUCTOR_TPL( // Destroy dictionary.
+ public virtual (~dictionary) ( void )
+ ) {}
+
+ // Basic queries.
+
+ CONTRACT_FUNCTION_TPL( // Number of key entires.
+ public int (count) ( void ) const
+ // Postcondition: non-negative count asserted by class invariants.
+ ) {
+ return items_.size();
+ }
+
+ CONTRACT_FUNCTION_TPL( // Has entry for key?
+ public bool (has) ( (Key const&) key ) const
+ postcondition(
+ auto result = return,
+ if(count() == 0) ( result == false ) // empty has no key
+ )
+ ) {
+ return items_.find(key) != items_.end();
+ }
+
+ CONTRACT_FUNCTION_TPL( // Value for given key.
+ public (Value const&) (value_for) ( (Key const&) key ) const
+ precondition( has(key) ) // has key
+ ) {
+ return items_.find(key)->second;
+ }
+
+ // Commands.
+
+ CONTRACT_FUNCTION_TPL( // Put value for given key.
+ public void (put) ( (Key const&) key, (Value const&) value )
+ postcondition(
+ auto old_count = CONTRACT_OLDOF count(),
+ count() == old_count + 1, // count increased
+ has(key), // has key
+ value_for(key) == value // value for key set
+ )
+ ) {
+ items_.insert(std::make_pair(key, value));
+ }
+
+ CONTRACT_FUNCTION_TPL( // Remove value for given key.
+ public void (remove) ( (Key const&) key )
+ precondition( has(key) ) // has key
+ postcondition(
+ auto old_count = CONTRACT_OLDOF count(),
+ count() == old_count - 1, // count decreased
+ has(key) == false // does not have key
+ )
+ ) {
+ items_.erase(key);
+ }
+
+private:
+ std::map<Key, Value> items_;
+};
+</pre>
+
+ 
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.examples.__mitchell02___courier__subcontracting_and_static_class_invariants"></a><a class="link" href="examples.html#contract__.examples.__mitchell02___courier__subcontracting_and_static_class_invariants" title="[Mitchell02] Courier: Subcontracting and static class invariants">[Mitchell02]
+ Courier: Subcontracting and static class invariants</a>
+</h3></div></div></div>
+
+
+
+<pre class="programlisting">// In header: courier.hpp
+#include <contract.hpp>
+#include <string>
+
+struct package { // Basic package information.
+ double weight_kg; // Weight in kilograms.
+ std::string location; // Current location.
+ double accepted_hour; // Hour when it was accepted for delivery.
+ double delivered_hour; // Hour when it was delivered.
+
+ package(double const a_weight_kg,
+ std::string const a_location = "",
+ double const an_accepted_hour = 0.0,
+ double const a_delivered_hour = 0.0)
+ : weight_kg(a_weight_kg)
+ , location(a_location)
+ , accepted_hour(an_accepted_hour)
+ , delivered_hour(a_delivered_hour)
+ {}
+};
+
+CONTRACT_CLASS( // Basic courier for package delivery.
+class (courier)
+) {
+ CONTRACT_CLASS_INVARIANT(
+ insurance_cover_dollar() >= min_insurance_dollar, // above min insurance
+ static class( // Static class invariants.
+ min_insurance_dollar > 0.0 // positive min insurance
+ )
+ )
+
+public:
+ static double min_insurance_dollar;
+
+ // Creation.
+
+ CONTRACT_CONSTRUCTOR( // Create courier with specified insurance value.
+ public explicit (courier) ( double const an_insurance_cover_dollar,
+ default min_insurance_dollar )
+ precondition( an_insurance_cover_dollar > 0.0 ) // positive insurance
+ ) ; // Deferred body definition.
+
+ CONTRACT_DESTRUCTOR( // Destroy courier.
+ public virtual (~courier) ( void )
+ ) ;
+
+ // Queries.
+
+ CONTRACT_FUNCTION( // Return insurance cover.
+ public double (insurance_cover_dollar) ( void ) const
+ ) ;
+
+ // Commands.
+
+ CONTRACT_FUNCTION( // Deliver package to destination.
+ public virtual void (deliver) ( (package&) the_package,
+ (std::string const) destination )
+ precondition(
+ the_package.weight_kg < 5.0 // within max wight
+ )
+ postcondition(
+ (the_package.delivered_hour - the_package.accepted_hour) <=
+ 3.0, // within max delivery time
+ the_package.location == destination // delivered at destination
+ )
+ ) ;
+
+private:
+ double insurance_cover_dollar_;
+};
+
+CONTRACT_CLASS( // Different courier for package delivery.
+class (different_courier) extends( public courier )
+) {
+ CONTRACT_CLASS_INVARIANT(
+ insurance_cover_dollar() >= different_insurance_dollar,
+ static class(
+ different_insurance_dollar >= courier::min_insurance_dollar
+ )
+ )
+
+public:
+ static double different_insurance_dollar;
+
+ // Creation.
+
+ CONTRACT_CONSTRUCTOR( // Create currier with specified insurance value.
+ public explicit (different_courier) ( double const insurance_cover_dollar,
+ default different_insurance_dollar )
+ initialize( courier(insurance_cover_dollar) )
+ precondition( insurance_cover_dollar > 0.0 )
+ ) {} // Cannot separated body definition because has member initializers.
+
+ CONTRACT_DESTRUCTOR( // Destroy courier.
+ public virtual (~different_courier) ( void )
+ ) ;
+
+ // Commands.
+
+ CONTRACT_FUNCTION(
+ public virtual void (deliver) ( (package&) the_package,
+ (std::string const) destination ) override final
+ precondition(
+ // Weaker precondition on weight (i.e., it can weight more).
+ the_package.weight_kg <= 8.0
+ )
+ postcondition(
+ // Stronger postcondition on delivery time (i.e., faster delivery).
+ (the_package.delivered_hour - the_package.accepted_hour) <= 2.0
+ // Inherits "delivered at destination" postcondition.
+ )
+ ) ;
+};
+</pre>
+
+ 
+
+
+
+<pre class="programlisting">#include "courier.hpp"
+
+// Courier.
+
+double courier::min_insurance_dollar = 10.0e+6;
+
+CONTRACT_CONSTRUCTOR_BODY(courier, courier) (
+ double const an_insurance_cover_dollar ) {
+ insurance_cover_dollar_ = an_insurance_cover_dollar;
+}
+
+CONTRACT_DESTRUCTOR_BODY(courier, ~courier) ( void ) {}
+
+double courier::CONTRACT_MEMBER_BODY(insurance_cover_dollar) ( void ) const
+ { return insurance_cover_dollar_; }
+
+void courier::CONTRACT_MEMBER_BODY(deliver) ( package& the_package,
+ std::string const destination ) {
+ the_package.location = destination;
+ // Delivery takes 2.5 hours.
+ the_package.delivered_hour = the_package.accepted_hour + 2.5;
+}
+
+// Different courier.
+
+double different_courier::different_insurance_dollar = 20.0e+6;
+
+CONTRACT_DESTRUCTOR_BODY(different_courier, ~different_courier) ( void ) {}
+
+void different_courier::CONTRACT_MEMBER_BODY(deliver) ( package& the_package,
+ std::string const destination ) {
+ the_package.location = destination;
+ // Delivery takes only 0.5 hours.
+ the_package.delivered_hour = the_package.accepted_hour + 0.5;
+}
+</pre>
+
+ 
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.examples.__mitchell02___stack__simple_stack_dispenser"></a><a class="link" href="examples.html#contract__.examples.__mitchell02___stack__simple_stack_dispenser" title="[Mitchell02] Stack: Simple stack dispenser">[Mitchell02]
+ Stack: Simple stack dispenser</a>
+</h3></div></div></div>
+
+
+
+<pre class="programlisting">#include <contract.hpp>
+#include <vector>
+
+CONTRACT_CLASS( // Simple stack.
+template( typename T )
+class (stack)
+) {
+ CONTRACT_CLASS_INVARIANT_TPL( count() >= 0 ) // non-negative count
+
+public:
+ // Creation.
+
+ CONTRACT_CONSTRUCTOR_TPL( // Create empty stack.
+ public (stack) ( void )
+ postcondition( count() == 0 ) // empty
+ ) {}
+
+ CONTRACT_DESTRUCTOR_TPL( // Destroy stack.
+ public virtual (~stack) ( void )
+ ) {}
+
+ // Basic queries.
+
+ CONTRACT_FUNCTION_TPL( // Number of items.
+ public int (count) ( void ) const
+ ) {
+ return items_.size();
+ }
+
+ CONTRACT_FUNCTION_TPL( // Item at index in [1, count()] (as in Eiffel).
+ public (T const&) (item_at) ( int const index ) const
+ precondition(
+ index > 0, // positive index
+ index <= count() // index within count
+ )
+ ) {
+ return items_.at(index - 1);
+ }
+
+ // Derived queries.
+
+ CONTRACT_FUNCTION_TPL( // If no items.
+ public bool (is_empty) ( void ) const
+ postcondition(
+ auto result = return,
+ result == (count() == 0) // consistent with count
+ )
+ ) {
+ return count() == 0;
+ }
+
+ CONTRACT_FUNCTION_TPL( // Top item.
+ public (T const&) (item) ( void ) const
+ precondition( count() > 0 ) // not empty
+ postcondition(
+ auto result = return,
+ result == item_at(count()) // item on top
+ )
+ ) {
+ return item_at(count());
+ }
+
+ // Commands.
+
+ CONTRACT_FUNCTION_TPL( // Push item to the top.
+ public void (put) ( (T const&) new_item )
+ postcondition(
+ auto old_count = CONTRACT_OLDOF count(),
+ count() == old_count + 1, // count increased
+ item() == new_item // item set
+ )
+ ) {
+ items_.push_back(new_item);
+ }
+
+ CONTRACT_FUNCTION_TPL( // Pop top item.
+ public void (remove) ( void )
+ precondition( count() > 0 ) // not empty
+ postcondition(
+ auto old_count = CONTRACT_OLDOF count(),
+ count() == old_count - 1 // count decreased
+ )
+ ) {
+ items_.resize(items_.size() - 1);
+ }
+
+private:
+ std::vector<T> items_;
+};
+</pre>
+
+ 
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.examples.__mitchell02___simple_queue__simple_queue_dispenser"></a><a class="link" href="examples.html#contract__.examples.__mitchell02___simple_queue__simple_queue_dispenser" title="[Mitchell02] Simple Queue: Simple queue dispenser">[Mitchell02]
+ Simple Queue: Simple queue dispenser</a>
+</h3></div></div></div>
+
+
+
+<pre class="programlisting">#include <contract.hpp>
+#include <vector>
+
+// Importance ordering used to model assertion computational complexity.
+#define O_1 0 // O(1) constant (default)
+#define O_N 1 // O(n) linear
+
+CONTRACT_CLASS(
+template( typename T )
+class (simple_queue)
+) {
+ CONTRACT_CLASS_INVARIANT( count() >= 0 ) // non-negative count
+
+public:
+ // Creation.
+
+ CONTRACT_CONSTRUCTOR_TPL( // Create empty queue.
+ public explicit (simple_queue) ( int const the_capacity )
+ precondition( the_capacity > 0 ) // positive capacity
+ postcondition(
+ capacity() == the_capacity, // capacity set
+ is_empty() // empty
+ )
+ ) {
+ items_.reserve(the_capacity);
+ }
+
+ CONTRACT_DESTRUCTOR_TPL( // Destroy queue.
+ public virtual (~simple_queue) ( void )
+ ) {}
+
+ // Basic queries.
+
+ CONTRACT_FUNCTION_TPL( // Items in the queue (in their order).
+ public (std::vector<T> const&) (items) ( void ) const
+ ) {
+ return items_;
+ }
+
+ CONTRACT_FUNCTION_TPL( // Max number of items queue can hold.
+ public int (capacity) ( void ) const
+ ) {
+ return items_.capacity();
+ }
+
+ // Derived queries.
+
+ CONTRACT_FUNCTION_TPL( // Number of items.
+ public int (count) ( void ) const
+ postcondition(
+ auto result = return,
+ result == int(items().size()) // return items count
+ )
+ ) {
+ return items_.size();
+ }
+
+ CONTRACT_FUNCTION_TPL( // Item at head.
+ public (T const&) (head) ( void ) const
+ precondition( is_empty() == false )
+ postcondition(
+ auto result = return,
+ result == items().at(0) // return item on top
+ )
+ ) {
+ return items_.at(0);
+ }
+
+ CONTRACT_FUNCTION_TPL( // If queue contains no item.
+ public bool (is_empty) ( void ) const
+ postcondition(
+ auto result = return,
+ result == (count() == 0) // consistent with count
+ )
+ ) {
+ return items_.size() == 0;
+ }
+
+ CONTRACT_FUNCTION_TPL( // If queue has no room for another item.
+ public bool (is_full) ( void ) const
+ postcondition(
+ auto result = return,
+ result == (capacity() ==
+ int(items().size())) // consistent with size and capacity
+ )
+ ) {
+ return items_.size() == items_.capacity();
+ }
+
+ // Commands.
+
+ CONTRACT_FUNCTION_TPL( // Remove head item and shift all other items.
+ public void (remove) ( void )
+ precondition( is_empty() == false )
+ postcondition(
+ auto old_count = CONTRACT_OLDOF count(),
+ auto old_items = CONTRACT_OLDOF items(),
+ count() == old_count - 1, // count decreased
+ // Expensive assertion to check so marked using importance.
+ all_equal(items(), old_items, 1 /* shifted */), importance O_N
+ )
+ ) {
+ items_.erase(items_.begin());
+ }
+
+ CONTRACT_FUNCTION_TPL( // Add item to tail.
+ public void (put) ( (T const&) item )
+ precondition( count() < capacity() )
+ postcondition(
+ auto old_count = CONTRACT_OLDOF count(),
+ auto old_items = CONTRACT_OLDOF items(),
+ count() == old_count + 1, // count increased
+ items().at(count() - 1) == item, // second last item
+ if(count() >= 2) (
+ // Expensive assertion to check so marked using importance.
+ all_equal(items(), old_items), importance O_N
+ )
+ )
+ ) {
+ items_.push_back(item);
+ }
+
+private:
+
+ /** @todo make this static */
+ CONTRACT_FUNCTION_TPL( // Postcondition helper.
+ private bool (all_equal) ( (std::vector<T> const&) left,
+ (std::vector<T> const&) right, size_t offset, default 0
+ ) const
+ precondition( right.size() == left.size() + offset ) // correct offset
+ ) {
+ for(size_t i = offset; i < right.size(); ++i)
+ if(left.at(i - offset) != right.at(i)) return false;
+ return true;
+ }
+
+ std::vector<T> items_;
+};
+</pre>
+
+ 
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.examples.__mitchell02___customer_manager__contracts_instead_of_defensive_programming"></a><a class="link" href="examples.html#contract__.examples.__mitchell02___customer_manager__contracts_instead_of_defensive_programming" title="[Mitchell02] Customer Manager: Contracts instead of Defensive Programming">[Mitchell02]
+ Customer Manager: Contracts instead of Defensive Programming</a>
+</h3></div></div></div>
+
+
+
+<pre class="programlisting">// In header: customer_manager.hpp
+#include <contract.hpp>
+#include <string>
+#include <map>
+
+class basic_customer_details { // Basic customer information.
+ friend class customer_manager;
+
+public:
+ typedef std::string identifier;
+
+ explicit basic_customer_details(identifier const& an_id)
+ : id(an_id), name(), address(), birthday()
+ {}
+
+protected:
+ identifier id; // Customer identifier.
+ std::string name; // Customer name.
+ std::string address; // Customer address.
+ std::string birthday; // Customer date of birth.
+};
+
+CONTRACT_CLASS( // Manage customers.
+class (customer_manager)
+) {
+ CONTRACT_CLASS_INVARIANT( count() >= 0 ) // non-negative count
+
+public:
+ // Creation.
+
+ CONTRACT_CONSTRUCTOR(
+ public (customer_manager) ( void )
+ // Cannot use member initializes because deferring body definition.
+ ) ; // Deferred body definition.
+
+ CONTRACT_DESTRUCTOR(
+ public virtual (~customer_manager) ( void )
+ ) ;
+
+ // Basic queries.
+
+ CONTRACT_FUNCTION(
+ public int (count) ( void ) const
+ // Postcondition: non-negative count asserted by class invariants
+ ) ;
+
+ CONTRACT_FUNCTION( // There is a customer with given identifier.
+ public bool (id_active) ( (basic_customer_details::identifier const&) id )
+ const
+ ) ;
+
+ // Derived queries.
+
+ CONTRACT_FUNCTION( // Name of customer with given identifier.
+ public (std::string const&) (name_for) (
+ (basic_customer_details::identifier const&) id ) const
+ precondition( id_active(id) ) // id active
+ ) ;
+
+ // Commands.
+
+ CONTRACT_FUNCTION( // Add given customer.
+ public void (add) ( (basic_customer_details const&) details )
+ precondition( id_active(details.id) == false ) // id not active
+ postcondition(
+ auto old_count = CONTRACT_OLDOF count(),
+ count() == old_count + 1, // count increased
+ id_active(details.id) // id active
+ )
+ ) ;
+
+ CONTRACT_FUNCTION( // Set name of customer with given identifier.
+ public void (set_name) (
+ (basic_customer_details::identifier const&) id,
+ (std::string const&) name )
+ precondition( id_active(id) ) // id active
+ postcondition( name_for(id) == name ) // name set
+ ) ;
+
+private:
+ class agent {}; // Customer agent.
+
+ struct customer : basic_customer_details { // Basic customer.
+ agent managing_agent; // Customer agent.
+ std::string last_contact; // Customer last contacted.
+
+ explicit customer(basic_customer_details const& details)
+ : basic_customer_details(details), managing_agent()
+ , last_contact()
+ {}
+ };
+
+ std::map<basic_customer_details::identifier, customer> customers_;
+};
+</pre>
+
+ 
+
+
+
+<pre class="programlisting">#include "customer_manager.hpp"
+#include <utility>
+
+CONTRACT_CONSTRUCTOR_BODY(customer_manager, customer_manager) ( void ) {}
+
+CONTRACT_DESTRUCTOR_BODY(customer_manager, ~customer_manager) ( void ) {}
+
+int customer_manager::CONTRACT_MEMBER_BODY(count) ( void ) const
+ { return customers_.size(); }
+
+bool customer_manager::CONTRACT_MEMBER_BODY(id_active) (
+ basic_customer_details::identifier const& id) const {
+ return customers_.find(id) != customers_.end();
+}
+
+std::string const& customer_manager::CONTRACT_MEMBER_BODY(name_for) (
+ basic_customer_details::identifier const& id) const {
+ // Find != end because of `id_active()` pre so no defensive programming.
+ return customers_.find(id)->second.name;
+}
+
+void customer_manager::CONTRACT_MEMBER_BODY(add) (
+ basic_customer_details const& details )
+ { customers_.insert(std::make_pair(details.id, customer(details))); }
+
+void customer_manager::CONTRACT_MEMBER_BODY(set_name) (
+ basic_customer_details::identifier const& id,
+ std::string const& name ) {
+ // Find != end because of `id_active()` pre so no defensive programming.
+ customers_.find(id)->second.name = name;
+}
+</pre>
+
+ 
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.examples.__mitchell02___observer__contracts_for_pure_virtual_functions"></a><a class="link" href="examples.html#contract__.examples.__mitchell02___observer__contracts_for_pure_virtual_functions" title="[Mitchell02] Observer: Contracts for pure virtual functions">[Mitchell02]
+ Observer: Contracts for pure virtual functions</a>
+</h3></div></div></div>
+
+
+
+<pre class="programlisting">// In header: observer.hpp
+#include <contract.hpp>
+
+CONTRACT_CLASS( // Observer.
+class (observer)
+) {
+ CONTRACT_CLASS_INVARIANT( void ) // no invariant
+
+ friend class subject;
+
+public:
+ // Creation.
+
+ CONTRACT_CONSTRUCTOR( // Create observer.
+ public (observer) ( void )
+ ) {}
+
+ CONTRACT_DESTRUCTOR( // Destroy observer.
+ public virtual (~observer) ( void )
+ ) {}
+
+protected:
+ // Commands.
+
+ CONTRACT_FUNCTION( // If up to date with its subject.
+ protected virtual bool (up_to_date_with_subject) ( void ) const new
+ ) = 0;
+
+ CONTRACT_FUNCTION( // Update and inform its subject.
+ protected virtual void (update) ( void ) new
+ postcondition( up_to_date_with_subject() ) // up-to-date
+ ) = 0;
+};
+</pre>
+
+ 
+
+
+
+<pre class="programlisting">// In header: subject.hpp
+#include "observer.hpp"
+#include <contract.hpp>
+#include <list>
+#include <algorithm>
+
+// Importance ordering used to model assertion computational complexity.
+#define O_1 0 // O(1) constant (default)
+#define O_N 1 // O(n) linear
+
+CONTRACT_CLASS( // Subject for observer design pattern.
+class (subject)
+) {
+ CONTRACT_CLASS_INVARIANT(
+ all_observers_valid(observers()), importance O_N // observes valid
+ )
+
+public:
+ // Creation.
+
+ CONTRACT_CONSTRUCTOR( // Construct subject with no observer.
+ public (subject) ( void )
+ ) {}
+
+ CONTRACT_DESTRUCTOR( // Destroy subject.
+ public virtual (~subject) ( void )
+ ) {}
+
+ // Queries.
+
+ CONTRACT_FUNCTION( // If given observer is attached.
+ public bool (attached) ( (observer const* const) obs ) const
+ precondition( obs ) // not null
+ ) {
+ return std::find(observers_.begin(), observers_.end(), obs) !=
+ observers_.end();
+ }
+
+ // Commands.
+
+ CONTRACT_FUNCTION( // Remember given object as an observer.
+ public void (attach) ( (observer* const) obs )
+ precondition(
+ obs, // not null
+ attached(obs) == false // not already attached
+ )
+ postcondition(
+ auto old_observers = CONTRACT_OLDOF observers(),
+ attached(obs), // attached
+ other_observers_unchanged(old_observers, observers(), obs),
+ importance O_N // others not changed (frame rule)
+ )
+ ) {
+ observers_.push_back(obs);
+ }
+
+protected:
+ // Queries.
+
+ CONTRACT_FUNCTION( // All observers attached to this subject.
+ protected (std::list<observer const*>) (observers) ( void ) const
+ ) {
+ // Create list of pointers to const observers.
+ std::list<const observer*> obs;
+ for(std::list<observer*>::const_iterator
+ i = observers_.begin(); i != observers_.end(); ++i) {
+ obs.push_back(*i);
+ }
+ return obs;
+ }
+
+ // Commands.
+
+ CONTRACT_FUNCTION( // Update all attached observers.
+ protected void (notify) ( void )
+ postcondition( all_observers_updated(observers()) ) // all updated
+ ) {
+ for(std::list<observer*>::iterator
+ i = observers_.begin(); i != observers_.end(); ++i) {
+ // Class invariant ensures no null pointers in observers but
+ // class invariants not checked for non-public members so check.
+ CONTRACT_BLOCK_INVARIANT( 0 != *i ) // pointer not null
+ (*i)->update();
+ }
+ }
+
+private:
+ // Contract helpers.
+
+ /** @todo make these static */
+ CONTRACT_FUNCTION(
+ private bool (all_observers_valid) (
+ (std::list<observer const*> const&) observers ) const
+ ) {
+ for(std::list<observer const*>::const_iterator
+ i = observers.begin(); i != observers.end(); ++i) {
+ if(!(*i)) return false;
+ }
+ return true;
+ }
+
+ CONTRACT_FUNCTION(
+ private bool (other_observers_unchanged) (
+ (std::list<observer const*> const&) old,
+ (std::list<observer const*> const&) now,
+ (observer const*) obs ) const
+ precondition( obs ) // not null
+ ) {
+ std::list<observer const*> remaining = now;
+ std::remove(remaining.begin(), remaining.end(), obs);
+
+ std::list<observer const*>::const_iterator
+ remaining_it = remaining.begin();
+ std::list<observer const*>::const_iterator old_it = old.begin();
+ while(remaining.end() != remaining_it && old.end() != old_it) {
+ if(*remaining_it != *old_it) return false;
+ ++remaining_it;
+ ++old_it;
+ }
+ return true;
+ }
+
+ CONTRACT_FUNCTION(
+ private bool (all_observers_updated) (
+ (std::list<observer const*> const&) observers ) const
+ ) {
+ for(std::list<observer const*>::const_iterator
+ i = observers.begin(); i != observers.end(); ++i) {
+ if(!(*i)) return false;
+ if(!(*i)->up_to_date_with_subject()) return false;
+ }
+ return true;
+ }
+
+ std::list<observer*> observers_;
+};
+</pre>
+
+ 
+
+
+
+<pre class="programlisting">#include "observer/observer.hpp"
+#include "observer/subject.hpp"
+#include <contract.hpp>
+#include <iostream>
+
+class concrete_subject : public subject { // Implement an actual subject.
+public:
+ typedef int state; // Some state being observed.
+
+ concrete_subject(): state_() {}
+
+ void set_state (state const& the_state) { // Set state being observed.
+ std::cout << "Changing state to " << the_state << std::endl;
+ state_ = the_state;
+ notify(); // Notify observers.
+ }
+
+ state get_state() const { return state_; } // Get state being observed.
+
+private:
+ state state_;
+};
+
+CONTRACT_CLASS( // Implement of actual observer.
+class (concrete_observer) extends( public observer )
+) {
+ CONTRACT_CLASS_INVARIANT( void )
+
+public:
+ CONTRACT_CONSTRUCTOR( // Create concrete observer.
+ public explicit (concrete_observer) (
+ (concrete_subject const&) the_subject)
+ initialize( subject_(the_subject), observed_state_() )
+ ) {}
+
+private: // Implement base virtual functions.
+
+ CONTRACT_FUNCTION(
+ private bool (up_to_date_with_subject) ( void ) const override final
+ ) {
+ return true; // For simplicity, always up-to-date.
+ }
+
+ CONTRACT_FUNCTION(
+ private void (update) ( void ) override final
+ ) {
+ observed_state_ = subject_.get_state();
+ std::cout << "Observed state " << observed_state_ << std::endl;
+ }
+
+ concrete_subject const& subject_;
+ concrete_subject::state observed_state_;
+};
+
+int main ( ) {
+ std::cout << std::endl << "Constructing objects" << std::endl;
+ concrete_subject sbj;
+ concrete_observer ob(sbj);
+
+ std::cout << std::endl << "Attaching observer " << &ob
+ << std::endl;
+ sbj.attach(&ob);
+
+ concrete_subject::state st = -10;
+ std::cout << std::endl << "Setting state to " << st << std::endl;
+ sbj.set_state(st);
+
+ st = +10;
+ std::cout << std::endl << "Re-setting state to " << st << std::endl;
+ sbj.set_state(st);
+
+ std::cout << std::endl << "Destructing objects" << std::endl;
+ return 0;
+}
+</pre>
+
+ 
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.examples.mitchell02_counter"></a><a class="link" href="examples.html#contract__.examples.mitchell02_counter" title="[Mitchell02] Counter: Subcontracting and virtual specifiers (final, override, new, and pure)">[Mitchell02]
+ Counter: Subcontracting and virtual specifiers (final, override, new, and pure)</a>
+</h3></div></div></div>
+
+
+
+<pre class="programlisting">// In header: push_button.hpp
+#include <contract.hpp>
+
+CONTRACT_CLASS( // Basic button.
+class (push_button)
+) {
+ CONTRACT_CLASS_INVARIANT( void ) // no invariant
+
+public:
+ // Creation.
+
+ CONTRACT_CONSTRUCTOR( // Create an enabled button.
+ public (push_button) ( void )
+ initialize( enabled_(true) )
+ postcondition( enabled() ) // enabled
+ ) {}
+
+ CONTRACT_DESTRUCTOR( // Destroy button.
+ public virtual (~push_button) ( void )
+ ) {}
+
+ // Queries.
+
+ CONTRACT_FUNCTION( // If button enabled.
+ public bool (enabled) ( void ) const
+ ) {
+ return enabled_;
+ }
+
+ // Commands.
+
+ CONTRACT_FUNCTION( // Enable this button.
+ public void (enable) ( void )
+ postcondition( enabled() ) // enabled
+ ) {
+ enabled_ = true;
+ }
+
+ CONTRACT_FUNCTION( // Disable this button.
+ public void (disable) ( void )
+ postcondition( enabled() == false ) // disabled
+ ) {
+ enabled_ = false;
+ }
+
+ CONTRACT_FUNCTION( // Invoked externally when this button is clicked.
+ public virtual void (on_bn_clicked) ( void ) new
+ precondition( enabled() ) // enabled
+ ) = 0; // Contract for pure virtual function.
+
+private:
+ bool enabled_;
+};
+</pre>
+
+ 
+
+
+
+<pre class="programlisting">// In header: decrement_button.hpp
+#include "push_button.hpp"
+#include "counter.hpp"
+#include "../observer/observer.hpp"
+#include <contract.hpp>
+#include <boost/utility.hpp>
+
+CONTRACT_CLASS( // Button that decrements counter.
+class (decrement_button) final // Contract for final class.
+ extends( public push_button, protected observer, boost::noncopyable )
+) {
+ CONTRACT_CLASS_INVARIANT( void ) // no invariant
+
+public:
+ // Creation.
+
+ CONTRACT_CONSTRUCTOR( // Create button associated with given counter.
+ public explicit (decrement_button) ( (counter&) the_counter )
+ initialize( counter_ref_(the_counter) )
+ postcondition(
+ enabled() == (the_counter.value() > 0) // enabled iff positive value
+ )
+ ) {
+ counter_ref_.attach(this);
+ }
+
+ CONTRACT_DESTRUCTOR( // Destroy button.
+ public (~decrement_button) ( void )
+ ) {}
+
+ // Commands.
+
+ CONTRACT_FUNCTION(
+ public void (on_bn_clicked) ( void ) override
+ postcondition(
+ old_value = CONTRACT_OLDOF counter_ref_.value(),
+ counter_ref_.value() == old_value - 1 // counter decremented
+ )
+ ) {
+ counter_ref_.decrement();
+ }
+
+private:
+ CONTRACT_FUNCTION(
+ private bool (up_to_date_with_subject) ( void ) const override
+ ) {
+ return true; // For simplicity, always up-to-date.
+ }
+
+ CONTRACT_FUNCTION(
+ private void (update) ( void ) override
+ postcondition(
+ enabled() == (counter_ref_.value() > 0) // enabled if positive value
+ )
+ ) {
+ if(counter_ref_.value() == 0) disable();
+ else enable();
+ }
+
+ counter& counter_ref_;
+};
+</pre>
+
+ 
+
+
+
+<pre class="programlisting">// In header: counter.hpp
+#include "../observer/subject.hpp"
+#include <contract.hpp>
+
+CONTRACT_CLASS( // Positive integer counter.
+class (counter) extends( public subject )
+) {
+ CONTRACT_CLASS_INVARIANT( void ) // no invariants
+
+public:
+ // Creation.
+
+ CONTRACT_CONSTRUCTOR( // Construct counter with specified value.
+ public explicit (counter) ( int const a_value, default 10 )
+ initialize( value_(a_value) )
+ postcondition( value() == a_value ) // value set
+ ) {}
+
+ CONTRACT_DESTRUCTOR( // Destroy counter.
+ public virtual (~counter) ( void )
+ ) {}
+
+ // Queries.
+
+ CONTRACT_FUNCTION( // Current counter value.
+ public int (value) ( void ) const
+ ) {
+ return value_;
+ }
+
+ // Commands.
+
+ CONTRACT_FUNCTION( // Decrement counter value.
+ public void (decrement) ( void )
+ postcondition(
+ auto old_value = CONTRACT_OLDOF value(),
+ value() == old_value - 1 // decremented
+ )
+ ) {
+ --value_;
+ notify(); // Notifies all attached observers.
+ }
+
+private:
+ int value_;
+};
+</pre>
+
+ 
+
+
+
+<pre class="programlisting">// In header: view_of_counter.hpp
+#include "counter.hpp"
+#include "../observer/observer.hpp"
+#include <contract.hpp>
+#include <iostream>
+
+CONTRACT_CLASS( // Show current value of associated counter.
+class (view_of_counter) extends( private observer )
+) {
+ CONTRACT_CLASS_INVARIANT( void ) // no invariant
+
+public:
+ // Creation.
+
+ CONTRACT_CONSTRUCTOR( // Create viewer associated with given counter.
+ public explicit (view_of_counter) ( (counter&) the_counter )
+ initialize( counter_ref_(the_counter) )
+ ) {
+ counter_ref_.attach(this);
+ std::cout << std::endl << "> Counter started at " <<
+ counter_ref_.value() << std::endl << std::endl;
+ }
+
+ CONTRACT_DESTRUCTOR( // Destroy viewer.
+ public virtual (~view_of_counter) ( void )
+ ) {}
+
+private:
+ CONTRACT_FUNCTION(
+ private bool (up_to_date_with_subject) ( void ) const override final
+ ) {
+ return true; // For simplicity, always up-to-date.
+ }
+
+ CONTRACT_FUNCTION(
+ private void (update) ( void ) override final // Contract final function.
+ ) {
+ std::cout << std::endl << "> Counter changed to " <<
+ counter_ref_.value() << std::endl << std::endl;
+ }
+
+ counter& counter_ref_;
+};
+</pre>
+
+ 
+
+
+
+<pre class="programlisting">#include "counter/counter.hpp"
+#include "counter/decrement_button.hpp"
+#include "counter/view_of_counter.hpp"
+#include <iostream>
+
+int main ( ) {
+ counter cnt(3);
+ view_of_counter view(cnt);
+ decrement_button dec(cnt);
+
+ char ch = '\0';
+ while(ch != 'q') { // Simple text-based menu selection.
+ if (dec.enabled()) std::cout << "(-) Decrement counter" << std::endl;
+ std::cout << "(q) Quit" << std::endl;
+ std::cout << "Select: ";
+
+ std::cin >> ch;
+ if ('q' == ch) {
+ return 0;
+ } else if ('-' == ch && dec.enabled()) {
+ dec.on_bn_clicked();
+ } else {
+ std::cout << "Invalid selection '" << ch << "'"
+ << std::endl;
+ }
+ }
+ return 0;
+}
+</pre>
+
+ 
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.examples.__stroustrup97___string__throw_when_contract_is_broken"></a><a class="link" href="examples.html#contract__.examples.__stroustrup97___string__throw_when_contract_is_broken" title="[Stroustrup97] String: Throw when contract is broken">[Stroustrup97]
+ String: Throw when contract is broken</a>
+</h3></div></div></div>
+
+
+
+<pre class="programlisting">// In header: string.hpp
+#include <contract.hpp>
+#include <cstring>
+
+// Adapted from an example presented in [Stroustrup1997] to illustrate
+// importance of class invariants. Simple preconditions were added where it
+// made sense. This should be compiled with postconditions checking turned off
+// because postconditions are deliberately not used.
+// See [Stroustrup1997] for a discussion on the importance of class invariants,
+// and on pros and cons of using pre and post conditions.
+CONTRACT_CLASS(
+class (String)
+) {
+ CONTRACT_CLASS_INVARIANT(
+ // It would be better to assert conditions separately so to generate
+ // more informative error in case they fail.
+ p && sz >= 0 && TOO_LARGE >= sz && !p[sz] ? true : throw Invariant()
+ )
+
+ int sz;
+ char* p;
+
+public:
+ // Broken contracts throw user defined exceptions.
+ class Range {}; // exception classes
+ class Invariant {};
+ class Null {};
+ class Too_large {};
+
+ enum { TOO_LARGE = 16000 }; // length limit
+
+ CONTRACT_CONSTRUCTOR(
+ public (String) ( (const char*) q )
+ precondition(
+ q ? true : throw Null(),
+ strlen(q) <= TOO_LARGE ? true : throw Too_large()
+ )
+ ) ; // Deferred body definition.
+
+ CONTRACT_CONSTRUCTOR(
+ public (String) ( (const String&) s )
+ ) ;
+
+ CONTRACT_DESTRUCTOR(
+ public (~String) ( void )
+ ) ;
+
+ CONTRACT_FUNCTION(
+ public (char&) operator([])(at) ( int i )
+ precondition( i >= 0 && sz > i ? true : throw Range() )
+ ) ;
+
+ CONTRACT_FUNCTION(
+ public int (size) ( void ) const
+ ) ;
+
+private:
+ CONTRACT_FUNCTION( // Not public so it does not check class invariants.
+ private void (init) ( (const char*) q )
+ ) ;
+};
+</pre>
+
+ 
+
+
+
+<pre class="programlisting">#include "string.hpp"
+
+CONTRACT_CONSTRUCTOR_BODY(String, String) ( const char* q )
+ { init(q); }
+
+CONTRACT_CONSTRUCTOR_BODY(String, String) ( const String& s)
+ { init(s.p); }
+
+CONTRACT_DESTRUCTOR_BODY(String, ~String) ( void )
+ { delete[] p; }
+
+char& String::CONTRACT_MEMBER_BODY(operator([])(at)) ( int i )
+ { return p[i]; }
+
+int String::CONTRACT_MEMBER_BODY(size) ( void ) const { return sz; }
+
+void String::CONTRACT_MEMBER_BODY(init) ( const char* q ) {
+ sz = strlen(q);
+ p = new char[sz + 1];
+ for(int i = 0; i < sz; ++i) p[i] = q[i];
+ p[sz] = '\0';
+}
+</pre>
+
+ 
+
+
+
+<pre class="programlisting">#include "string.hpp"
+#include <iostream>
+
+// Handler that re-throws contract broken exceptions instead of terminating.
+void throwing_handler(const contract::from& context) {
+ if (context == contract::FROM_DESTRUCTOR) {
+ // Cannot throw from within destructor for STL exception safety.
+ std::clog << "Ignored destructor contract failure" << std::endl;
+ } else {
+ // Failure handlers always called with active an exception.
+ throw; // Re-throw active exception thrown by precondition.
+ }
+}
+
+int main ( ) {
+ // Setup contract failure handlers that throw (instead of terminate).
+ contract::set_precondition_broken(&throwing_handler);
+ contract::set_postcondition_broken(&throwing_handler);
+ contract::set_class_invariant_broken(&throwing_handler);
+ contract::set_block_invariant_broken(&throwing_handler);
+
+ std::cout << std::endl << "constructor()" << std::endl;
+ String s("A");
+
+ std::cout << std::endl << "operator[0]" << std::endl;
+ std::cout << s[0] << std::endl;
+
+ std::cout << std::endl << "operator[1] (throws)" << std::endl;
+ std::cout << s[1] << std::endl;
+
+ std::cout << std::endl << "destructor()" << std::endl;
+ return 0;
+}
+</pre>
+
+ 
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.examples.cline90_vector"></a><a class="link" href="examples.html#contract__.examples.cline90_vector" title="[Cline90] Vector: Comparison with A++ proposal syntax">[Cline90] Vector:
+ Comparison with A++ proposal syntax</a>
+</h3></div></div></div>
+<div class="informaltable"><table class="table">
+<colgroup>
+<col>
+<col>
+</colgroup>
+<thead><tr>
+<th>
+ 
+ ISO C++ (this library)
+ 
+ </th>
+<th>
+ 
+ A++ Proposals <a class="link" href="bibliography.html" title="Bibliography">[Cline90]</a>
+ 
+ </th>
+</tr></thead>
+<tbody><tr>
+<td>
+ 
+
+
+<pre xmlns:rev="http://www.cs.rpi.edu/~gregod/boost/tools/doc/revision" class="table-programlisting">// In header: vector.hpp
+#include <contract.hpp>
+
+CONTRACT_CLASS(
+template( typename T )
+class (vector)
+) {
+ // NOTE: Incomplete set of assertions addressing only `size`.
+
+ CONTRACT_CLASS_INVARIANT_TPL( size() >= 0 )
+
+public:
+ CONTRACT_CONSTRUCTOR_TPL(
+ public explicit (vector) ( int count, default 10 )
+ initialize( data_(new T[count]), size_(count) )
+ precondition( count >= 0 )
+ postcondition( size() == count )
+ ) {
+ for(int i = 0; i < size_; ++i) data_[i] = T();
+ }
+
+ CONTRACT_DESTRUCTOR_TPL(
+ public virtual (~vector) ( void )
+ ) {
+ delete[] data_;
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public int (size) ( void ) const
+ // Postcondition: Result non-negative checked by class invariant.
+ ) {
+ return size_;
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public void (resize) ( int count )
+ precondition( count >= 0 )
+ // A++ `init` is equivalent to this library OLDOF but not needed here.
+ postcondition( size() == count )
+ ) {
+ T* slice = new T[count];
+ for(int i = 0; i < count && i < size_; ++i) slice[i] = data_[i];
+ delete[] data_;
+ data_ = slice;
+ size_ = count;
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public (T&) operator([])(at) ( int index )
+ precondition(
+ index >= 0,
+ index < size()
+ )
+ ) {
+ return data_[index];
+ }
+
+private:
+ T* data_;
+ int size_;
+};
+</pre>
+
+ 
+ </td>
+<td>
+ 
+
+
+<pre xmlns:rev="http://www.cs.rpi.edu/~gregod/boost/tools/doc/revision" class="table-programlisting">// Extra spacing and newlines used to visually align with this library code.
+
+
+
+template< typename T>
+class vector
+{
+legal: // Class invariants (legal).
+ size() >= 0;
+
+public:
+ explicit vector ( int count = 10 )
+ : data_(new T[count]), size_(count)
+ {
+ for(int i = 0; i < size_; ++i) data_[i] = T();
+ }
+
+ virtual ~vector ( void )
+ {
+ delete[] data_;
+ }
+
+ int size ( ) const
+ {
+ return size_;
+ }
+
+ void resize ( int count )
+ {
+ T* slice = new T[count];
+ for(int i = 0; i < count && i < size_; ++i) slice[i] = data_[i];
+ delete[] data_;
+ data_ = slice;
+ size_ = count;
+ }
+
+ T& operator[] ( int index )
+ {
+ return data_[index];
+ }
+
+axioms: // Preconditions (require) and postconditions (promise).
+ [ int count; require count >= 0; promise size() == count ] vector(count);
+ [ int count; require count >= 0; promise size() == count ] resize(count);
+ [ int index; require index >= 0 && index < size() ] (*this)[x];
+
+private:
+ T* data_;
+ int size_;
+};
+
+
+
+
+
+
+
+
+
+
+
+</pre>
+
+ 
+ </td>
+</tr></tbody>
+</table></div>
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.examples.__cline90___vector_stack__subcontracting_from_abstract_data_type"></a><a class="link" href="examples.html#contract__.examples.__cline90___vector_stack__subcontracting_from_abstract_data_type" title="[Cline90] Vector-Stack: Subcontracting from Abstract Data Type">[Cline90]
+ Vector-Stack: Subcontracting from Abstract Data Type</a>
+</h3></div></div></div>
+
+
+
+<pre class="programlisting">#include "vector.hpp"
+#include <contract.hpp>
+
+CONTRACT_CLASS( // Stack Abstract Data Type (ADT).
+template( typename T )
+class (stack_adt)
+) {
+ // NOTE: Incomplete set of assertions addressing only empty/full issues.
+
+ CONTRACT_CLASS_INVARIANT_TPL( void ) // no invariants
+
+public:
+ CONTRACT_CONSTRUCTOR_TPL(
+ public (stack_adt) ( void )
+ // Postcondition: empty (cannot be checked because empty's
+ // postcondition uses length with is pure virtual during construction.
+ ) {
+ std::cout << "adt\n";
+ }
+
+ CONTRACT_DESTRUCTOR_TPL(
+ public (~stack_adt) ( void )
+ ) {}
+
+ CONTRACT_FUNCTION_TPL(
+ public bool (full) ( void ) const
+ postcondition(
+ auto result = return,
+ result == (length() == capacity())
+ )
+ ) {
+ return length() == capacity();
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public bool (empty) ( void ) const
+ postcondition( auto result = return, result == (length() == 0) )
+ ) {
+ return length() == 0;
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public virtual int (length) ( void ) const
+ postcondition( auto result = return, result >= 0 )
+ ) = 0;
+
+ CONTRACT_FUNCTION_TPL(
+ public virtual int (capacity) ( void ) const
+ postcondition( auto result = return, result >= 0 )
+ ) = 0;
+
+ CONTRACT_FUNCTION_TPL(
+ public virtual void (push) ( (T) value )
+ precondition( full() == false )
+ postcondition( empty() == false )
+ ) = 0; // Contract for pure virtual function.
+
+ CONTRACT_FUNCTION_TPL(
+ public virtual (T) (pop) ( void )
+ precondition( empty() == false )
+ postcondition( full() == false )
+ ) = 0;
+
+ CONTRACT_FUNCTION_TPL(
+ public virtual void (clear) ( void )
+ postcondition( empty() )
+ ) = 0;
+};
+
+CONTRACT_CLASS( // Vector-based stack.
+template( typename T )
+class (vstack) extends( public stack_adt<T> )
+) {
+ CONTRACT_CLASS_INVARIANT_TPL(
+ length() >= 0,
+ length() < capacity()
+ )
+
+public:
+ CONTRACT_CONSTRUCTOR_TPL(
+ public explicit (vstack) ( int count, default 10 )
+ initialize(
+ vect_(count), // OK, initializers executed after preconditions.
+ length_(0)
+ )
+ precondition( count >= 0 )
+ postcondition( length() == 0, capacity() == count )
+ ) {}
+
+ CONTRACT_DESTRUCTOR_TPL(
+ public virtual (~vstack) ( void )
+ ) {}
+
+ // NOTE: All following inherit contracts from `stack_adt`.
+
+ CONTRACT_FUNCTION_TPL(
+ public int (length) ( void ) const override final
+ ) {
+ return length_;
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public int (capacity) ( void ) const
+ ) {
+ return vect_.size();
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public void (push) ( (T) value ) override final
+ ) {
+ vect_[length_++] = value;
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public (T) (pop) ( void ) override final
+ ) {
+ return vect_[--length_];
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public void (clear) ( void ) override final
+ ) {
+ length_ = 0;
+ }
+
+private:
+ vector<T> vect_;
+ int length_;
+};
+</pre>
+
+ 
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.examples.__cline90___stack__a_very_simple_stack"></a><a class="link" href="examples.html#contract__.examples.__cline90___stack__a_very_simple_stack" title="[Cline90] Stack: A very simple stack">[Cline90]
+ Stack: A very simple stack</a>
+</h3></div></div></div>
+
+
+
+<pre class="programlisting">#include <contract.hpp>
+#include <vector>
+
+CONTRACT_CLASS(
+template( typename T )
+class (stack)
+) {
+ // NOTE: Incomplete set of assertions addressing only `empty` and `full`.
+
+ CONTRACT_CLASS_INVARIANT( void )
+
+public:
+ CONTRACT_CONSTRUCTOR_TPL(
+ public explicit (stack) ( int count )
+ initialize( data_() )
+ precondition( count >= 0 )
+ postcondition(
+ empty(),
+ full() == (count == 0)
+ )
+ ) {
+ data_.reserve(count);
+ }
+
+ CONTRACT_DESTRUCTOR_TPL(
+ public virtual (~stack) ( void )
+ ) {}
+
+ CONTRACT_FUNCTION_TPL(
+ public bool (empty) ( void ) const
+ ) {
+ return data_.empty();
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public bool (full) ( void ) const
+ ) {
+ return data_.size() == data_.capacity();
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public void (push) ( (T) value )
+ precondition( full() == false )
+ postcondition( empty() == false )
+ ) {
+ data_.push_back(value);
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public (T) (pop) ( void )
+ precondition( empty() == false )
+ postcondition( full() == false )
+ ) {
+ T value = data_.back();
+ data_.pop_back();
+ return value;
+ }
+
+private:
+ std::vector<T> data_;
+};
+</pre>
+
+ 
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.examples.__cline90___calendar__a_very_simple_calendar"></a><a class="link" href="examples.html#contract__.examples.__cline90___calendar__a_very_simple_calendar" title="[Cline90] Calendar: A very simple calendar">[Cline90]
+ Calendar: A very simple calendar</a>
+</h3></div></div></div>
+
+
+
+<pre class="programlisting">#include <contract.hpp>
+
+CONTRACT_CLASS(
+class (calendar)
+) {
+ CONTRACT_CLASS_INVARIANT(
+ month() >= 1,
+ month() <= 12,
+ date() >= 1,
+ date() <= days_in(month_)
+ )
+
+public:
+ CONTRACT_CONSTRUCTOR(
+ public (calendar) ( void )
+ initialize( month_(1), date_(31) )
+ postcondition( month() == 1, date() == 31 )
+ ) {}
+
+ CONTRACT_DESTRUCTOR(
+ public virtual (~calendar) ( void )
+ ) {}
+
+ CONTRACT_FUNCTION(
+ public int (month) ( void ) const
+ ) {
+ return month_;
+ }
+
+ CONTRACT_FUNCTION(
+ public int (date) ( void ) const
+ ) {
+ return date_;
+ }
+
+ CONTRACT_FUNCTION(
+ public void (reset) ( int new_month )
+ precondition( new_month >= 1, new_month <= 12 )
+ postcondition( month() == new_month )
+ ) {
+ month_ = new_month;
+ }
+
+private:
+ /** @todo make this static */
+ CONTRACT_FUNCTION(
+ private int (days_in) ( int month ) const
+ ) {
+ return 31; // For simplicity, assume all months have 31 days.
+ }
+
+ int month_, date_;
+};
+</pre>
+
+ 
+</div>
+</div>
+<table xmlns:rev="http://www.cs.rpi.edu/~gregod/boost/tools/doc/revision" width="100%"><tr>
+<td align="left"></td>
+<td align="right"><div class="copyright-footer">Copyright © 2008-2012 Lorenzo Caminiti
+ Use, modification, and distribution is subject to the Boost Software License,
+ Version 1.0 (see accompanying file LICENSE_1_0.txt or a copy at http://www.boost.org/LICENSE_1_0.txt).
+ Documentation at http://contractpp.sourceforge.net.
+ 
+</div></td>
+</tr></table>
+<hr>
+<div class="spirit-nav">
+<a accesskey="p" href="../index.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="grammar.html"><img src="../../../../../doc/src/images/next.png" alt="Next"></a>
+</div>
+</body>
+</html>

Added: sandbox/contract/libs/contract/doc/html2/contract__/bibliography.html
==============================================================================
--- (empty file)
+++ sandbox/contract/libs/contract/doc/html2/contract__/bibliography.html 2011-09-04 13:37:15 EDT (Sun, 04 Sep 2011)
@@ -0,0 +1,154 @@
+<html>
+<head>
+<meta http-equiv="Content-Type" content="text/html; charset=US-ASCII">
+<title>Bibliography</title>
+<link rel="stylesheet" href="../../../../../doc/src/boostbook.css" type="text/css">
+<meta name="generator" content="DocBook XSL Stylesheets V1.76.1">
+<link rel="home" href="../index.html" title="Contract++ 0.4.x">
+<link rel="up" href="../index.html" title="Contract++ 0.4.x">
+<link rel="prev" href="grammar.html" title="Appendix: Grammar">
+<link rel="next" href="release_notes.html" title="Release Notes">
+</head>
+<body bgcolor="white" text="black" link="#0000FF" vlink="#840084" alink="#0000FF">
+<table cellpadding="2" width="100%"><tr>
+<td valign="top"><img alt="Boost C++ Libraries" width="277" height="86" src="../../../../../boost.png"></td>
+<td align="center">Home</td>
+<td align="center">Libraries</td>
+<td align="center">People</td>
+<td align="center">FAQ</td>
+<td align="center">More</td>
+</tr></table>
+<hr>
+<div class="spirit-nav">
+<a accesskey="p" href="grammar.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="release_notes.html"><img src="../../../../../doc/src/images/next.png" alt="Next"></a>
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h2 class="title" style="clear: both">
+<a name="contract__.bibliography"></a><a class="link" href="bibliography.html" title="Bibliography">Bibliography</a>
+</h2></div></div></div>
+
+ [Bright04] W. Bright. <a href="http://www.digitalmars.com/d/2.0/dbc.html" target="_top">Contract
+ Programming for the D Programming Language.</a> 2004.
+ 
+
+ [Bright04b] W. Bright. <a href="http://www.digitalmars.com/ctg/contract.html" target="_top">Contract
+ Programming for the Digital Mars C++ Compiler.</a> 2004.
+ 
+
+ [C^2] Aechmea. <a href="http://www.programmersheaven.com/app/news/DisplayNews.aspx?NewsID=3843" target="_top">C^2
+ Contract Programming add-on for C++.</a> 2005.
+ 
+
+ [Chrome02] RemObjects. <a href="http://blogs.remobjects.com/blogs/mh/2008/05/01/p216" target="_top">Chromes:
+ Contract Programming for Object Pascal in .NET.</a> 2002.
+ 
+
+ [Cline90] M. Cline and D. Lea. "The Behaviour of C++ Classes" and
+ "Using Annotated C++". Proc. of the Symposium on Object
+ Oriented Programming Emphasizing Practical Applications, Maris College,
+ 19090.
+ 
+
+ [iContract] O. Enseling. <a href="http://www.javaworld.com/javaworld/jw-02-2001/jw-0216-cooltools.html" target="_top">iContract:
+ Contract Programming for Java.</a> 2001.
+ 
+
+ [Jcontract] Parasoft. <a href="http://www.parasoft.com/jsp/products/article.jsp?label=product_info_Jcontract" target="_top">Jcontract:
+ Contract Programming for Java.</a>
+ 
+
+ [Maley99] D. Maley and I. Spence. <a href="http://www.computer.org/portal/web/csdl/doi/10.1109/TOOLS.1999.779000" target="_top">Emulating
+ Design by Contract in C++.</a> Proceedings of TOOLS, IEEE Computer
+ Society, 1999.
+ 
+
+ [Meyer97] B. Meyer. Object Oriented Software Construction.
+ Prentice-Hall, 2nd edition, 1997.
+ 
+
+ [Mitchell02] R. Mitchell and J. McKim. Design by Contract, by Example.
+ Addison-Wesley, 2002.
+ 
+
+ [N1613] T. Ottosen. Proposal to add Design by Contract to C++.
+ The C++ Standards Committee, N1613,
+ 2004.
+ 
+
+ [N1653] C. Nelson. Working draft changes for C99 preprocessor synchronization.
+ C++ Standards Committee N1653,
+ 2004.
+ 
+
+ [N1669] T. Ottosen. Proposal to add Contract Programming to C++ (revision
+ 1). The C++ Standards Committee, N1669,
+ 2004.
+ 
+
+ [N1773] D. Abrahams, L. Crowl, T. Ottosen, and J. Widman. Proposal
+ to add Contract Programming to C++ (revision 2). The C++ Standards
+ Committee, N1773,
+ 2005.
+ 
+
+ [N1866] L. Crowl and T. Ottosen. Proposal to add Contract Programming
+ to C++ (revision 3). The C++ Standards Committee, N1866,
+ 2005.
+ 
+
+ [N1895] H. Sutter and F. Glassborow. Delegating Constructors, revision
+ 2. C++ Standards Committee, N1895,
+ 2005.
+ 
+
+ [N1962] L. Crowl and T. Ottosen. Proposal to add Contract Programming
+ to C++ (revision 4). The C++ Standards Committee, N1962,
+ 2006.
+ 
+
+ [N2081] D. Gregor, B. Stroustrup. Concepts (revision 1).
+ The C++ Standards Committee, N2081,
+ 2006.
+ 
+
+ [N2906] B. Stroustrup. Simplifying the sue of concepts.
+ The C++ Standards Committee, N2906,
+ 2009.
+ 
+
+ [SPARKAda] Praxis. <a href="http://www.praxis-his.com/sparkada/language.asp" target="_top">SPARKAda
+ (Ada-like Language with Contract Programming).</a>
+ 
+
+ [Spec#] Microsoft. <a href="http:://research.microsoft.com/en-us/projects/specsharp/" target="_top">Spec#
+ (C# Extension).</a>
+ 
+
+ [Stroustrup97] B. Stroustrup. The C++ Programming Language.
+ Prentice-Hall, 2nd Edition, 1997
+ 
+
+ [Tandin04] A. Tandin. <a href="http://www.codeproject.com/KB/macros/DbC_and_Doxygen.aspx" target="_top">Design
+ by Contract macros for C++ and link to Doxygen.</a> 2004.
+ 
+
+ [Wilson06] M. Wilson. Contract Programming 101 -- The Nuclear Reactor
+ and the Deep Space Probe. <a href="http://www.artima.com/cppsource/deepspace.html" target="_top">The
+ C++ Source</a>, 2006.
+ 
+</div>
+<table xmlns:rev="http://www.cs.rpi.edu/~gregod/boost/tools/doc/revision" width="100%"><tr>
+<td align="left"></td>
+<td align="right"><div class="copyright-footer">Copyright © 2008-2012 Lorenzo Caminiti
+ Use, modification, and distribution is subject to the Boost Software License,
+ Version 1.0 (see accompanying file LICENSE_1_0.txt or a copy at http://www.boost.org/LICENSE_1_0.txt).
+ Documentation at http://contractpp.sourceforge.net.
+ 
+</div></td>
+</tr></table>
+<hr>
+<div class="spirit-nav">
+<a accesskey="p" href="grammar.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="release_notes.html"><img src="../../../../../doc/src/images/next.png" alt="Next"></a>
+</div>
+</body>
+</html>

Added: sandbox/contract/libs/contract/doc/html2/contract__/grammar.html
==============================================================================
--- (empty file)
+++ sandbox/contract/libs/contract/doc/html2/contract__/grammar.html 2011-09-04 13:37:15 EDT (Sun, 04 Sep 2011)
@@ -0,0 +1,1055 @@
+<html>
+<head>
+<meta http-equiv="Content-Type" content="text/html; charset=US-ASCII">
+<title>Appendix: Grammar</title>
+<link rel="stylesheet" href="../../../../../doc/src/boostbook.css" type="text/css">
+<meta name="generator" content="DocBook XSL Stylesheets V1.76.1">
+<link rel="home" href="../index.html" title="Contract++ 0.4.x">
+<link rel="up" href="../index.html" title="Contract++ 0.4.x">
+<link rel="prev" href="examples.html" title="Appendix: Examples">
+<link rel="next" href="bibliography.html" title="Bibliography">
+</head>
+<body bgcolor="white" text="black" link="#0000FF" vlink="#840084" alink="#0000FF">
+<table cellpadding="2" width="100%"><tr>
+<td valign="top"><img alt="Boost C++ Libraries" width="277" height="86" src="../../../../../boost.png"></td>
+<td align="center">Home</td>
+<td align="center">Libraries</td>
+<td align="center">People</td>
+<td align="center">FAQ</td>
+<td align="center">More</td>
+</tr></table>
+<hr>
+<div class="spirit-nav">
+<a accesskey="p" href="examples.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="bibliography.html"><img src="../../../../../doc/src/images/next.png" alt="Next"></a>
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h2 class="title" style="clear: both">
+<a name="contract__.grammar"></a><a class="link" href="grammar.html" title="Appendix: Grammar">Appendix: Grammar</a>
+</h2></div></div></div>
+<div class="toc"><dl>
+<dt>Preprocessor DSEL</dt>
+<dt><a href="grammar.html#contract__.grammar.differences_with_c___syntax">Differences
+ with C++ Syntax</a></dt>
+<dt>Lexical Conventions</dt>
+<dt>Macro Interface</dt>
+<dt>Class Declarations</dt>
+<dt>Template Parameters</dt>
+<dt>Types</dt>
+<dt>Base Classes</dt>
+<dt>Function Declarations</dt>
+<dt><a href="grammar.html#contract__.grammar.function_and_operator_names">Function
+ and Operator Names</a></dt>
+<dt><a href="grammar.html#contract__.grammar.exception_specifications">Exception
+ Specifications</a></dt>
+<dt>Function Parameters</dt>
+<dt><a href="grammar.html#contract__.grammar.result_and_old_of_declarations">Result
+ and Old-Of Declarations</a></dt>
+<dt>Class Invariants</dt>
+<dt>Assertions</dt>
+<dt>Loop Variants</dt>
+<dt>Terminals</dt>
+</dl></div>
+
+ The syntax used by this library macros effectively defies a new language within
+ C++. More precisely, this library defines a new Domain-Specific Embedded Language
+ (DSEL) that the authors have named L++. This section illustrates
+ the complete L++ grammar.
+ 
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.grammar.preprocessor_dsel"></a><a class="link" href="grammar.html#contract__.grammar.preprocessor_dsel" title="Preprocessor DSEL">Preprocessor DSEL</a>
+</h3></div></div></div>
+
+ The domain of L++ is the specification of C++ program interfaces and L++
+ host language is obviously C++.
+ 
+
+ It is important to note that in contrast with other C++ DSEL which are parsed
+ using C++ template meta-programming (e.g., Boost.Phoenix and Boost.Lambda),
+ L++ is parsed "one meta-programming level higher" using C++ preprocessor
+ meta-programming. Using both processor and template meta-programming allows
+ L++ to implement rules like the following:
+ 
+<pre class="programlisting">if a member function is not public then it does not check the class invariants
+</pre>
+
+ This rule cannot be implemented using only template meta-programming because
+ (at lest to the authors' knowledge) it is not possible to check if a function
+ is public using a C++ template meta-function like <code class="computeroutput">is_public<</code>function-type<code class="computeroutput">></code>. Instead a macro <code class="computeroutput">IS_PUBLIC(</code>function-decl<code class="computeroutput">)</code> can be written to parse the function declaration
+ and expand to <code class="computeroutput">1</code> if and only if
+ the function is public:
+ 
+<pre class="programlisting">#define IS_PUBLIC(function_decl) ...
+
+IS_PUBLIC( public void f ( int x ) ) // expand to 1
+IS_PUBLIC( private void g ( int y ) ) // expand to 0
+</pre>
+
+ More in general, macros can parse L++ class and function declarations extracting
+ any declaration trait (if a constructor is <code class="computeroutput">explicit</code>, if a member function is <code class="computeroutput">virtual</code>, if a base class if <code class="computeroutput">protected</code>, etc).
+ 
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.grammar.differences_with_c___syntax"></a><a class="link" href="grammar.html#contract__.grammar.differences_with_c___syntax" title="Differences with C++ Syntax">Differences
+ with C++ Syntax</a>
+</h3></div></div></div>
+
+ Spaces and new lines do not matter in L++ however the following lexical conventions
+ are followed to improve readability:
+ 
+<div class="orderedlist"><ol class="orderedlist" type="1">
+<li class="listitem">
+ Round parenthesis are spaced when they specify a list of tokens <code class="computeroutput">( </code>token-list <code class="computeroutput">)</code>. For example, function parameters <code class="computeroutput">( int x, int y )</code>.
+ </li>
+<li class="listitem">
+ Round parenthesis are not spaced when they wrap a single token <code class="computeroutput">(</code>token<code class="computeroutput">)</code>. For example, a function name <code class="computeroutput">(myfunc)</code>.
+ </li>
+</ol></div>
+<div class="warning"><table border="0" summary="Warning">
+<tr>
+<td rowspan="2" align="center" valign="top" width="25"><img alt="[Warning]" src="../../../../../doc/src/images/warning.png"></td>
+<th align="left">Warning</th>
+</tr>
+<tr><td align="left" valign="top">
+ A bug in the MSVC preprocessor makes it not accept the following expression
+ <code class="computeroutput">(type)name</code>
+ without a space between the parenthesized type and the name. Therefore,
+ MSVC programmers should make sure to always introduce at least a space
+ or new line between type and name <code class="computeroutput">(type) name</code> (this form is also more readable).
+ </td></tr>
+</table></div>
+
+ The following is a summary of the differences between L++ and usual C++ declaration
+ syntax:
+ 
+<div class="orderedlist"><ol class="orderedlist" type="1">
+<li class="listitem">
+ Use round parenthesis <code class="computeroutput">( ... )</code>
+ instead of angular parenthesis <code class="computeroutput"><
+ ... ></code>
+ to declare template parameter lists (note that template instantiations
+ are not template declarations and they still use angular parenthesis).
+ </li>
+<li class="listitem">
+ Use round parenthesis <code class="computeroutput">( ... )</code>
+ instead of angular parenthesis <code class="computeroutput"><
+ ... ></code>
+ after a class template name to specify template specialization parameters.
+ </li>
+<li class="listitem">
+ Wrap class and function names within round parenthesis <code class="computeroutput">(</code>/name<code class="computeroutput">/)</code>.
+ </li>
+<li class="listitem">
+ Use <code class="computeroutput">extend(
+ ... )</code>
+ instead of the comma symbol <code class="computeroutput">:</code>
+ to inherit from base classes.
+ </li>
+<li class="listitem">
+ Use <code class="computeroutput">default </code>default-value
+ instead of the symbol <code class="computeroutput">= </code>default-value
+ to specify template and function parameter default values.
+ </li>
+<li class="listitem">
+ Always specify the access level <code class="computeroutput">public</code>,
+ <code class="computeroutput">protected</code>, or <code class="computeroutput">private</code> and without the trailing comma
+ <code class="computeroutput">:</code> for every constructor,
+ destructor, and member function declaration.
+ </li>
+<li class="listitem">
+ Wrap the function result and parameter types within round parenthesis
+ <code class="computeroutput">(</code>type<code class="computeroutput">)</code>. The wrapping parenthesis are allowed
+ but not required for types that only use keywords and contain no non-alphanumeric
+ symbol. For example: Both <code class="computeroutput">(const unsigned
+ int)</code>
+ and <code class="computeroutput">const unsigned
+ int</code> are allowed; Only <code class="computeroutput">(int&)</code>
+ and not <code class="computeroutput">int&</code>
+ is allowed because of the non-alphanumeric symbol <code class="computeroutput">&</code>;
+ Only <code class="computeroutput">(my_type)</code> is allowed because <code class="computeroutput">my_type</code>
+ is not a keyword.
+ </li>
+<li class="listitem">
+ Use <code class="computeroutput">initialize(
+ ... )</code>
+ instead of the comma <code class="computeroutput">: ...</code> to specify constructor member initializers.
+ </li>
+<li class="listitem">
+ Separate list elements using commas <code class="computeroutput">...
+ , ...</code>
+ if variadic macros are supported (preferred) or round parenthesis <code class="computeroutput">(...) (...)</code>
+ regardless of variadic macro support. Specify empty lists using <code class="computeroutput">( )</code> if
+ empty empty macro parameters are supported, <code class="computeroutput">(
+ void )</code>
+ if variadic macros are supported (preferred), or <code class="computeroutput">(
+ (void) )</code> regardless
+ or empty and variaid macro support.
+ </li>
+<li class="listitem">
+ Assertions, default parameter values, and select assertion if-conditions
+ must start with an alphanumeric letter or an open round parenthesis
+ <code class="computeroutput">0-9, a-z, A-Z, (</code>. For
+ example, use <code class="computeroutput">x ==
+ false</code>, <code class="computeroutput">bool(!x)</code> or <code class="computeroutput">(!x)</code>
+ instead of <code class="computeroutput">!x</code>
+ which starts with the non alphanumeric symbol <code class="computeroutput">!</code>.
+ Similarly use <code class="computeroutput">(1.23)</code> or <code class="computeroutput">double(1.23)</code>
+ instead of <code class="computeroutput">1.23</code> because
+ <code class="computeroutput">1.23</code> is a C++ non-alphanumeric
+ token (it contains <code class="computeroutput">.</code>).
+ </li>
+</ol></div>
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.grammar.lexical_conventions"></a><a class="link" href="grammar.html#contract__.grammar.lexical_conventions" title="Lexical Conventions">Lexical Conventions</a>
+</h3></div></div></div>
+
+ The following conventions are followed by this grammar:
+ 
+<div class="itemizedlist"><ul class="itemizedlist" type="disc">
+<li class="listitem">
+ <code class="computeroutput">[tokens]</code> indicates either <code class="computeroutput">tokens</code>
+ or nothing.
+ </li>
+<li class="listitem">
+ <code class="computeroutput">{expr}</code> indicates the result of the enclosed
+ expression <code class="computeroutput">expr</code>.
+ </li>
+<li class="listitem">
+ <code class="computeroutput">tokens1 |
+ tokens2</code> indicates either <code class="computeroutput">tokens1</code> or <code class="computeroutput">tokens2</code>.
+ </li>
+<li class="listitem">
+ <code class="computeroutput">tokens*</code>
+ indicates <code class="computeroutput">tokens</code> repeated
+ zero or more times.
+ </li>
+<li class="listitem">
+ Terminals are indicated in bold <code class="literal">symbol</code>.
+ </li>
+<li class="listitem">
+ Non-terminals are indicated in italic <code class="literal">symbol</code>.
+ </li>
+</ul></div>
+<div class="important"><table border="0" summary="Important">
+<tr>
+<td rowspan="2" align="center" valign="top" width="25"><img alt="[Important]" src="../../../../../doc/src/images/important.png"></td>
+<th align="left">Important</th>
+</tr>
+<tr><td align="left" valign="top">
+ The following grammar is written assuming variadic macros support and therefore
+ it uses comma separated list of tokens <code class="computeroutput">token1, token2, ...</code>. The
+ same grammar holds with parenthesized token lists <code class="computeroutput">(token1) (token2) ...</code> for
+ compilers that do not support varidiac macros or if programmers want to
+ avoid using variaidc macros to write fully ISO C++ compliant code.
+ </td></tr>
+</table></div>
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.grammar.macro_interface"></a><a class="link" href="grammar.html#contract__.grammar.macro_interface" title="Macro Interface">Macro Interface</a>
+</h3></div></div></div>
+
+ This library uses the following macros:
+ 
+<pre class="programlisting">CONTRACT_CLASS( class-decl )
+
+CONTRACT_CLASS_INVARIANT( [class-invariants] )
+CONTRACT_CLASS_INVARIANT_TPL( [class-invariants] )
+
+CONTRACT_FUNCTION( function-decl )
+CONTRACT_FUNCTION_TPL( function-decl )
+
+CONTRACT_BLOCK_INVARIANT( assertions )
+CONTRACT_BLOCK_INVARIANT_TPL( assertions )
+
+CONTRACT_LOOP( loop-decl )
+CONTRACT_LOOP_VARIANT( loop-variant )
+CONTRACT_LOOP_VARIANT_TPL( loop-variant )
+
+CONTRACT_FREE_BODY(function-name)
+CONTRACT_MEMBER_BODY(function-name)
+CONTRACT_CONSTRUCTOR_BODY(class-type, class-name)
+CONTRACT_DESTRUCTOR_BODY(class-type, ~class-name)
+</pre>
+
+ The macros with the trailing <code class="computeroutput">_TPL</code>
+ must be used when the enclosing scope is type dependant (e.g., within a class
+ template).
+ 
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.grammar.class_declarations"></a><a class="link" href="grammar.html#contract__.grammar.class_declarations" title="Class Declarations">Class Declarations</a>
+</h3></div></div></div>
+<pre class="programlisting">class-decl:
+ [[export] template( [template-params] ) [requires( boost-concept, ... )]]
+ {class | struct} (class-name)[( template-specialization-type, ... )] [final]
+ [extends( base, ... )]
+</pre>
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.grammar.template_parameters"></a><a class="link" href="grammar.html#contract__.grammar.template_parameters" title="Template Parameters">Template Parameters</a>
+</h3></div></div></div>
+<pre class="programlisting">template-params:
+ void | {template-param, ...}
+
+template-param:
+ type-template-param | value-template-param
+
+type-template-param:
+ {class | typename} type-name [, default default-type]
+
+value-template-param:
+ type value-name [, default default-value]
+</pre>
+
+ Note that if <code class="computeroutput">typename</code> appears
+ within <code class="literal">type</code> for a <code class="literal">value-template-param</code>
+ then it will be wrapped within parenthesis <code class="computeroutput">(typename ...)</code>
+ so it is distinguishable from the <code class="computeroutput">typename</code>
+ in <code class="literal">type-template-param</code>.
+ 
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.grammar.types"></a><a class="link" href="grammar.html#contract__.grammar.types" title="Types">Types</a>
+</h3></div></div></div>
+
+ This is the type used to specify value template parameter types, function
+ result types, function parameter types, etc. As specified by the following
+ grammar rules, extra parenthesis around this type are always allowed but
+ they are required only around user-defined types <code class="computeroutput">(mytype)</code>
+ or types containing non-alphanumeric symbols <code class="computeroutput">(int*)</code>.
+ 
+<pre class="programlisting">type:
+ keyword-type | (keyword-type) | (type)
+
+keyword-type:
+ type-qualifier* fundamental-type type-qualifier*
+
+type-qualifier:
+ const | volatile | long | short | signed | unsigned
+
+fundamental-type:
+ void | bool | char | double | float | int | wchar_t | size_t | ptrdiff_t
+</pre>
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.grammar.base_classes"></a><a class="link" href="grammar.html#contract__.grammar.base_classes" title="Base Classes">Base Classes</a>
+</h3></div></div></div>
+<pre class="programlisting">base:
+ [virtual] [public | protected | private] base-type
+</pre>
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.grammar.function_declarations"></a><a class="link" href="grammar.html#contract__.grammar.function_declarations" title="Function Declarations">Function Declarations</a>
+</h3></div></div></div>
+
+ Grammatic rules used to declare any function (free functions, member functions,
+ constructors, destructors, and operators). The usual constraints of C++ function
+ declarations apply (for example, it is not possible to declare a static virtual
+ member function, only constructors can use the class name as the function
+ name, etc).
+ 
+<pre class="programlisting">function-decl:
+ [public | protected | private]
+ [[export] [template( template-param, ... ) [requires( concept, ... )]]
+ [explicit] [inline] [extern] [static] [virtual]
+ [type] function-name ( [function-params] )
+ [const] [volatile] [override | new] [final]
+ [throw( [expections] )]
+ [initialize( member-initializer, ... )]
+ [precondition( assertion, ... )]
+ [postcondition( result-oldof-assertions )]
+</pre>
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.grammar.function_and_operator_names"></a><a class="link" href="grammar.html#contract__.grammar.function_and_operator_names" title="Function and Operator Names">Function
+ and Operator Names</a>
+</h3></div></div></div>
+<pre class="programlisting">function-name:
+ (function-name) | (class-name) | (~class_name) | operator-name
+
+operator-name:
+ operator(operator-symbol)(operator-arbitrary-name) | operator type |
+ operator new | operator delete | operator comma
+</pre>
+
+ Operator names are specified by the usual operator symbol followed by an
+ arbitrary alphanumeric name, for example:
+ 
+<pre class="programlisting">operator([])(at)
+operator(+)(plus)
+operator(())(call)
+operator(new[])(new_array)
+operator(delete[])(delete_array)
+</pre>
+
+ Implicit type conversion operators use the same syntax, for example:
+ 
+<pre class="programlisting">operator(int*)(int_ptr)
+operator(mytype const&)(mytype_const_ref)
+</pre>
+
+ However, if the type does not contain any alphanumeric symbol then the parenthesis
+ and the arbitrary name are optional, for example both the following are valid:
+ 
+<pre class="programlisting">operator(const int)(const_int)
+operator const int // Simpler.
+
+operator(mytype)(mytype_t)
+operator (mytype) // Simpler.
+</pre>
+
+ Similarly, the parenthesis and arbitrary name are optional for the <code class="computeroutput">new</code> and <code class="computeroutput">delete</code>
+ operators so all the followings are valid:
+ 
+<pre class="programlisting">operator(new)(new_ptr)
+operator new // Simpler.
+
+operator(delete)(delete_ptr)
+operator delete // Simpler.
+</pre>
+
+ Finally, the comma symbol <code class="computeroutput">,</code>
+ can never be used (because for macros a comma <code class="computeroutput">,</code>
+ has the special meaning of separating the macro parameters) so the "keyword"
+ <code class="computeroutput">comma</code> must be used to specify
+ the comma operator:
+ 
+<pre class="programlisting">operator(,)(comma) // Error.
+operator comma // OK.
+</pre>
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.grammar.exception_specifications"></a><a class="link" href="grammar.html#contract__.grammar.exception_specifications" title="Exception Specifications">Exception
+ Specifications</a>
+</h3></div></div></div>
+<pre class="programlisting">exceptions:
+ void | {exception-type, ...}
+</pre>
+
+ The keyword <code class="computeroutput">void</code> is used for
+ no-throw <code class="computeroutput">throw(
+ void )</code>.
+ 
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.grammar.function_parameters"></a><a class="link" href="grammar.html#contract__.grammar.function_parameters" title="Function Parameters">Function Parameters</a>
+</h3></div></div></div>
+<pre class="programlisting">function-params:
+ void | positional-function-params | shuffled-function-params
+
+positional-function-params:
+ positional-function-param, ...
+
+shuffled-function-params:
+ [namespace tag-namespace,]
+ named-function-params | deduced-function-params |
+ {named-function-params, deduced-function-params}
+
+named-function-params:
+ named-function-param, ...
+
+deduced-function-params:
+ deduce( named-function-param, ... )
+
+function-param:
+ positional-function-param | named-function-param
+
+positional-function-param:
+ [auto | register]
+ type value-name
+ [, default defaul-value]
+
+named-function-param:
+ [in | out | inout]
+ {auto | requires(predicate-metafunction) | type} value-name
+ [, default default-value]
+</pre>
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.grammar.result_and_old_of_declarations"></a><a class="link" href="grammar.html#contract__.grammar.result_and_old_of_declarations" title="Result and Old-Of Declarations">Result
+ and Old-Of Declarations</a>
+</h3></div></div></div>
+<pre class="programlisting">result_oldof_assertions:
+ [auto var-name = return, ]
+ [oldof, ...]
+ assertion, ...
+</pre>
+
+ If present, result and old-ofs declarations should appear at the top because
+ they will always be visible to all assertions plus these declarations cannot
+ be nested (within select-assertions, etc). The result declaration type is
+ always <code class="computeroutput">auto</code> because the function
+ result type is know and already specified by the function declaration.
+ 
+<pre class="programlisting">oldof:
+ {auto | type} var-name = CONTRACT_OLDOF oldof-expr
+</pre>
+
+ The macro "operator" <code class="computeroutput">CONTRACT_OLDOF</code>
+ does not require but allows parenthesis around the value expression <code class="literal">oldof-expr</code> (this is as specified
+ for the <code class="computeroutput">oldof</code> operator in
+ <a class="link" href="bibliography.html" title="Bibliography">[N1962]</a> and similarly to the
+ <code class="computeroutput">sizeof</code> operator which requires
+ parenthesis when applied to a type expression <code class="computeroutput">sizeof(size_type)</code> but not when applied to a value expression
+ <code class="computeroutput">sizeof size()</code>). The old-of declaration type is automatically
+ deduced (using Boost.Typeof) when specified as <code class="computeroutput">auto</code>
+ instead of <code class="literal">type</code>. For example, all
+ the followings are valid:
+ 
+<pre class="programlisting">auto old_size = CONTRACT_OLDOF size()
+auto old_size = CONTRACT_OLDOF(size()) // Extra parenthesis around expression (optional).
+(size_type) old_size = CONTRACT_OLDOF size() // Do not use Boost.Typeof.
+(size_type) old_size = CONTRACT_OLDOF(size()) // No Boost.Typeof and extra parenthesis.
+</pre>
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.grammar.class_invariants"></a><a class="link" href="grammar.html#contract__.grammar.class_invariants" title="Class Invariants">Class Invariants</a>
+</h3></div></div></div>
+<pre class="programlisting">class-invariants:
+ void | {class-invariant, ...}
+
+class-invariant:
+ assertion |
+ volatile class( void | [assertion, ...] ) |
+ static class( void | [assertion, ...] )
+</pre>
+
+ Volatile class invariants are assumed to have the same assertions as the
+ class invariants unless explicitly specified. Static class invariants are
+ assumed to assert nothing unless explicitly specified.
+ 
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.grammar.assertions"></a><a class="link" href="grammar.html#contract__.grammar.assertions" title="Assertions">Assertions</a>
+</h3></div></div></div>
+<pre class="programlisting">assertion:
+ expr-assertion | select-assertion |
+ using using-directive | namespace namespace-alias
+</pre>
+
+ Some basic name visibility manipulations are allowed at the local scope where
+ the assertions are being declared in case they are ever needed to simplify
+ the assertion expressions. Therefore, using-directives and namespace-aliases
+ are allowed where assertions are declaraed (this will affect all assertion
+ in the specific declaration scope). Note that these name visibility manipulations
+ have no effect on the program run-time state and therefore they do not compromise
+ the assertion constant-correctness requirement.
+ 
+<pre class="programlisting">expr-assertion:
+ bool-expr | static_assert(static-bool-expr, string-literal)
+ [, importance natural-literal]
+
+select-assertion:
+ if(bool-expr) ( expr-assertion, ... )
+ [else ( expr-assertion, ... )]
+</pre>
+
+ Note that select-assertions cannot be nested into one another. Furthermore,
+ it is not possible to specify importance ordering for the entire select-assertion
+ if-then-else expression. Eventual importance ordering must be specified for
+ the single assertions within the select-assertion if-then-else expression.
+ 
+<pre class="programlisting">bool-epxr:
+ runtime-bool-expr | const( [type] inscope-var, ... ) const-bool-expr
+</pre>
+
+ Constant-expressions <code class="computeroutput">const(
+ ... ) </code><code class="literal">const-bool-expr</code> can be used to
+ assert conditions and to check the select-assertion if-condition so to fully
+ enforce the assertion constant-correctness requirement. However, function
+ arguments, result value, old-of values, and the object <code class="computeroutput">this</code>
+ are automatically made <code class="computeroutput">const</code>
+ by this library so explicit constant-expressions only need to be used to
+ assert conditions on global variables, etc. The type of the in-scope variable
+ <code class="literal">inscope_var</code> to access
+ as <code class="computeroutput">const</code> is optional and it
+ is automatically deduced using Boost.Tyepof when it is not specified.
+ 
+<div class="note"><table border="0" summary="Note">
+<tr>
+<td rowspan="2" align="center" valign="top" width="25"><img alt="[Note]" src="../../../../../doc/src/images/note.png"></td>
+<th align="left">Note</th>
+</tr>
+<tr><td align="left" valign="top">
+
+ Alternatively, assertions could be programmed as follow:
+ 
+<pre class="programlisting">postcondition(
+ var(auto result = return)
+ var(auto old_size = CONTRACT_OLDOF size())
+ assert(size() == old_size + 1)
+ const_assert(x, y, x == y)
+ static_assert(sizeof(T) < sizeof(int), "size")
+ if(const(x, y, x == y)) (
+ ...
+ ) else (
+ ...
+ )
+)
+</pre>
+
+ An advantage of this syntax is that is does not require variadic commas
+ <code class="computeroutput">,</code> or sequencing parenthesis
+ <code class="computeroutput">()</code> to separate the assertions.
+ However, this syntax is overall more verbose, it uses more parenthesis,
+ it deviates more from <a class="link" href="bibliography.html" title="Bibliography">[N1962]</a>
+ (and Eiffel) that just list boolean expressions, and it looks less readable
+ because of <code class="computeroutput">var(...)</code>
+ when compared to the syntax adopted by this library.
+ 
+</td></tr>
+</table></div>
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.grammar.loop_variants"></a><a class="link" href="grammar.html#contract__.grammar.loop_variants" title="Loop Variants">Loop Variants</a>
+</h3></div></div></div>
+
+ A loop variant must be a non-negative integral expression that monotonically
+ decreases at each subsequent loop iteration.
+ 
+<pre class="programlisting">loop-variant:
+ natural-expr | const( [type] inscope-var, ... ) const-natural-expr
+ [, importance natural-literal]
+</pre>
+
+ The loop variant can be specified using a constant-expression <code class="computeroutput">const( ...
+ ) </code><code class="literal">const-natural-expr</code>
+ so to fully enforce the assertion constant-correctness requirement.
+ 
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.grammar.terminals"></a><a class="link" href="grammar.html#contract__.grammar.terminals" title="Terminals">Terminals</a>
+</h3></div></div></div>
+<div class="informaltable"><table class="table">
+<colgroup>
+<col>
+<col>
+</colgroup>
+<thead><tr>
+<th>
+ 
+ Terminal
+ 
+ </th>
+<th>
+ 
+ Description
+ 
+ </th>
+</tr></thead>
+<tbody>
+<tr>
+<td>
+ 
+ <code class="literal">loop-decl</code>
+ 
+ </td>
+<td>
+ 
+ A loop declaration: <code class="computeroutput">for(int i =
+ 0;
+ i <
+ 10;
+ ++i)</code>, <code class="computeroutput">while(i
+ < 10)</code>, etc.
+ 
+ </td>
+</tr>
+<tr>
+<td>
+ 
+ <code class="literal">class-type</code>
+ 
+ </td>
+<td>
+ 
+ The class type. For class templates this must include the template
+ instantiation parameters: <code class="computeroutput">vector<T, Alloc></code>.
+ 
+ </td>
+</tr>
+<tr>
+<td>
+ 
+ <code class="literal">class-name</code>
+ 
+ </td>
+<td>
+ 
+ The class name. For class templates this must not include the template
+ instantiation parameters: <code class="computeroutput">vector</code>.
+ (For non-template classes, the class type and name are the same.)
+ 
+ </td>
+</tr>
+<tr>
+<td>
+ 
+ <code class="literal">boost-concept</code>
+ 
+ </td>
+<td>
+ 
+ A concept type defined accordingly to Boost.Concept: <code class="computeroutput">boost::InputIterator</code>.
+ 
+ </td>
+</tr>
+<tr>
+<td>
+ 
+ <code class="literal">template-specialization-type</code>
+ 
+ </td>
+<td>
+ 
+ The type of a template specialization: <code class="computeroutput">void
+ (int, T)</code>.
+ 
+ </td>
+</tr>
+<tr>
+<td>
+ 
+ <code class="literal">type-name</code>
+ 
+ </td>
+<td>
+ 
+ The name of type parameter: <code class="computeroutput">T</code>.
+ 
+ </td>
+</tr>
+<tr>
+<td>
+ 
+ <code class="literal">default-type</code>
+ 
+ </td>
+<td>
+ 
+ A default parameter type: <code class="computeroutput">int</code>.
+ 
+ </td>
+</tr>
+<tr>
+<td>
+ 
+ <code class="literal">value-name</code>
+ 
+ </td>
+<td>
+ 
+ The name of a value parameter: <code class="computeroutput">x</code>.
+ 
+ </td>
+</tr>
+<tr>
+<td>
+ 
+ <code class="literal">default-value</code>
+ 
+ </td>
+<td>
+ 
+ A default parameter value: <code class="computeroutput">10</code>.
+ 
+ </td>
+</tr>
+<tr>
+<td>
+ 
+ <code class="literal">type</code>
+ 
+ </td>
+<td>
+ 
+ A type: <code class="computeroutput">int</code>, <code class="computeroutput">int const&</code>, <code class="computeroutput">mytype</code>,
+ etc.
+ 
+ </td>
+</tr>
+<tr>
+<td>
+ 
+ <code class="literal">base-type</code>
+ 
+ </td>
+<td>
+ 
+ A base class type: <code class="computeroutput">std::vector<int></code>.
+ 
+ </td>
+</tr>
+<tr>
+<td>
+ 
+ <code class="literal">member-initializer</code>
+ 
+ </td>
+<td>
+ 
+ A member initialization expression: <code class="computeroutput">vector_(count)</code>.
+ 
+ </td>
+</tr>
+<tr>
+<td>
+ 
+ <code class="literal">function-name</code>
+ 
+ </td>
+<td>
+ 
+ A function name: <code class="computeroutput">f</code>.
+ 
+ </td>
+</tr>
+<tr>
+<td>
+ 
+ <code class="literal">operator-symbol</code>
+ 
+ </td>
+<td>
+ 
+ An operator symbolic name: <code class="computeroutput">[]</code>,
+ <code class="computeroutput">+</code>, etc.
+ 
+ </td>
+</tr>
+<tr>
+<td>
+ 
+ <code class="literal">operator-arbitrary-name</code>
+ 
+ </td>
+<td>
+ 
+ An arbitrary name that does not contain any non-alphanumeric symbol:
+ <code class="computeroutput">at</code>, <code class="computeroutput">plus</code>, etc.
+ 
+ </td>
+</tr>
+<tr>
+<td>
+ 
+ <code class="literal">exception-type</code>
+ 
+ </td>
+<td>
+ 
+ The type of an exception: <code class="computeroutput">int</code>,
+ <code class="computeroutput">std::runtime_error</code>, etc.
+ 
+ </td>
+</tr>
+<tr>
+<td>
+ 
+ <code class="literal">var-name</code>
+ 
+ </td>
+<td>
+ 
+ The name of a variable being declared: <code class="computeroutput">result</code>,
+ <code class="computeroutput">old_size</code>, etc.
+ 
+ </td>
+</tr>
+<tr>
+<td>
+ 
+ <code class="literal">oldof-expr</code>
+ 
+ </td>
+<td>
+ 
+ The expression of an old-of declaration: <code class="computeroutput">size()</code>, <code class="computeroutput">x
+ + 10</code>,
+ etc.
+ 
+ </td>
+</tr>
+<tr>
+<td>
+ 
+ <code class="literal">using-directive</code>
+ 
+ </td>
+<td>
+ 
+ A using directive: <code class="computeroutput">namespace
+ std</code>, <code class="computeroutput">std::vector</code>,
+ etc.
+ 
+ </td>
+</tr>
+<tr>
+<td>
+ 
+ <code class="literal">namespace-alias</code>
+ 
+ </td>
+<td>
+ 
+ A namespace alias: <code class="computeroutput">mpl
+ = boost::mpl</code>.
+ 
+ </td>
+</tr>
+<tr>
+<td>
+ 
+ <code class="literal">static-bool-expr</code>
+ 
+ </td>
+<td>
+ 
+ A static boolean expression that can be evaluated at compile-time:
+ <code class="computeroutput">1 ==
+ 2</code>, <code class="computeroutput">sizeof(T) >=
+ sizeof(int)</code>,
+ etc.
+ 
+ </td>
+</tr>
+<tr>
+<td>
+ 
+ <code class="literal">runtime-bool-expr</code>
+ 
+ </td>
+<td>
+ 
+ A boolean expression that can be evaluated at run-time: <code class="computeroutput">x ==
+ y</code>, <code class="computeroutput">size() ==
+ old_size +
+ 1</code>, etc.
+ 
+ </td>
+</tr>
+<tr>
+<td>
+ 
+ <code class="literal">const-bool-expr</code>
+ 
+ </td>
+<td>
+ 
+ A boolean expression that can be evaluated at run-time but only
+ using some specified variables in constant-correct context: <code class="computeroutput">x ==
+ y</code>.
+ 
+ </td>
+</tr>
+<tr>
+<td>
+ 
+ <code class="literal">inscope-var</code>
+ 
+ </td>
+<td>
+ 
+ The name of a variable visible from the current scope: <code class="computeroutput">x</code>, <code class="computeroutput">y</code>,
+ etc.
+ 
+ </td>
+</tr>
+<tr>
+<td>
+ 
+ <code class="literal">natural-expr</code>
+ 
+ </td>
+<td>
+ 
+ A expression that evaluates at run-time to a non-negative integer
+ number: <code class="computeroutput">size()
+ - i</code>,
+ <code class="computeroutput">std::max(x,
+ y)</code>,
+ etc.
+ 
+ </td>
+</tr>
+<tr>
+<td>
+ 
+ <code class="literal">const-natural-expr</code>
+ 
+ </td>
+<td>
+ 
+ A expression that evaluates at run-time to a non-negative integer
+ number but inly using some specified variables in constant-correct
+ context: <code class="computeroutput">size()
+ - i</code>,
+ <code class="computeroutput">std::max(x,
+ y)</code>,
+ etc.
+ 
+ </td>
+</tr>
+<tr>
+<td>
+ 
+ <code class="literal">string-literal</code>
+ 
+ </td>
+<td>
+ 
+ A string token: <code class="computeroutput">"abc"</code>,
+ <code class="computeroutput">"invalid size"</code>,
+ etc.
+ 
+ </td>
+</tr>
+<tr>
+<td>
+ 
+ <code class="literal">natural-literal</code>
+ 
+ </td>
+<td>
+ 
+ A non-negative integer token: <code class="computeroutput">0</code>,
+ <code class="computeroutput">1</code>, <code class="computeroutput">123</code>...
+ 
+ </td>
+</tr>
+</tbody>
+</table></div>
+</div>
+</div>
+<table xmlns:rev="http://www.cs.rpi.edu/~gregod/boost/tools/doc/revision" width="100%"><tr>
+<td align="left"></td>
+<td align="right"><div class="copyright-footer">Copyright © 2008-2012 Lorenzo Caminiti
+ Use, modification, and distribution is subject to the Boost Software License,
+ Version 1.0 (see accompanying file LICENSE_1_0.txt or a copy at http://www.boost.org/LICENSE_1_0.txt).
+ Documentation at http://contractpp.sourceforge.net.
+ 
+</div></td>
+</tr></table>
+<hr>
+<div class="spirit-nav">
+<a accesskey="p" href="examples.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="bibliography.html"><img src="../../../../../doc/src/images/next.png" alt="Next"></a>
+</div>
+</body>
+</html>

Added: sandbox/contract/libs/contract/doc/html2/contract__/release_notes.html
==============================================================================
--- (empty file)
+++ sandbox/contract/libs/contract/doc/html2/contract__/release_notes.html 2011-09-04 13:37:15 EDT (Sun, 04 Sep 2011)
@@ -0,0 +1,76 @@
+<html>
+<head>
+<meta http-equiv="Content-Type" content="text/html; charset=US-ASCII">
+<title>Release Notes</title>
+<link rel="stylesheet" href="../../../../../doc/src/boostbook.css" type="text/css">
+<meta name="generator" content="DocBook XSL Stylesheets V1.76.1">
+<link rel="home" href="../index.html" title="Contract++ 0.4.x">
+<link rel="up" href="../index.html" title="Contract++ 0.4.x">
+<link rel="prev" href="bibliography.html" title="Bibliography">
+</head>
+<body bgcolor="white" text="black" link="#0000FF" vlink="#840084" alink="#0000FF">
+<table cellpadding="2" width="100%"><tr>
+<td valign="top"><img alt="Boost C++ Libraries" width="277" height="86" src="../../../../../boost.png"></td>
+<td align="center">Home</td>
+<td align="center">Libraries</td>
+<td align="center">People</td>
+<td align="center">FAQ</td>
+<td align="center">More</td>
+</tr></table>
+<hr>
+<div class="spirit-nav">
+<a accesskey="p" href="bibliography.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>
+</div>
+<div class="section">
+<div class="titlepage"><div><div><h2 class="title" style="clear: both">
+<a name="contract__.release_notes"></a><a class="link" href="release_notes.html" title="Release Notes">Release Notes</a>
+</h2></div></div></div>
+<div class="toc"><dl><dt>To-Do</dt></dl></div>
+<div class="section">
+<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.release_notes.to_do"></a><a class="link" href="release_notes.html#contract__.release_notes.to_do" title="To-Do">To-Do</a>
+</h3></div></div></div>
+
+ Remaining open items:
+ 
+<div class="orderedlist"><ol class="orderedlist" type="1">
+<li class="listitem">
+ Include all necessary headers for all files.
+ </li>
+<li class="listitem">
+ Program concept checking for functions (not just class).
+ </li>
+<li class="listitem">
+ Fix static member function contract (see some examples that fails).
+ </li>
+<li class="listitem">
+ Implement named parameters.
+ </li>
+<li class="listitem">
+ Allows const( [(type_)] var, ... ) with optional (type_) for const assertions,
+ select-assertion if-conditions, and loop variants.
+ </li>
+<li class="listitem">
+ Add support for exception spec.
+ </li>
+<li class="listitem">
+ Replace all PP_NOT with PP_COMPL when no bool conversion is needed.
+ </li>
+</ol></div>
+</div>
+</div>
+<table xmlns:rev="http://www.cs.rpi.edu/~gregod/boost/tools/doc/revision" width="100%"><tr>
+<td align="left"></td>
+<td align="right"><div class="copyright-footer">Copyright © 2008-2012 Lorenzo Caminiti
+ Use, modification, and distribution is subject to the Boost Software License,
+ Version 1.0 (see accompanying file LICENSE_1_0.txt or a copy at http://www.boost.org/LICENSE_1_0.txt).
+ Documentation at http://contractpp.sourceforge.net.
+ 
+</div></td>
+</tr></table>
+<hr>
+<div class="spirit-nav">
+<a accesskey="p" href="bibliography.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>
+</div>
+</body>
+</html>

Added: sandbox/contract/libs/contract/doc/html2/index.html
==============================================================================
--- (empty file)
+++ sandbox/contract/libs/contract/doc/html2/index.html 2011-09-04 13:37:15 EDT (Sun, 04 Sep 2011)
@@ -0,0 +1,64 @@
+<html>
+<head>
+<meta http-equiv="Content-Type" content="text/html; charset=US-ASCII">
+<title>Contract++ 0.4.x</title>
+<link rel="stylesheet" href="../../../../doc/src/boostbook.css" type="text/css">
+<meta name="generator" content="DocBook XSL Stylesheets V1.76.1">
+<link rel="home" href="index.html" title="Contract++ 0.4.x">
+<link rel="next" href="contract__/examples.html" title="Appendix: Examples">
+</head>
+<body bgcolor="white" text="black" link="#0000FF" vlink="#840084" alink="#0000FF">
+<table cellpadding="2" width="100%"><tr>
+<td valign="top"><img alt="Boost C++ Libraries" width="277" height="86" src="../../../../boost.png"></td>
+<td align="center">Home</td>
+<td align="center">Libraries</td>
+<td align="center">People</td>
+<td align="center">FAQ</td>
+<td align="center">More</td>
+</tr></table>
+<hr>
+<div class="spirit-nav"><a accesskey="n" href="contract__/examples.html"><img src="../../../../doc/src/images/next.png" alt="Next"></a></div>
+<div class="preface">
+<div class="titlepage"><div>
+<div><h2 class="title">
+<a name="contract__"></a>Contract++ 0.4.x </h2></div>
+<div><div class="authorgroup"><div class="author"><h3 class="author">
+Lorenzo Caminiti
+</h3></div></div></div>
+<div>Copyright © 2008-2012 Lorenzo Caminiti</div>
+<div><div class="legalnotice">
+<a name="id808786"></a>
+ Use, modification, and distribution is subject to the Boost Software License,
+ Version 1.0 (see accompanying file LICENSE_1_0.txt or a copy at http://www.boost.org/LICENSE_1_0.txt).
+ Documentation at http://contractpp.sourceforge.net.
+ 
+</div></div>
+</div></div>
+<div class="toc">
+Table of Contents
+<dl>
+<dt>Introduction</dt>
+<dt>Appendix: Examples</dt>
+<dt>Appendix: Grammar</dt>
+<dt>Bibliography</dt>
+<dt>Release Notes</dt>
+</dl>
+</div>
+
+ The Contract++ library implements Contract Programming (a.k.a., Design by Contract,
+ DbC) for the C++ programming language. This library also supports virtual specifiers
+ (<code class="computeroutput">final</code>, <code class="computeroutput">virtual</code>,
+ and <code class="computeroutput">new</code>), concepts, and named parameters.
+ 
+<div class="section"><div class="titlepage"><div><div><h2 class="title" style="clear: both">
+<a name="contract__.Introduction"></a><a class="link" href="index.html#contract__.Introduction" title="Introduction">Introduction</a>
+</h2></div></div></div></div>
+</div>
+<table xmlns:rev="http://www.cs.rpi.edu/~gregod/boost/tools/doc/revision" width="100%"><tr>
+<td align="left">Last revised: September 04, 2011 at 17:34:44 GMT</td>
+<td align="right"><div class="copyright-footer"></div></td>
+</tr></table>
+<hr>
+<div class="spirit-nav"><a accesskey="n" href="contract__/examples.html"><img src="../../../../doc/src/images/next.png" alt="Next"></a></div>
+</body>
+</html>

Date view	Thread view	Subject view	Author view

Boost-Commit list run by bdawes at acm.org, david.abrahams at rcn.com, gregod at cs.rpi.edu, cpdaniel at pacbell.net, john at johnmaddock.co.uk