Heron-Centric: Ruminations of a Language Designer
A Real-World Example of a C++ Contract Verification Class
by Christopher Diggins
May 24, 2005

Summary
I have been talking a lot about methods for contract verification lately, so I decided to share a real-world example involving an arbitrary precision integer.

I have talked a fair amount on my blog and in articles about contract verification classes but I haven't really put my money where my mouth is until now.

My latest project is an arbitrary precision integer called big_int, which holds unsigned integer values as big as memory allows. Not much new here, except that this is public domain code.

Here is how big_int is defined:

  #ifdef NDEBUG 
    typedef big_int_impl big_int;
  #else
    typedef big_int_contract<big_int_impl> big_int;
  #endif

and here is the big_int_contract class:

#ifndef BIG_INT_CONTRACT_HPP
#define BIG_INT_CONTRACT_HPP

#include <cassert>
#include <stdexcept>

template<typename T>
struct invariant_checker
{
  invariant_checker(const T* x) : m(x) {
    if (!m->invariant()) {
      std::logic_error("invariant failure on entry");
    }
  }
  ~invariant_checker() {
    if (!m->invariant()) {
      std::logic_error("invariant failure on exit");
    }
  }
  const T* m;
};

#define INVARIANT_ASSERT invariant_checker<self> invariant_checker__(this);
#define PRE_ASSERT(TKN) assert("precondition " && TKN);
#define POST_ASSERT(TKN) assert("postcondition " && TKN);

