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

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

 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 24, 2005 12:58 AM
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.

 Harrison Ainsworth Posts: 57 Nickname: hxa7241 Registered: Apr, 2005
Re: A Real-World Example of a C++ Contract Verification Class Posted: May 29, 2005 10:23 AM
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
 Previous Topic Next Topic