class - 一个 OverFlowException 的 Contract.Ensures

Question

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

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

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

如何使用创建后置条件Contract.Ensure()？我尝试了以下但它没有做任何事情：

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

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

score 0 · Accepted Answer

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)

1 回答 1