Boost-Commit mailing page: [Boost-commit] svn:boost r74486 - in sandbox/contract/libs/contract/doc/html2: . contract_

Date view	Thread view	Subject view	Author view

Subject: [Boost-commit] svn:boost r74486 - in sandbox/contract/libs/contract/doc/html2: . contract__
From: lorcaminiti_at_[hidden]
Date: 2011-09-21 12:45:13

Author: lcaminiti
Date: 2011-09-21 12:45:12 EDT (Wed, 21 Sep 2011)
New Revision: 74486
URL: http://svn.boost.org/trac/boost/changeset/74486

Log:
Upd docs.
Text files modified:
   sandbox/contract/libs/contract/doc/html2/contract__/examples.html | 303 ++++++++++++++++++++++++---------------
   sandbox/contract/libs/contract/doc/html2/contract__/grammar.html | 44 +---
   sandbox/contract/libs/contract/doc/html2/index.html | 4
   3 files changed, 204 insertions(+), 147 deletions(-)

Modified: sandbox/contract/libs/contract/doc/html2/contract__/examples.html
==============================================================================
--- sandbox/contract/libs/contract/doc/html2/contract__/examples.html (original)
+++ sandbox/contract/libs/contract/doc/html2/contract__/examples.html 2011-09-21 12:45:12 EDT (Wed, 21 Sep 2011)
@@ -37,8 +37,8 @@
 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___square_root__default_parameters_and_comparison_with_d_syntax">[N1962]
+ Square Root: Default parameters and comparison with D syntax</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
@@ -93,10 +93,10 @@
 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___stack__function_try_blocks_and_exception_specifications">[Cline90]
+ Stack: Function-try-blocks and exception specifications</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>
@@ -218,68 +218,68 @@

 CONTRACT_CONSTRUCTOR_TPL(
 public (vector) ( void ) // Must always specify the access level (public).
- initialize( vect_() ) // Member initializers.
 postcondition( empty() == false )
+ initialize( vect_() ) // Member initializers.
 ) {}

 CONTRACT_CONSTRUCTOR_TPL(
 public explicit (vector) ( (const Alloc&) al )
- initialize( vect_(al) )
 postcondition( empty(), al == get_allocator() )
+ initialize( vect_(al) )
 ) {}

 CONTRACT_CONSTRUCTOR_TPL(
 public explicit (vector) ( (size_type) count )
- initialize( vect_(count) )
 postcondition(
 size() == count,
 contract::trivial::range(begin(), end()) == T()
 )
+ initialize( vect_(count) )
 ) {}

 CONTRACT_CONSTRUCTOR_TPL(
 public (vector) ( (size_type) count, (const T&) val )
- initialize( vect_(count, val) )
 postcondition(
 size() == count,
 contract::trivial::range(begin(), end()) == val
 )
+ initialize( vect_(count, val) )
 ) {}

 CONTRACT_CONSTRUCTOR_TPL(
 public (vector) ( (size_type) count, (const T&) val, (const Alloc&) al )
- initialize( vect_(count, val, al) )
 postcondition(
 size() == count,
 contract::trivial::range(begin(), end()) == val,
 al == get_allocator()
 )
+ initialize( vect_(count, val, al) )
 ) {}

 CONTRACT_CONSTRUCTOR_TPL( // With concept requirements.
 public template( class InIt ) requires( boost::InputIterator<InIt> )
 (vector) ( (InIt) first, (InIt) last )
- initialize( vect_(first, last) )
 postcondition( std::distance(first, last) == int(size()) )
+ initialize( vect_(first, last) )
 ) {}

 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(
 std::distance(first, last) == int(size()),
 al == get_allocator()
 )
