• Home
  • Line#
  • Scopes#
  • Navigate#
  • Raw
  • Download
1  
2  // Copyright (C) 2008-2018 Lorenzo Caminiti
3  // Distributed under the Boost Software License, Version 1.0 (see accompanying
4  // file LICENSE_1_0.txt or a copy at http://www.boost.org/LICENSE_1_0.txt).
5  // See: http://www.boost.org/doc/libs/release/libs/contract/doc/html/index.html
6  
7  //[meyer97_stack3
8  // File: stack3.cpp
9  #include "stack4.hpp"
10  #include <boost/contract.hpp>
11  #include <boost/optional.hpp>
12  #include <cassert>
13  
14  // Dispenser LIFO with max capacity using error codes.
15  template<typename T>
16  class stack3 {
17      friend class boost::contract::access;
18  
invariant() const19      void invariant() const {
20          if(!error()) {
21              BOOST_CONTRACT_ASSERT(count() >= 0); // Count non-negative.
22              BOOST_CONTRACT_ASSERT(count() <= capacity()); // Count bounded.
23              // Empty if no element.
24              BOOST_CONTRACT_ASSERT(empty() == (count() == 0));
25          }
26      }
27  
28  public:
29      enum error_code {
30          no_error = 0,
31          overflow_error,
32          underflow_error,
33          size_error
34      };
35  
36      /* Initialization */
37  
38      // Create stack for max of n elems, if n < 0 set error (no preconditions).
stack3(int n,T const & default_value=T ())39      explicit stack3(int n, T const& default_value = T()) :
40              stack_(0), error_(no_error) {
41          boost::contract::check c = boost::contract::constructor(this)
42              .postcondition([&] {
43                  // Error if impossible.
44                  BOOST_CONTRACT_ASSERT((n < 0) == (error() == size_error));
45                  // No error if possible.
46                  BOOST_CONTRACT_ASSERT((n >= 0) == !error());
47                  // Created if no error.
48                  if(!error()) BOOST_CONTRACT_ASSERT(capacity() == n);
49              })
50          ;
51  
52          if(n >= 0) stack_ = stack4<T>(n);
53          else error_ = size_error;
54      }
55  
56      /* Access */
57  
58      // Max number of stack elements.
capacity() const59      int capacity() const {
60          // Check invariants.
61          boost::contract::check c = boost::contract::public_function(this);
62          return stack_.capacity();
63      }
64  
65      // Number of stack elements.
count() const66      int count() const {
67          // Check invariants.
68          boost::contract::check c = boost::contract::public_function(this);
69          return stack_.count();
70      }
71  
72      // Top element if present, otherwise none and set error (no preconditions).
item() const73      boost::optional<T const&> item() const {
74          boost::contract::check c = boost::contract::public_function(this)
75              .postcondition([&] {
76                  // Error if impossible.
77                  BOOST_CONTRACT_ASSERT(empty() == (error() == underflow_error));
78                  // No error if possible.
79                  BOOST_CONTRACT_ASSERT(!empty() == !error());
80              })
81          ;
82  
83          if(!empty()) {
84              error_ = no_error;
85              return boost::optional<T const&>(stack_.item());
86          } else {
87              error_ = underflow_error;
88              return boost::optional<T const&>();
89          }
90      }
91  
92      /* Status Report */
93  
94      // Error indicator set by various operations.
error() const95      error_code error() const {
96          // Check invariants.
97          boost::contract::check c = boost::contract::public_function(this);
98          return error_;
99      }
100  
empty() const101      bool empty() const {
102          // Check invariants.
103          boost::contract::check c = boost::contract::public_function(this);
104          return stack_.empty();
105      }
106  
full() const107      bool full() const {
108          // Check invariants.
109          boost::contract::check c = boost::contract::public_function(this);
110          return stack_.full();
111      }
112  
113      /* Element Change */
114  
115      // Add x to top if capacity allows, otherwise set error (no preconditions).
put(T const & x)116      void put(T const& x) {
117          boost::contract::old_ptr<bool> old_full = BOOST_CONTRACT_OLDOF(full());
118          boost::contract::old_ptr<int> old_count = BOOST_CONTRACT_OLDOF(count());
119          boost::contract::check c = boost::contract::public_function(this)
120              .postcondition([&] {
121                  // Error if impossible.
122                  BOOST_CONTRACT_ASSERT(*old_full == (error() == overflow_error));
123                  // No error if possible.
124                  BOOST_CONTRACT_ASSERT(!*old_full == !error());
125                  if(!error()) { // If no error...
126                      BOOST_CONTRACT_ASSERT(!empty()); // ...not empty.
127                      BOOST_CONTRACT_ASSERT(*item() == x); // ...added to top.
128                      // ...one more.
129                      BOOST_CONTRACT_ASSERT(count() == *old_count + 1);
130                  }
131              })
132          ;
133  
134          if(full()) error_ = overflow_error;
135          else {
136              stack_.put(x);
137              error_ = no_error;
138          }
139      }
140  
141      // Remove top element if possible, otherwise set error (no preconditions).
remove()142      void remove() {
143          boost::contract::old_ptr<bool> old_empty =
144                  BOOST_CONTRACT_OLDOF(empty());
145          boost::contract::old_ptr<int> old_count = BOOST_CONTRACT_OLDOF(count());
146          boost::contract::check c = boost::contract::public_function(this)
147              .postcondition([&] {
148                  // Error if impossible.
149                  BOOST_CONTRACT_ASSERT(*old_empty == (error() ==
150                          underflow_error));
151                  // No error if possible.
152                  BOOST_CONTRACT_ASSERT(!*old_empty == !error());
153                  if(!error()) { // If no error...
154                      BOOST_CONTRACT_ASSERT(!full()); // ...not full.
155                      // ...one less.
156                      BOOST_CONTRACT_ASSERT(count() == *old_count - 1);
157                  }
158              })
159          ;
160  
161          if(empty()) error_ = underflow_error;
162          else {
163              stack_.remove();
164              error_ = no_error;
165          }
166      }
167  
168  private:
169      stack4<T> stack_;
170      mutable error_code error_;
171  };
172  
main()173  int main() {
174      stack3<int> s(3);
175      assert(s.capacity() == 3);
176      assert(s.count() == 0);
177      assert(s.empty());
178      assert(!s.full());
179  
180      s.put(123);
181      assert(!s.empty());
182      assert(!s.full());
183      assert(*s.item() == 123);
184  
185      s.remove();
186      assert(s.empty());
187      assert(!s.full());
188  
189      return 0;
190  }
191  //]
192  
193