OverFlowException的Contract.Ensures

Question

我有一个简单的方法，可以返回给定数字的指数值：

    public int Exp(int num)
    {
        return Convert.ToInt32(System.Math.Exp(num));
    }

运行Pex时，对于某个较大的数字: 1969057606，我在Summary/Exception字段中得到一个OverFlowException。

如何使用Contract.Ensure()创建Post条件？我尝试了以下操作，但没有任何效果：

Contract.Ensures(Contract.Result<int>() < 2147483647);

// This is because the max value an int variable can hold is 2147483647

Answer 1

Contract.Ensures用于在函数运行后断言类的状态，或者，在本例中，断言函数的结果，而不管输入是什么。您需要添加一个Contract.Requires，以便e^num <= int.MaxValue，例如

Contract.Requires<ArgumentOutOfRangeException>(num <= Math.Floor(Math.Log(int.MaxValue)))

尽管您可能希望将最大值计算结果提取为一个常量。

public static readonly int MAX_EXPONENT = Math.Floor(Math.Log(int.MaxValue));
...
Contract.Requires<ArgumentOutOfRangeException>(num <= MAX_EXPONENT)