+ initialize( vect_(first, last, al) )
 ) {}

 CONTRACT_CONSTRUCTOR_TPL(
 public (vector) ( (const vector&) right )
- initialize( vect_(right.vect_) )
 postcondition(
 using contract::trivial::range,
 range(begin(), end()) == range(right.begin(), right.end())
 )
+ initialize( vect_(right.vect_) )
 ) {}

 CONTRACT_FUNCTION_TPL( // Operator symbol and (arbitrary) name `copy`.
@@ -684,68 +684,68 @@

 // `public:` and `void` used to visually align with this library code.
 public: vector ( void )
- : vect_()
 postcondition { empty() == false; }
+ : vect_()
 {}

 public: explicit vector ( const Alloc& al )
- : vect_(al)
 postcondition { empty(); al == get_allocator(); }
+ : vect_(al)
 {}

 public: explicit vector ( size_type count )
- : vect_(count)
 postcondition {
 size() == count;
 all_equals(begin(), end(), T());
 }
+ : vect_(count)
 {}

 public: vector ( size_type count, const T& val )
- : vect_(count, val)
 postcondition {
 size() == count;
 all_equals(begin(), end(), val);
 }
+ : vect_(count, 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();
 }
+ : vect_(count, val, al)
 {}

 public: template< class InIt > requires std::InputIterator<InIt>
 vector ( InIt first, InIt last )
- : vect_(first, last)
 postcondition { std::distance(first, last) == int(size()); }
+ : vect_(first, last)
 {}

 public: template< class InIt > requires std::InputIterator<InIt>
 vector ( InIt first, InIt last, const Alloc& al )
- : vect_(first, last, al)
 postcondition {
 std::distance(first, last) == int(size());
 al == get_allocator();
 }
+ : vect_(first, last, al)
 {}

 public: vector ( const vector& right )
- : vect_(right.vect_)
 postcondition {

 right == *this;
 }
+ : vect_(right.vect_)
 {}

@@ -1294,13 +1294,32 @@
</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>
+<a name="contract__.examples.__n1962___square_root__default_parameters_and_comparison_with_d_syntax"></a><a class="link" href="examples.html#contract__.examples.__n1962___square_root__default_parameters_and_comparison_with_d_syntax" title="[N1962] Square Root: Default parameters and comparison with D syntax">[N1962]
+ Square Root: Default parameters and comparison with D syntax</a>
</h3></div></div></div>
-
-
+<div class="informaltable"><table class="table">
+<colgroup>
+<col>
+<col>
+</colgroup>
+<thead><tr>
+<th>
+ 
+ C++03 (this library)
+ 
+ </th>
+<th>
+ 
+ D (_D_)
+ 
+ </th>
+</tr></thead>
+<tbody><tr>
+<td>
+ 
+

-<pre class="programlisting">#include <contract.hpp>
+<pre xmlns:rev="http://www.cs.rpi.edu/~gregod/boost/tools/doc/revision" class="table-programlisting">#include <contract.hpp>
#include <cmath>

CONTRACT_FUNCTION( // Default value for `precision` parameter.
@@ -1315,7 +1334,31 @@
}
</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.
+
+
+
+real mysqrt ( real x ) // No default parameters in D.
+ in { assert( x >= 0 ); }
+ out(root) {
+
+ assert( std.math.fabs(root * root - x) <= 1e6 );
+ }
+body {
+ return std.math.sqrt(x);
+}
+</pre>
+
+ 
+ </td>
+</tr></tbody>
+</table></div>
</div>
<div class="section">
<div class="titlepage"><div><div><h3 class="title">
@@ -2251,12 +2294,12 @@
 // 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
 )
+ initialize( none_(none), representation_(0), error_(NO_ERROR) )
 ) {
 if(n >= 0) representation_ = stack4<T>(n);
 else error_ = SIZE_ERROR;
@@ -2416,8 +2459,8 @@
 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.
+ 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;
@@ -2822,8 +2865,8 @@
 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 )
+ initialize( courier(insurance_cover_dollar) )
 ) {} // Cannot separated body definition because has member initializers.

 CONTRACT_DESTRUCTOR( // Destroy courier.
@@ -3504,7 +3547,7 @@
public:
 CONTRACT_CONSTRUCTOR( // Create concrete observer.
 public explicit (concrete_observer) (
- (concrete_subject const&) the_subject)
+ (concrete_subject const&) the_subject )
 initialize( subject_(the_subject), observed_state_() )
 ) {}

@@ -3572,8 +3615,8 @@

 CONTRACT_CONSTRUCTOR( // Create an enabled button.
 public (push_button) ( void )
- initialize( enabled_(true) )
 postcondition( enabled() ) // enabled
+ initialize( enabled_(true) )
 ) {}

 CONTRACT_DESTRUCTOR( // Destroy button.
@@ -3636,10 +3679,10 @@

 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
 )
+ initialize( counter_ref_(the_counter) )
 ) {
 counter_ref_.attach(this);
 }
@@ -3699,8 +3742,8 @@

 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
