• 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 #include <boost/contract.hpp>
8 #include <cassert>
9 
10 //[static_public
11 template<class C>
12 class make {
13 public:
static_invariant()14     static void static_invariant() { // Static class invariants.
15         BOOST_CONTRACT_ASSERT(instances() >= 0);
16     }
17 
18     // Contract for a static public function.
instances()19     static int instances() {
20         // Explicit template parameter `make` (check static invariants).
21         boost::contract::check c = boost::contract::public_function<make>();
22 
23         return instances_; // Function body.
24     }
25 
26     /* ... */
27 //]
28 
make()29     make() : object() {
30         boost::contract::old_ptr<int> old_instances =
31                 BOOST_CONTRACT_OLDOF(instances());
32         boost::contract::check c = boost::contract::constructor(this)
33             .postcondition([&] {
34                 BOOST_CONTRACT_ASSERT(instances() == *old_instances + 1);
35             })
36         ;
37 
38         ++instances_;
39     }
40 
~make()41     ~make() {
42         boost::contract::old_ptr<int> old_instances =
43                 BOOST_CONTRACT_OLDOF(instances());
44         boost::contract::check c = boost::contract::destructor(this)
45             .postcondition([&] { // (An example of destructor postconditions.)
46                 BOOST_CONTRACT_ASSERT(instances() == *old_instances - 1);
47             })
48         ;
49 
50         --instances_;
51     }
52 
53     C object;
54 
55 private:
56     static int instances_;
57 };
58 
59 template<class C>
60 int make<C>::instances_ = 0;
61 
main()62 int main() {
63     struct x {};
64     make<x> x1, x2, x3;
65     assert(make<x>::instances() == 3);
66 
67     return 0;
68 }
69 
70