1 files changed, 138 insertions, 0 deletions
diff --git a/src/boost/libs/contract/example/mitchell02/stack.cpp b/src/boost/libs/contract/example/mitchell02/stack.cpp
new file mode 100644
index 000000000..a0bd6b144
--- /dev/null
+++ b/src/boost/libs/contract/example/mitchell02/stack.cpp
@@ -0,0 +1,138 @@
+
+// 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
+
+//[mitchell02_stack
+#include <boost/contract.hpp>
+#include <boost/optional.hpp>
+#include <vector>
+#include <cassert>
+
+template<typename T>
+class stack {
+    friend class boost::contract::access;
+
+    void invariant() const {
+        BOOST_CONTRACT_ASSERT(count() >= 0); // Non-negative count.
+    }
+
+public:
+    /* Creation */
+
+    // Create empty stack.
+    stack() {
+        boost::contract::check c = boost::contract::constructor(this)
+            .postcondition([&] {
+                BOOST_CONTRACT_ASSERT(count() == 0); // Empty.
+            })
+        ;
+    }
+
+    // Destroy stack.
+    virtual ~stack() {
+        // Check invariants.
+        boost::contract::check c = boost::contract::destructor(this);
+    }
+
+    /* Basic Queries */
+
+    // Number of items.
+    int count() const {
+        // Check invariants.
+        boost::contract::check c = boost::contract::public_function(this);
+        return items_.size();
+    }
+
+    // Item at index in [1, count()] (as in Eiffel).
+    T const& item_at(int index) const {
+        boost::contract::check c = boost::contract::public_function(this)
+            .precondition([&] {
+                BOOST_CONTRACT_ASSERT(index > 0); // Positive index.
+                BOOST_CONTRACT_ASSERT(index <= count()); // Index within count.
+            })
+        ;
+
+        return items_[index - 1];
+    }
+
+    /* Derived Queries */
+
+    // If no items.
+    bool is_empty() const {
+        bool result;
+        boost::contract::check c = boost::contract::public_function(this)
+            .postcondition([&] {
+                // Consistent with count.
+                BOOST_CONTRACT_ASSERT(result == (count() == 0));
+            })
+        ;
+
+        return result = (count() == 0);
+    }
+
+    // Top item.
+    T const& item() const {
+        boost::optional<T const&> result; // Avoid extra construction of T.
+        boost::contract::check c = boost::contract::public_function(this)
+            .precondition([&] {
+                BOOST_CONTRACT_ASSERT(count() > 0); // Not empty.
+            })
+            .postcondition([&] {
+                // Item on top.
+                BOOST_CONTRACT_ASSERT(*result == item_at(count()));
+            })
+        ;
+
+        return *(result = item_at(count()));
+    }
+
+    /* Commands */
+
+    // Push item to the top.
+    void put(T const& new_item) {
+        boost::contract::old_ptr<int> old_count = BOOST_CONTRACT_OLDOF(count());
+        boost::contract::check c = boost::contract::public_function(this)
+            .postcondition([&] {
+                BOOST_CONTRACT_ASSERT(count() == *old_count + 1); // Count inc.
+                BOOST_CONTRACT_ASSERT(item() == new_item); // Item set.
+            })
+        ;
+
+        items_.push_back(new_item);
+    }
+
+    // Pop top item.
+    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(count() > 0); // Not empty.
+            })
+            .postcondition([&] {
+                BOOST_CONTRACT_ASSERT(count() == *old_count - 1); // Count dec.
+            })
+        ;
+
+        items_.pop_back();
+    }
+
+private:
+    std::vector<T> items_;
+};
+
+int main() {
+    stack<int> s;
+    assert(s.count() == 0);
+
+    s.put(123);
+    assert(s.item() == 123);
+
+    s.remove();
+    assert(s.is_empty());
+
+    return 0;
+}
+//]
+