+ initialize( value_(a_value) )
 ) {}

 CONTRACT_DESTRUCTOR( // Destroy counter.
@@ -3999,9 +4042,9 @@
public:
 CONTRACT_CONSTRUCTOR_TPL(
 public explicit (vector) ( int count, default 10 )
- initialize( data_(new T[count]), size_(count) )
 precondition( count >= 0 )
 postcondition( size() == count )
+ initialize( data_(new T[count]), size_(count) )
 ) {
 for(int i = 0; i < size_; ++i) data_[i] = T();
 }
@@ -4022,7 +4065,6 @@
 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];
@@ -4114,7 +4156,6 @@

-
</pre>

 
@@ -4124,6 +4165,114 @@
</div>
<div class="section">
<div class="titlepage"><div><div><h3 class="title">
+<a name="contract__.examples.__cline90___stack__function_try_blocks_and_exception_specifications"></a><a class="link" href="examples.html#contract__.examples.__cline90___stack__function_try_blocks_and_exception_specifications" title="[Cline90] Stack: Function-try-blocks and exception specifications">[Cline90]
+ Stack: Function-try-blocks and exception specifications</a>
+</h3></div></div></div>
+
+
+
+<pre class="programlisting">#include <contract.hpp>
+#include <exception>
+
+CONTRACT_CLASS(
+template( typename T )
+class (stack)
+) {
+ // NOTE: Incomplete set of assertions addressing only `empty` and `full`.
+
+ CONTRACT_CLASS_INVARIANT( void )
+
+public:
+ struct out_of_memory {};
+ struct error {};
+
+ CONTRACT_CONSTRUCTOR_TPL(
+ public explicit (stack) ( int capacity )
+ precondition( capacity >= 0 )
+ postcondition(
+ empty(),
+ full() == (capacity == 0)
+ )
+ // Function-try-blocks are programmed within the macros only for
+ // constructors with member initializers otherwise they are programmed
+ // with the body definition and outside the macros.
+ try initialize( // Try-block for both constructor initializers and body.
+ data_(new T[capacity]),
+ capacity_(capacity),
+ size_(0)
+ ) catch(std::bad_alloc& e) (
+ std::cerr << "out of memory for " << capacity << "-stack: " <<
+ e.what() << std::endl;
+ throw out_of_memory();
+ ) catch(std::exception& e) (
+ std::cerr << "error for " << capacity << "-stack: " << e.what() <<
+ std::endl;
+ throw; // Re-throw STL exception.
+ ) catch(...) (
+ std::cerr << "unknown error for " << capacity << "-stack" <<
+ std::endl;
+ throw error();
+ )
+ ) {
+ for(int i = 0; i < capacity_; ++i) data_[i] = T();
+ }
+
+ CONTRACT_DESTRUCTOR_TPL(
+ public virtual (~stack) ( void ) throw( void ) // Throw nothing.
+ ) try { // Function-try-block (outside the macro).
+ delete[] data_;
+ } catch(...) {
+ std::cerr << "error for stack destruction, terminating" << std::endl;
+ std::terminate(); // Destructor should never throw.
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public bool (empty) ( void ) const
+ ) {
+ return size_ == 0;
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public bool (full) ( void ) const
+ ) {
+ return size_ == capacity_;
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public void (push) ( (T) value ) throw( std::exception, error ) // Ex spec.
+ precondition( full() == false )
+ postcondition( empty() == false )
+ ) try { // Function-try-block (outside the macro).
+ data_[size_++] = value;
+ } catch(std::exception& e) {
+ std::cerr << "error for " << capacity_ << "-stack: " << e.what() <<
+ std::endl;
+ throw; // Re-throw STL exception.
+ } catch(...) {
+ std::cerr << "unknown error for " << capacity_ << "-stack" <<
+ std::endl;
+ throw error();
+ }
+
+ CONTRACT_FUNCTION_TPL(
+ public (T) (pop) ( void )
+ precondition( empty() == false )
+ postcondition( full() == false )
+ ) {
+ return data_[--size_];
+ }
+
+private:
+ T* data_;
+ int capacity_;
+ int size_;
+};
+</pre>
+
+ 
+</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>
@@ -4211,12 +4360,9 @@
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 )
+ initialize( vect_(count), length_(0) ) // OK, executed after precond.
 ) {}

 CONTRACT_DESTRUCTOR_TPL(
@@ -4265,79 +4411,6 @@
</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>
@@ -4359,8 +4432,8 @@
public:
 CONTRACT_CONSTRUCTOR(
 public (calendar) ( void )
- initialize( month_(1), date_(31) )
 postcondition( month() == 1, date() == 31 )
+ initialize( month_(1), date_(31) )
 ) {}

 CONTRACT_DESTRUCTOR(

Modified: sandbox/contract/libs/contract/doc/html2/contract__/grammar.html
==============================================================================
--- sandbox/contract/libs/contract/doc/html2/contract__/grammar.html (original)
+++ sandbox/contract/libs/contract/doc/html2/contract__/grammar.html 2011-09-21 12:45:12 EDT (Wed, 21 Sep 2011)
@@ -446,36 +446,13 @@
 The keyword <code class="computeroutput">void</code> is used for
 no-throw <code class="computeroutput">throw(
 void )</code>
- (instead of <code class="computeroutput">throw()</code>).
+ (instead of <code class="computeroutput">throw(
+ )</code>). Exception specifications apply
+ to only to exceptions thrown by the body and not to exceptions thrown by
+ the contract checking code (if the contract broken handlers are redefined
+ to throw) and to exceptions thrown by this library implementation code (in
+ case the library runs out of resources, encounters an internal error, etc).
 
-
- Exception specifications apply to the entire function call so to exceptions
- thrown by the body but also to exceptions thrown by the contract checking
- code (if the contract broken handlers are redefined to throw) and to exceptions
- thrown by this library implementation code (in case the library runs out
- of resources, encounters an internal error, etc):
- 
-<pre class="programlisting">CONTRACT_FUNCTION(
-int (f) ( int x ) throw( void ) // The entire function call (body and contracts) do not throw.
-) ;
-</pre>
-
- If exception specifications are instead programmed just outside the macros
- and before the body definition then they only apply to exceptions thrown
- by the body and not to exceptions thrown by the contract checking and implementation
- code:
- 
-<pre class="programlisting">CONTRACT_FUNCTION(
-int (f) ( int x )
-) throw( ) ; // Only the body does not throw (contracts might still throw).
-</pre>
-
- In both cases the exception specifications are part of the function declaration
- so they need to be repeated in the body function signature when the body
- is defined separately from the function declaration like in the example above:
- 
-<pre class="programlisting">int CONTRACT_FREE_BODY(f) ( int x ) throw( ) { ... } // Body definition for both function declarations above.
-</pre>
</div>
<div class="section">
<div class="titlepage"><div><div><h3 class="title">
@@ -514,7 +491,7 @@

 For functions other than constructors or constructors without member initializers,
 function-try-blocks are programmed outside the macros and around the body
- definition as usual:
+ definition as usual: [<a name="id956506" href="#ftn.id956506" class="footnote">1</a>]
 
<pre class="programlisting">CONTRACT_CONSTRUCTOR( // Constructor without member initializers.
(vector) ( void )
@@ -1142,6 +1119,13 @@
</tbody>
</table></div>
</div>
+<div class="footnotes">
+ <hr width="100" align="left">
+<div class="footnote">[<a id="ftn.id956506" href="#id956506" class="para">1</a>] 
+ Rationale. This ensures zero run-time
+ overhead for these functions when all contracts are disable at compile-time.
+ </div>
+</div>
</div>
<table xmlns:rev="http://www.cs.rpi.edu/~gregod/boost/tools/doc/revision" width="100%"><tr>
<td align="left"></td>

Modified: sandbox/contract/libs/contract/doc/html2/index.html
==============================================================================
--- sandbox/contract/libs/contract/doc/html2/index.html (original)
+++ sandbox/contract/libs/contract/doc/html2/index.html 2011-09-21 12:45:12 EDT (Wed, 21 Sep 2011)
@@ -27,7 +27,7 @@
</h3></div></div></div>
<div>Copyright © 2008-2012 Lorenzo Caminiti</div>
<div><div class="legalnotice">
-<a name="id808786"></a>
+<a name="id810142"></a>
 Use, modification, and distribution is subject to the Boost Software License,
 Version 1.0 (see accompanying file LICENSE_1_0.txt or a copy at http://www.boost.org/LICENSE_1_0.txt).
 Documentation at http://contractpp.sourceforge.net.
@@ -55,7 +55,7 @@
</h2></div></div></div></div>
</div>
<table xmlns:rev="http://www.cs.rpi.edu/~gregod/boost/tools/doc/revision" width="100%"><tr>
-<td align="left">Last revised: September 15, 2011 at 15:46:41 GMT</td>
+<td align="left">Last revised: September 21, 2011 at 16:09:23 GMT</td>
<td align="right"><div class="copyright-footer"></div></td>
</tr></table>
<hr>

Date view	Thread view	Subject view	Author view