First draft of C++ library contract_light published

Oct 212014

I am happy to announce that I published a C++ library that offers a lightweight version of a Design by Contract functionality. You can find it under http://github.com/FelixPetriconi/contract_light.

Here is a simple example for the beginning. More to come later


class Rect 
{
  // Use this define if an invariant is defined. If no invariant is defined
  // no need to do it
  CONTRACTOR
  int w_;
  int h_;
public:
  Rect() : w_(0), h_(0) {}
  
  ~Rect() {
    // checking that the invariants are fulfilled, even before destruction
    INVARIANT;
  }
  
  void setWidth(int newW) {
    // setting the pre condition of this method; the invariant is checked 
    // once at the end of the scope
    PRECONDITION [&] { return newW >= 0; };
    // setting the post condition; the invariant is checked only once after 
    // leaving the scope, regardless of the number of pre- and/or post-conditions
    POSTCONDITION [&, this] { return newW == w_; };
    w_ = newW;
    
    // There is no need to define here INVARIANT here. This is done automatically
    // whenever there is a bool invariant() const method is defined
  }
  
  int size() const {
    int result;
    POSTCONDITION [&] { return result == w_ * h_; }
    result = w_ * h_;
    
    return result;
  }
  
  bool invariant() const {
    return w_ >= 0 && h_ >= 0;
  }
};

class Rect

{

// Use this define if an invariant is defined. If no invariant is defined

// no need to do it

CONTRACTOR

int w_;

int h_;

public:

Rect() : w_(0), h_(0) {}

~Rect() {

// checking that the invariants are fulfilled, even before destruction

INVARIANT;

}

void setWidth(int newW) {

// setting the pre condition of this method; the invariant is checked

// once at the end of the scope

PRECONDITION [&] { return newW >= 0; };

// setting the post condition; the invariant is checked only once after

// leaving the scope, regardless of the number of pre- and/or post-conditions

POSTCONDITION [&, this] { return newW == w_; };

w_ = newW;

// There is no need to define here INVARIANT here. This is done automatically

// whenever there is a bool invariant() const method is defined

}

int size() const {

int result;

POSTCONDITION [&] { return result == w_ * h_; }

result = w_ * h_;

return result;

}

bool invariant() const {

return w_ >= 0 && h_ >= 0;

}

};

Sorry, the comment form is closed at this time.