contract2.cpp

class Foobar
{
public:
	Foobar(float val) { myVal = val;  }

	float func1(float x)
	{
		REQUIRES(x > 0);
		return sqrt(myVal + x);
	}

	float func2(float x)
	{
		REQUIRES(x != myVal);
		ENSURES(x > 0);
		return myVal + x;
	}
private:
	BEGIN_INVARIANT(Foobar)
	INVARIANT(self.myVal > 0)
	END_INVARIANT()

	float myVal;
};