boost/contract
2
0
Fork 0
mirror of https://github.com/boostorg/contract.git synced 2026-02-26 04:32:22 +00:00
Code Issues Projects Releases Wiki Activity

added comments to docs from all references recentely read (n/p-papers, boost emails, etc.)

Browse Source
This commit is contained in:
Lorenzo Caminiti
2017-07-20 08:44:03 -07:00
parent b68b13eac7
commit 2b73d42ee1
17 changed files with 449 additions and 75 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
example/Jamfile.v2
View File

@@ -8,8 +8,9 @@ make help : : help_exit ;
explicit help ;
test-suite features :
[ subdir-run features : introduction ]
[ subdir-run features : introduction_comments ]
[ subdir-run features : introduction ]
[ subdir-run features : introduction_public ]
[ subdir-run features : non_member ]
[ subdir-run features : lambda ]
@@ -42,6 +43,7 @@ test-suite features :
[ subdir-run features : separate_body ]
[ subdir-run features : throw_on_failure ]
[ subdir-run features : ifdef ]
[ subdir-run features : ifdef_audit ]
[ subdir-run features : ifdef_macro ]
[ subdir-run features : base_types_no_macro ]
[ subdir-run features : old_no_macro ]

56
example/features/ifdef_audit.cpp Normal file
View File

@@ -0,0 +1,56 @@
// Copyright (C) 2008-2016 Lorenzo Caminiti
// Distributed under 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).
// See: http://www.boost.org/doc/libs/release/libs/contract/doc/html/index.html
#include <boost/contract.hpp>
#include <vector>
#include <iostream>
#include <cassert>
#define CONTRACT_AUDIT // Check "audit" assertions for this example.
//[ifdef_audit
// #define this only when willing to check expensive assertions.
#ifdef CONTRACT_AUDIT
#define CONTRACT_ASSERT_AUDIT(cond) BOOST_CONTRACT_ASSERT(cond)
#else
#define CONTRACT_ASSERT_AUDIT(cond) BOOST_CONTRACT_ASSERT(true || (cond))
#endif
// Prohibitively expensive assertions, never checked (same as formal comments).
#define CONTRACT_ASSERT_AXIOM(cond) BOOST_CONTRACT_ASSERT(true || (cond))
template<typename RandomIter, typename T>
bool random_binary_search(RandomIter first, RandomIter last, T const& value) {
boost::contract::check c = boost::contract::function()
.precondition([&] {
BOOST_CONTRACT_ASSERT(first <= last);
// Expensive O(n) assertion so marked "audit".
CONTRACT_ASSERT_AUDIT(std::is_sorted(first, last));
})
;
/* ... */
//]
while(first < last) {
RandomIter middle = first + ((last - first) >> 1);
BOOST_CONTRACT_CHECK(*first <= *middle || value < *middle ||
*middle < value);
if(value < *middle) last = middle;
else if(value > *middle) first = middle + 1;
else return true;
}
return false;
}
int main() {
std::vector<char> i(3);
i[0] = 'a'; i[1] = 'b'; i[2] = 'c';
assert(random_binary_search(i.begin(), i.end(), 'b'));
return 0;
}

2
example/features/introduction.cpp
View File

