Boost-Commit :

Date view	Thread view	Subject view	Author view

Subject: [Boost-commit] svn:boost r74228 - sandbox/contract/libs/contract/doc/html2/contract__
From: lorcaminiti_at_[hidden]
Date: 2011-09-04 14:00:16

Next message: lorcaminiti_at_[hidden]: "[Boost-commit] svn:boost r74229 - sandbox/contract/libs/contract/doc/html2/contract__"
Previous message: lorcaminiti_at_[hidden]: "[Boost-commit] svn:boost r74227 - in sandbox/contract/libs/contract/doc/html2: . contract__"

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

Log:
Renaming.
Removed:
sandbox/contract/libs/contract/doc/html2/contract__/Examples.html

Deleted: sandbox/contract/libs/contract/doc/html2/contract__/Examples.html
==============================================================================
--- sandbox/contract/libs/contract/doc/html2/contract__/Examples.html 2011-09-04 14:00:15 EDT (Sun, 04 Sep 2011)
+++ (empty file)
@@ -1,4470 +0,0 @@
-<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>

Next message: lorcaminiti_at_[hidden]: "[Boost-commit] svn:boost r74229 - sandbox/contract/libs/contract/doc/html2/contract__"
Previous message: lorcaminiti_at_[hidden]: "[Boost-commit] svn:boost r74227 - in sandbox/contract/libs/contract/doc/html2: . contract__"

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