CodeContracts: How to fullfill Require in Ctor using this() call?

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?

Answer 1

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.

Answer 2

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.