namespace cdiggins
{
  template<typename Impl_T>
  class big_int_contract : public Impl_T
  {
    typedef Impl_T impl;
    typedef big_int_contract self;
  public:
    self() {
    }
    self(const std::vector<bool>& x) : impl(x) {
      INVARIANT_ASSERT;
    }
    self(int x) : impl(x) {
      INVARIANT_ASSERT;
    }
    self(const impl& x) {
      impl::operator=(x);
    }
    self& operator=(const self& x) {
      INVARIANT_ASSERT;
      impl::operator=(x);
      POST_ASSERT(*this == x);
      return *this;
    }
    self& operator<<=(int n) {
      INVARIANT_ASSERT;
      self old = *this;
      impl::operator<<=(n);
      POST_ASSERT(*this >= old);
      return *this;
    }
    self& operator>>=(int n) {
      INVARIANT_ASSERT;
      self old = *this;
      impl::operator>>=(n);
      POST_ASSERT(*this <= old);
      return *this;
    }
    self operator++(int ignored) {
      INVARIANT_ASSERT;
      self old = *this;
      self ret = impl::operator++(ignored);
      POST_ASSERT(*this == old + 1);
      return ret;
    }
    self operator--(int ignored) {
      INVARIANT_ASSERT;
      PRE_ASSERT(*this > 0);
      self old = *this;
      self ret = impl::operator--(ignored);
      POST_ASSERT(*this == old - 1);
      return ret;
    }
    self& operator++() {
      INVARIANT_ASSERT;
      self old = *this;
      impl::operator++();
      POST_ASSERT(*this == old + 1);
      return *this;
    }
    self& operator--() {
      INVARIANT_ASSERT;
      PRE_ASSERT(*this > 0);
      self old = *this;
      impl::operator--();
      POST_ASSERT(*this == old - 1);
      return *this;
    }
    self& operator+=(const self& x) {
      INVARIANT_ASSERT;
      self old = *this;
      impl::operator+=(x);
      POST_ASSERT(*this >= old);
      POST_ASSERT(*this >= x);
      // TEMP:
      // POST_ASSERT(impl(*this) - impl(x) == impl(old));
      return *this;
    }
    self& operator-=(const self& x) {
      INVARIANT_ASSERT;
      PRE_ASSERT(*this >= x);
      self old = *this;
      impl::operator-=(x);
      POST_ASSERT(*this <= old);
      POST_ASSERT(impl(*this) + impl(x) == impl(old));
      return *this;
    }
    self& operator*=(const self& x) {
      INVARIANT_ASSERT;
      self old = *this;
      impl::operator*=(x);
      if (x > 0) {
        POST_ASSERT(impl(*this) / impl(x) == impl(old));
      }
      if (old > 0) {
        POST_ASSERT(impl(*this) / impl(old) == impl(x));
      }
      return *this;
    }
    self& operator/=(const self& x) {
      INVARIANT_ASSERT;
      PRE_ASSERT(x > 0);
      self old = *this;
      impl::operator/=(x);
      POST_ASSERT((impl(*this) * impl(x)) + (impl(old) % impl(x)) == impl(old));
      return *this;
    }
    self& operator%=(const self& x) {
      INVARIANT_ASSERT;
      PRE_ASSERT(x > 0);
      PRE_ASSERT(x != 0);
      PRE_ASSERT(impl(x) != 0);
      self old = *this;
      impl::operator%=(x);
      PRE_ASSERT(x > 0);
      PRE_ASSERT(x != 0);
      PRE_ASSERT(impl(x) != 0);
      POST_ASSERT(((impl(old) / impl(x)) * impl(x)) + impl(*this) == impl(old));
      return *this;
    }
    self operator~() const {
      INVARIANT_ASSERT;
      self ret = impl::operator~();
      for (int i=0; i < size(); i++) {
        POST_ASSERT(ret[i] != operator[](i));
      }
      return ret;
    }
    self& operator&=(const self& x) {
      INVARIANT_ASSERT;
      self old = *this;
      impl::operator&=(x);
      for (int i=0; i < size(); i++) {
        POST_ASSERT(operator[](i) == (x[i] && old[i]));
      }
      return *this;
    }
    self& operator|=(const self& x) {
      INVARIANT_ASSERT;
      self old = *this;
      impl::operator|=(x);
      for (int i=0; i < size(); i++) {
        POST_ASSERT(operator[](i) == (x[i] || old[i]));
      }
      return *this;
    }
    self& operator^=(const self& x) {
      INVARIANT_ASSERT;
      self old = *this;
      impl::operator^=(x);
      for (int i=0; i < size(); i++) {
        POST_ASSERT(operator[](i) == logical_xor(x[i], old[i]));
      }
      return *this;
    }
    bool operator[](int n) const {
      INVARIANT_ASSERT;
      return impl::operator[](n);
    }
    int size() const {
      INVARIANT_ASSERT;
      return impl::size();
    }
    // friend functions
    friend self operator<<(const self& x, unsigned int n) {
      invariant_checker<self> ic1(&x);
      self ret = impl(x) << n;
      POST_ASSERT(ret == (self(x) <<= n));
      return ret;
    }
    friend self operator>>(const self& x, unsigned int n) {
      invariant_checker<self> ic1(&x);
      self ret = impl(x) >> n;
      POST_ASSERT(ret == (self(x) >>= n));
      return ret;
    }
    friend self operator+(const self& x, const self& y) {
      invariant_checker<self> ic1(&x);
      invariant_checker<self> ic2(&y);
      self ret = impl(x) + impl(y);
      POST_ASSERT(ret == (self(x) += y));
      return ret;
    }
    friend self operator-(const self& x, const self& y) {
      invariant_checker<self> ic1(&x);
      invariant_checker<self> ic2(&y);
      PRE_ASSERT(x >= y);
      self ret = impl(x) - impl(y);
      POST_ASSERT(ret == (self(x) -= y));
      return ret;
    }
    friend self operator*(const self& x, const self& y) {
      invariant_checker<self> ic1(&x);
      invariant_checker<self> ic2(&y);
      self ret = impl(x) * impl(y);
      POST_ASSERT(ret == (self(x) *= y));
      return ret;
    }
    friend self operator/(const self& x, const self& y) {
      invariant_checker<self> ic1(&x);
      invariant_checker<self> ic2(&y);
      PRE_ASSERT(y != 0);
      self ret = impl(x) / impl(y);
      POST_ASSERT(ret == (self(x) /= y));
      return ret;
    }
    friend self operator%(const self& x, const self& y) {
      invariant_checker<self> ic1(&x);
      invariant_checker<self> ic2(&y);
      PRE_ASSERT(y != 0);
      self ret = impl(x) % impl(y);
      POST_ASSERT(ret == (self(x) %= y));
      return ret;
    }
    friend self operator^(const self& x, const self& y) {
      invariant_checker<self> ic1(&x);
      invariant_checker<self> ic2(&y);
      PRE_ASSERT(y != 0);
      self ret = impl(x) ^ impl(y);
      POST_ASSERT(ret == (self(x) ^= y));
      return ret;
    }
    friend self operator|(const self& x, const self& y) {
      invariant_checker<self> ic1(&x);
      invariant_checker<self> ic2(&y);
      PRE_ASSERT(y != 0);
      self ret = impl(x) | impl(y);
      POST_ASSERT(ret == (self(x) |= y));
      return ret;
    }
    friend self operator&(const self& x, const self& y) {
      invariant_checker<self> ic1(&x);
      invariant_checker<self> ic2(&y);
      PRE_ASSERT(y != 0);
      self ret = impl(x) & impl(y);
      POST_ASSERT(ret == (self(x) &= y));
      return ret;
    }
    // comparison operators
    friend bool operator==(const self& x, const self& y) {
      invariant_checker<self> ic1(&x);
      invariant_checker<self> ic2(&y);
      bool ret = (impl(x) == impl(y));
      POST_ASSERT(ret != (impl(x) != impl(y)));
      return ret;
    }
    friend bool operator!=(const self& x, const self& y) {
      invariant_checker<self> ic1(&x);
      invariant_checker<self> ic2(&y);
      bool ret = (impl(x) != impl(y));
      POST_ASSERT(ret != (impl(x) == impl(y)));
      return ret;
    }
    friend bool operator>(const self& x, const self& y) {
      invariant_checker<self> ic1(&x);
      invariant_checker<self> ic2(&y);
      bool ret = (impl(x) > impl(y));
      POST_ASSERT(ret != (impl(x) <= impl(y)));
      return ret;
    }
    friend bool operator<(const self& x, const self& y) {
      invariant_checker<self> ic1(&x);
      invariant_checker<self> ic2(&y);
      bool ret = (impl(x) < impl(y));
      POST_ASSERT(ret != (impl(x) >= impl(y)));
      return ret;
    }
    friend bool operator>=(const self& x, const self& y) {
      invariant_checker<self> ic1(&x);
      invariant_checker<self> ic2(&y);
      bool ret = (impl(x) >= impl(y));
      POST_ASSERT(ret != (impl(x) < impl(y)));
      return ret;
    }
    friend bool operator<=(const self& x, const self& y) {
      invariant_checker<self> ic1(&x);
      invariant_checker<self> ic2(&y);
      bool ret = (impl(x) <= impl(y));
      POST_ASSERT(ret != (impl(x) > impl(y)));
      return ret;
    }
  public:
    bool invariant() const {
      // the leading bit should always be one
      if (impl::size() == 0) return true;
      return impl::operator[](impl::size() - 1);
    }
  private:
    operator impl() {
      return *this;
    }
  };
}

#endif

It is in fact bigger than my implementation class. Notice that because this uses templates, it can be used on almost any big_int implementation.

Talk Back!

Have an opinion? Readers have already posted 1 comment about this weblog entry. Why not add yours?

RSS Feed

If you'd like to be notified whenever Christopher Diggins adds a new entry to his weblog, subscribe to his RSS feed.

Digg |

del.icio.us |

About the Blogger

Christopher Diggins is a software developer and freelance writer. Christopher loves programming, but is eternally frustrated by the shortcomings of modern programming languages. As would any reasonable person in his shoes, he decided to quit his day job to write his own ( www.heron-language.com ). Christopher is the co-author of the C++ Cookbook from O'Reilly. Christopher can be reached through his home page at www.cdiggins.com.


	Web Artima.com