text: 
  // 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
  
  #include "no_lambdas.hpp"
  #include <boost/bind.hpp>
  #include <cassert>
  
  //[no_lambdas_cpp
  iarray::iarray(unsigned max, unsigned count) :
      boost::contract::constructor_precondition<iarray>(boost::bind(
              &iarray::constructor_precondition, max, count)),
      values_(new int[max]), // Member initializations can be here.
      capacity_(max)
  {
      boost::contract::old_ptr<int> old_instances;
      boost::contract::check c = boost::contract::constructor(this)
          .old(boost::bind(&iarray::constructor_old, boost::ref(old_instances)))
          .postcondition(boost::bind(
              &iarray::constructor_postcondition,
              this,
              boost::cref(max),
              boost::cref(count),
              boost::cref(old_instances)
          ))
      ;
  
      for(unsigned i = 0; i < count; ++i) values_[i] = int();
      size_ = count;
      ++instances_;
  }
  
  iarray::~iarray() {
      boost::contract::old_ptr<int> old_instances;
      boost::contract::check c = boost::contract::destructor(this)
          .old(boost::bind(&iarray::destructor_old, this,
                  boost::ref(old_instances)))
          .postcondition(boost::bind(&iarray::destructor_postcondition,
                  boost::cref(old_instances)))
      ;
      
      delete[] values_;
      --instances_;
  }
  
  void iarray::push_back(int value, boost::contract::virtual_* v) {
      boost::contract::old_ptr<unsigned> old_size;
      boost::contract::check c = boost::contract::public_function(v, this)
          .precondition(boost::bind(&iarray::push_back_precondition, this))
          .old(boost::bind(&iarray::push_back_old, this, boost::cref(v),
                  boost::ref(old_size)))
          .postcondition(boost::bind(&iarray::push_back_postcondition, this,
                  boost::cref(old_size)))
      ;
  
      values_[size_++] = value;
  }
  
  unsigned iarray::capacity() const {
      // Check invariants.
      boost::contract::check c = boost::contract::public_function(this);
      return capacity_;
  }
  
  unsigned iarray::size() const {
      // Check invariants.
      boost::contract::check c = boost::contract::public_function(this);
      return size_;
  }
  
  int iarray::instances() {
      // Check static invariants.
      boost::contract::check c = boost::contract::public_function<iarray>();
      return instances_;
  }
  
  int iarray::instances_ = 0;
  //]
  
  int main() {
      iarray a(3, 2);
      assert(a.capacity() == 3);
      assert(a.size() == 2);
      
      a.push_back(-123);
      assert(a.size() == 3);
  
      return 0;
  }
  
  