The Artima Developer Community
Articles | News | Weblogs | Books | Forums
Artima Forums | Articles | Weblogs | Java Answers | News
Sponsored Link •

Weblogs Forum
A Real-World Example of a C++ Contract Verification Class

1 reply on 1 page. Most recent reply: May 29, 2005 7:23 AM by Harrison Ainsworth

Welcome Guest
  Sign In

Go back to the topic listing  Back to Topic List Click to reply to this topic  Reply to this Topic Click to search messages in this forum  Search Forum Click for a threaded view of the topic  Threaded View   
Previous Topic   Next Topic
Flat View: This topic has 1 reply on 1 page
Christopher Diggins

Posts: 1215
Nickname: cdiggins
Registered: Feb, 2004

A Real-World Example of a C++ Contract Verification Class (View in Weblogs)
 		Posted: May 23, 2005 9:58 PM
Reply to this message Reply
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.
Advertisement
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.


Harrison Ainsworth

Posts: 57
Nickname: hxa7241
Registered: Apr, 2005

Re: A Real-World Example of a C++ Contract Verification Class Posted: May 29, 2005 7:23 AM
Reply to this message Reply
It looks as if it needs language support... or some code generation...

Another possible idea: to execute the invariant checks, an object is constructed and destructed at function end points. Could this be arranged with a by-value argument to the function -- and make it a default parameter, that would be tidier...?

Flat View: This topic has 1 reply on 1 page
Topic: Kelly Doesn't Care About Hash Tables Previous Topic   Next Topic Topic: Project Atom, Amazon, Mobile Web Services, and Fireflies at REST
Sponsored Links


Google
  Web Artima.com   

Copyright © 1996-2019 Artima, Inc. All Rights Reserved. - Privacy Policy - Terms of Use