@@ -11,7 +11,7 @@
#include <boost/contract.hpp>
void inc(int& x) {
boost::contract::old_ptr<int> old_x = BOOST_CONTRACT_OLDOF(x);
boost::contract::old_ptr<int> old_x = BOOST_CONTRACT_OLDOF(x); // Old values.
boost::contract::check c = boost::contract::function()
.precondition([&] {
BOOST_CONTRACT_ASSERT(x < std::numeric_limits<int>::max()); // Line 17.

2
example/features/introduction_comments.cpp
View File

@@ -9,7 +9,7 @@
//[introduction_comments
void inc(int& x)
// Precondition: x < std::numeric_limit<int>::max()
// Postcondition: x == old(x) + 1
// Postcondition: x == oldof(x) + 1
{
++x; // Function body.
}

89
example/features/introduction_public.cpp Normal file
View File

@@ -0,0 +1,89 @@
// Copyright (C) 2008-2016 Lorenzo Caminiti
// Distributed under 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).
// See: http://www.boost.org/doc/libs/release/libs/contract/doc/html/index.html
#include <boost/contract.hpp>
#include <vector>
#include <cassert>
template<typename T>
class pushable { // Somewhat arbitrary base (used just to show subcontracting).
public:
void invariant() const {
BOOST_CONTRACT_ASSERT(capacity() <= max_size());
}
virtual void push_back(T const& value,
boost::contract::virtual_* v = 0) = 0; // Pure virtual function.
protected:
virtual unsigned capacity() const = 0;
virtual unsigned max_size() const = 0;
};
template<typename T> // Contract for pure virtual function.
void pushable<T>::push_back(T const& value, boost::contract::virtual_* v) {
boost::contract::old_ptr<unsigned> old_capacity =
BOOST_CONTRACT_OLDOF(v, capacity());
boost::contract::guard c = boost::contract::public_function(v, this)
.precondition([&] {
BOOST_CONTRACT_ASSERT(capacity() < max_size());
})
.postcondition([&] {
BOOST_CONTRACT_ASSERT(capacity() >= *old_capacity);
})
;
assert(false); // Shall never execute this body.
}
//[introduction_public
template<typename T>
class vector
#define BASES public pushable<T>
: BASES
{
public:
typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types; // For subcontracting.
#undef BASES
void invariant() const { // Checked in AND with base class invariants.
BOOST_CONTRACT_ASSERT(size() <= capacity());
}
virtual void push_back(T const& value,
boost::contract::virtual_* v = 0) /* override */ { // Tag virtuals.
boost::contract::old_ptr<unsigned> old_size =
BOOST_CONTRACT_OLDOF(v, size()); // Old values for virtuals.
boost::contract::guard c = boost::contract::public_function< // For overrides.
override_push_back>(v, &vector::push_back, this, value)
.precondition([&] { // Checked in OR with base preconditions.
BOOST_CONTRACT_ASSERT(size() < max_size());
})
.postcondition([&] { // Checked in AND with base postconditions.
BOOST_CONTRACT_ASSERT(size() == *old_size + 1);
})
;
vect_.push_back(value);
}
BOOST_CONTRACT_OVERRIDE(push_back) // Define `override_push_back` above.
// Could program contracts for those as well.
unsigned size() const { return vect_.size(); }
unsigned max_size() const { return vect_.max_size(); }
unsigned capacity() const { return vect_.capacity(); }
private:
std::vector<T> vect_;
};
//]
int main() {
vector<int> vect;
vect.push_back(123);
assert(vect.size() == 1);
return 0;
}

21
example/n1962/vector.cpp
View File

@@ -470,12 +470,15 @@ public:
iterator result;
boost::contract::old_ptr<size_type> old_size =
BOOST_CONTRACT_OLDOF(size());
boost::contract::old_ptr<size_type> old_capacity =
BOOST_CONTRACT_OLDOF(capacity());
boost::contract::check c = boost::contract::public_function(this)
.precondition([&] {
BOOST_CONTRACT_ASSERT(size() < max_size());
})
.postcondition([&] {
BOOST_CONTRACT_ASSERT(size() == *old_size + 1);
BOOST_CONTRACT_ASSERT(capacity() >= *old_capacity);
BOOST_CONTRACT_ASSERT(
boost::contract::condition_if<boost::has_equal_to<T> >(
boost::bind(std::equal_to<T>(), boost::cref(*result),
@@ -531,6 +534,8 @@ public:
BOOST_CONTRACT_OLDOF(size());
boost::contract::old_ptr<size_type> old_capacity =
BOOST_CONTRACT_OLDOF(capacity());
boost::contract::old_ptr<iterator> old_where =
BOOST_CONTRACT_OLDOF(where);
boost::contract::check c = boost::contract::public_function(this)
.precondition([&] {
BOOST_CONTRACT_ASSERT(size() + std::distance(first, last) <
@@ -541,6 +546,19 @@ public:
BOOST_CONTRACT_ASSERT(size() == *old_size() +
std::distance(first, last));
BOOST_CONTRACT_ASSERT(capacity() >= *old_capacity);
if(capacity() == *old_capacity) {
BOOST_CONTRACT_ASSERT(
boost::contract::condition_if<boost::has_equal_to<T> >(
boost::bind(all_of_equal_to(),
boost::prior(*old_where),
boost::prior(*old_where) + count,
boost::cref(value)
)
)
);
// [where, end()) is invalid
}
// else [begin(), end()) is invalid
})
;
@@ -600,6 +618,9 @@ public:
boost::contract::old_ptr<vector> old_other =
BOOST_CONTRACT_OLDOF(other);
boost::contract::check c = boost::contract::public_function(this)
.precondition([&] {
BOOST_CONTRACT_ASSERT(get_allocator() == other.get_allocator());
})
.postcondition([&] {
BOOST_CONTRACT_ASSERT(
boost::contract::condition_if<boost::has_equal_to<

21
example/n1962/vector_n1962.hpp
View File

@@ -472,6 +472,7 @@ public:
}
postcondition(result) {
size() == oldof size() + 1;
capacity() >= oldof capacity();
if constexpr(boost::has_equal_to<T>::value) {
*result == value;
}
@@ -492,6 +493,8 @@ public:
void insert(iterator where, size_type count, T const& value)
precondition {
size() + count < max_size();
@@ -534,6 +537,14 @@ public:
postcondition {
size() == oldof size() + std::distance(first, last);
capacity() >= oldof capacity();
if constexpr(boost::has_equal_to<T>::value) {
if(capacity() == oldof capacity()) {
boost::algorithm::all_of_equal(boost::prior(oldof where),
boost::prior(oldof where) + count, value);
}
// [where, end()) is invalid
}
// else [begin(), end()) is invalid
}
{
vect_.insert(where, first, last);
@@ -547,6 +558,13 @@ public:
iterator erase(iterator where)
precondition {
!empty();
@@ -596,6 +614,9 @@ public:
void swap(vector& other)
precondition {
get_allocator() == other.get_allocator();
}
postcondition {
if constexpr(boost::has_equal_to<T>::value) {
*this == oldof other;