CodeContracts: How to fulfill Require in Ctor using this() call?
-
19-09-2019 - |
Question
I'm playing around with Microsoft's CodeContracts and encountered a problem I was unable to solve. I've got a class with two constructors:
public Foo (public float f) {
Contracts.Require(f > 0);
}
public Foo (int i)
: this ((float)i)
{}
The example is simplified. I don't know how to check the second constructor's f
for being > 0. Is this even possible with Contracts?
Solution
You can just add the precondition to the second constructor's body.
public TestClass(float f)
{
Contract.Requires(f > 0);
throw new Exception("foo");
}
public TestClass(int i): this((float)i)
{
Contract.Requires(i > 0);
}
EDIT
Try calling the code above with:
TestClass test2 = new TestClass((int)-1);
You will see that the precondition is thrown before the regular Exception is thrown.
OTHER TIPS
I would add a static Method that converts the int to the float and include the Contract.Requires
in there.
class Foo
{
public Foo(float f)
{
Contract.Requires(f > 0);
}
public Foo(int i) : this(ToFloat(i))
{
}
private static float ToFloat(int i)
{
Contract.Requires(i > 0);
return i;
}
}
Hope this helps.
Licensed under: CC-BY-SA with attribution
Not affiliated with StackOverflow