4 files changed, 624 insertions, 0 deletions
diff --git a/src/boost/libs/contract/example/meyer97/stack3.cpp b/src/boost/libs/contract/example/meyer97/stack3.cpp
new file mode 100644
index 00000000..0da895b4
--- /dev/null
+++ b/src/boost/libs/contract/example/meyer97/stack3.cpp
@@ -0,0 +1,192 @@
+
+// Copyright (C) 2008-2018 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
+
+//[meyer97_stack3
+// File: stack3.cpp
+#include "stack4.hpp"
+#include <boost/contract.hpp>
+#include <boost/optional.hpp>
+#include <cassert>
+
+// Dispenser LIFO with max capacity using error codes.
+template<typename T>
+class stack3 {
+    friend class boost::contract::access;
+
+    void invariant() const {
+        if(!error()) {
+            BOOST_CONTRACT_ASSERT(count() >= 0); // Count non-negative.
+            BOOST_CONTRACT_ASSERT(count() <= capacity()); // Count bounded.
+            // Empty if no element.
+            BOOST_CONTRACT_ASSERT(empty() == (count() == 0));
+        }
+    }
+
+public:
+    enum error_code {
+        no_error = 0,
+        overflow_error,
+        underflow_error,
+        size_error
+    };
+
+    /* Initialization */
+
+    // Create stack for max of n elems, if n < 0 set error (no preconditions).
+    explicit stack3(int n, T const& default_value = T()) :
+            stack_(0), error_(no_error) {
+        boost::contract::check c = boost::contract::constructor(this)
+            .postcondition([&] {
+                // Error if impossible.
+                BOOST_CONTRACT_ASSERT((n < 0) == (error() == size_error));
+                // No error if possible.
+                BOOST_CONTRACT_ASSERT((n >= 0) == !error());
+                // Created if no error.
+                if(!error()) BOOST_CONTRACT_ASSERT(capacity() == n);
+            })
+        ;
+
+        if(n >= 0) stack_ = stack4<T>(n);
+        else error_ = size_error;
+    }
+
+    /* Access */
+
+    // Max number of stack elements.
+    int capacity() const {
+        // Check invariants.
+        boost::contract::check c = boost::contract::public_function(this);
+        return stack_.capacity();
+    }
+
+    // Number of stack elements.
+    int count() const {
+        // Check invariants.
+        boost::contract::check c = boost::contract::public_function(this);
+        return stack_.count();
+    }
+
+    // Top element if present, otherwise none and set error (no preconditions).
+    boost::optional<T const&> item() const {
+        boost::contract::check c = boost::contract::public_function(this)
+            .postcondition([&] {
+                // Error if impossible.
+                BOOST_CONTRACT_ASSERT(empty() == (error() == underflow_error));
+                // No error if possible.
+                BOOST_CONTRACT_ASSERT(!empty() == !error());
+            })
+        ;
+
+        if(!empty()) {
+            error_ = no_error;
+            return boost::optional<T const&>(stack_.item());
+        } else {
+            error_ = underflow_error;
+            return boost::optional<T const&>();
+        }
+    }
+
+    /* Status Report */
+
+    // Error indicator set by various operations.
+    error_code error() const {
+        // Check invariants.
+        boost::contract::check c = boost::contract::public_function(this);
+        return error_;
+    }
+
+    bool empty() const {
+        // Check invariants.
+        boost::contract::check c = boost::contract::public_function(this);
+        return stack_.empty();
+    }
+
+    bool full() const {
+        // Check invariants.
+        boost::contract::check c = boost::contract::public_function(this);
+        return stack_.full();
+    }
+
+    /* Element Change */
+
+    // Add x to top if capacity allows, otherwise set error (no preconditions).
+    void put(T const& x) {
+        boost::contract::old_ptr<bool> old_full = BOOST_CONTRACT_OLDOF(full());
+        boost::contract::old_ptr<int> old_count = BOOST_CONTRACT_OLDOF(count());
+        boost::contract::check c = boost::contract::public_function(this)
+            .postcondition([&] {
+                // Error if impossible.
+                BOOST_CONTRACT_ASSERT(*old_full == (error() == overflow_error));
+                // No error if possible.
+                BOOST_CONTRACT_ASSERT(!*old_full == !error());
+                if(!error()) { // If no error...
+                    BOOST_CONTRACT_ASSERT(!empty()); // ...not empty.
+                    BOOST_CONTRACT_ASSERT(*item() == x); // ...added to top.
+                    // ...one more.
+                    BOOST_CONTRACT_ASSERT(count() == *old_count + 1);
+                }
+            })
+        ;
+
+        if(full()) error_ = overflow_error;
+        else {
+            stack_.put(x);
+            error_ = no_error;
+        }
+    }
+
+    // Remove top element if possible, otherwise set error (no preconditions).
+    void remove() {
+        boost::contract::old_ptr<bool> old_empty =
+                BOOST_CONTRACT_OLDOF(empty());
+        boost::contract::old_ptr<int> old_count = BOOST_CONTRACT_OLDOF(count());
+        boost::contract::check c = boost::contract::public_function(this)
+            .postcondition([&] {
+                // Error if impossible.
+                BOOST_CONTRACT_ASSERT(*old_empty == (error() ==
+                        underflow_error));
+                // No error if possible.
+                BOOST_CONTRACT_ASSERT(!*old_empty == !error());
+                if(!error()) { // If no error...
+                    BOOST_CONTRACT_ASSERT(!full()); // ...not full.
+                    // ...one less.
+                    BOOST_CONTRACT_ASSERT(count() == *old_count - 1);
+                }
+            })
+        ;
+
+        if(empty()) error_ = underflow_error;
+        else {
+            stack_.remove();
+            error_ = no_error;
+        }
+    }
+
+private:
+    stack4<T> stack_;
+    mutable error_code error_;
+};
+
+int main() {
+    stack3<int> s(3);
+    assert(s.capacity() == 3);
+    assert(s.count() == 0);
+    assert(s.empty());
+    assert(!s.full());
+
+    s.put(123);
+    assert(!s.empty());
+    assert(!s.full());
+    assert(*s.item() == 123);
+    
+    s.remove();
+    assert(s.empty());
+    assert(!s.full());
+
+    return 0;
+}
+//]
+
diff --git a/src/boost/libs/contract/example/meyer97/stack4.e b/src/boost/libs/contract/example/meyer97/stack4.e
new file mode 100644
index 00000000..85d6e539
--- /dev/null
+++ b/src/boost/libs/contract/example/meyer97/stack4.e
@@ -0,0 +1,201 @@
+
+-- Copyright (C) 2008-2018 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
+
+//[meyer97_stack4_e
+-- Extra spaces, newlines, etc. for visual alignment with this library code.
+
+
+
+
+
+indexing
+    destription: "Dispenser with LIFO access policy and a fixed max capacity."
+class interface STACK4[G] creation make -- Interface only (no implementation).
+
+
+
+
+
+
+
+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
+
+-- End.
+//]
+
diff --git a/src/boost/libs/contract/example/meyer97/stack4.hpp b/src/boost/libs/contract/example/meyer97/stack4.hpp
new file mode 100644
index 00000000..541625cc
--- /dev/null
+++ b/src/boost/libs/contract/example/meyer97/stack4.hpp
@@ -0,0 +1,201 @@
+
+// Copyright (C) 2008-2018 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
+
+//[meyer97_stack4
+// File: stack4.hpp
+#ifndef STACK4_HPP_
+#define STACK4_HPP_
+
+#include <boost/contract.hpp>
+
+// Dispenser with LIFO access policy and fixed max capacity.
+template<typename T>
+class stack4
+    #define BASES private boost::contract::constructor_precondition<stack4<T> >
+    : BASES
+{
+    friend boost::contract::access;
+    typedef BOOST_CONTRACT_BASE_TYPES(BASES) base_types;
+    #undef BASES
+
+    void invariant() const {
+        BOOST_CONTRACT_ASSERT(count() >= 0); // Count non-negative.
+        BOOST_CONTRACT_ASSERT(count() <= capacity()); // Count bounded.
+        BOOST_CONTRACT_ASSERT(empty() == (count() == 0)); // Empty if no elem.
+    }
+
+public:
+    /* Initialization */
+
+    // Allocate static from a maximum of n elements.
+    explicit stack4(int n) :
+        boost::contract::constructor_precondition<stack4>([&] {
+            BOOST_CONTRACT_ASSERT(n >= 0); // Non-negative capacity.
+        })
+    {
+        boost::contract::check c = boost::contract::constructor(this)
+            .postcondition([&] {
+                BOOST_CONTRACT_ASSERT(capacity() == n); // Capacity set.
+            })
+        ;
+
+        capacity_ = n;
+        count_ = 0;
+        array_ = new T[n];
+    }
+
+    // Deep copy via constructor.
+    /* implicit */ stack4(stack4 const& other) {
+        boost::contract::check c = boost::contract::constructor(this)
+            .postcondition([&] {
+                BOOST_CONTRACT_ASSERT(capacity() == other.capacity());
+                BOOST_CONTRACT_ASSERT(count() == other.count());
+                BOOST_CONTRACT_ASSERT_AXIOM(*this == other);
+            })
+        ;
+
+        capacity_ = other.capacity_;
+        count_ = other.count_;
+        array_ = new T[other.capacity_];
+        for(int i = 0; i < other.count_; ++i) array_[i] = other.array_[i];
+    }
+
+    // Deep copy via assignment.
+    stack4& operator=(stack4 const& other) {
+        boost::contract::check c = boost::contract::public_function(this)
+            .postcondition([&] {
+                BOOST_CONTRACT_ASSERT(capacity() == other.capacity());
+                BOOST_CONTRACT_ASSERT(count() == other.count());
+                BOOST_CONTRACT_ASSERT_AXIOM(*this == other);
+            })
+        ;
+
+        delete[] array_;
+        capacity_ = other.capacity_;
+        count_ = other.count_;
+        array_ = new T[other.capacity_];
+        for(int i = 0; i < other.count_; ++i) array_[i] = other.array_[i];
+        return *this;
+    }
+
+    // Destroy this stack.
+    virtual ~stack4() {
+        // Check invariants.
+        boost::contract::check c = boost::contract::destructor(this);
+        delete[] array_;
+    }
+
+    /* Access */
+
+    // Max number of stack elements.
+    int capacity() const {
+        // Check invariants.
+        boost::contract::check c = boost::contract::public_function(this);
+        return capacity_;
+    }
+
+    // Number of stack elements.
+    int count() const {
+        // Check invariants.
+        boost::contract::check c = boost::contract::public_function(this);
+        return count_;
+    }
+
+    // Top element.
+    T const& item() const {
+        boost::contract::check c = boost::contract::public_function(this)
+            .precondition([&] {
+                BOOST_CONTRACT_ASSERT(!empty()); // Not empty (i.e., count > 0).
+            })
+        ;
+
+        return array_[count_ - 1];
+    }
+    
+    /* Status Report */
+
+    // Is stack empty?
+    bool empty() const {
+        bool result;
+        boost::contract::check c = boost::contract::public_function(this)
+            .postcondition([&] {
+                // Empty definition.
+                BOOST_CONTRACT_ASSERT(result == (count() == 0));
+            })
+        ;
+
+        return result = (count_ == 0);
+    }
+
+    // Is stack full?
+    bool full() const {
+        bool result;
+        boost::contract::check c = boost::contract::public_function(this)
+            .postcondition([&] {
+                BOOST_CONTRACT_ASSERT( // Full definition.
+                        result == (count() == capacity()));
+            })
+        ;
+
+        return result = (count_ == capacity_);
+    }
+
+    /* Element Change */
+
+    // Add x on top.
+    void put(T const& x) {
+        boost::contract::old_ptr<int> old_count = BOOST_CONTRACT_OLDOF(count());
+        boost::contract::check c = boost::contract::public_function(this)
+            .precondition([&] {
+                BOOST_CONTRACT_ASSERT(!full()); // Not full.
+            })
+            .postcondition([&] {
+                BOOST_CONTRACT_ASSERT(!empty()); // Not empty.
+                BOOST_CONTRACT_ASSERT(item() == x); // Added to top.
+                BOOST_CONTRACT_ASSERT(count() == *old_count + 1); // One more.
+            })
+        ;
+
+        array_[count_++] = x;
+    }
+
+    // Remove top element.
+    void remove() {
+        boost::contract::old_ptr<int> old_count = BOOST_CONTRACT_OLDOF(count());
+        boost::contract::check c = boost::contract::public_function(this)
+            .precondition([&] {
+                BOOST_CONTRACT_ASSERT(!empty()); // Not empty (i.e., count > 0).
+            })
+            .postcondition([&] {
+                BOOST_CONTRACT_ASSERT(!full()); // Not full.
+                BOOST_CONTRACT_ASSERT(count() == *old_count - 1); // One less.
+            })
+        ;
+
+        --count_;
+    }
+
+    /* Friend Helpers */
+
+    friend bool operator==(stack4 const& left, stack4 const& right) {
+        boost::contract::check inv1 = boost::contract::public_function(&left);
+        boost::contract::check inv2 = boost::contract::public_function(&right);
+        if(left.count_ != right.count_) return false;
+        for(int i = 0; i < left.count_; ++i) {
+            if(left.array_[i] != right.array_[i]) return false;
+        }
+        return true;
+    }
+
+private:
+    int capacity_;
+    int count_;
+    T* array_; // Internally use C-style array.
+};
+
+#endif // #include guard
+//]
+
diff --git a/src/boost/libs/contract/example/meyer97/stack4_main.cpp b/src/boost/libs/contract/example/meyer97/stack4_main.cpp
new file mode 100644
index 00000000..0ea28896
--- /dev/null
+++ b/src/boost/libs/contract/example/meyer97/stack4_main.cpp
@@ -0,0 +1,30 @@
+
+// Copyright (C) 2008-2018 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
+
+//[meyer97_stack4_main
+#include "stack4.hpp"
+#include <cassert>
+
+int main() {
+    stack4<int> s(3);
+    assert(s.capacity() == 3);
+    assert(s.count() == 0);
+    assert(s.empty());
+    assert(!s.full());
+
+    s.put(123);
+    assert(!s.empty());
+    assert(!s.full());
+    assert(s.item() == 123);
+
+    s.remove();
+    assert(s.empty());
+    assert(!s.full());
+
+    return 0;
+}
+//]
+