1

我正在研究一个将位图封装为像素数组的对象。该数组是一维的，我将图像的宽度存储在只读字段中。我还添加了一个基于像素数组长度和宽度计算高度的属性。我有以下关于高度的不变量：

  • 像素数组（Data 属性，使用私有数据字段）不为空，并且至少有一个元素。
  • 宽度大于零

高度属性的代码：

public int Height
{
    [Pure]
    get
    {
        Contract.Requires(Data != null);
        Contract.Requires(Width > 0);
        Contract.Requires(Data.Length > 0);

        Contract.Ensures(Contract.Result<int>() > 0);
        Contract.EndContractBlock();
        Contract.Assume(Data.Length > Width);

        return Data.Length / Width;
    }
}

但我无法让静态检查器证明这一点。问题可能是（据我了解），没有要求Data.Length % Width == 0，所以因为整数除法Data.Length / Width可能为零；因此我添加了没有运气的假设。我不确定如何提示静态检查器接受我的保证。

4

1 回答 1

1

我写了一个简单的小测试，似乎通过了

测试对象类：

public class Class1
{
    public int Width { get; set; }
    public byte[] Data { get; set; }

    public int Height
    {
        [Pure]
        get
        {
            Contract.Requires(Data != null);
            Contract.Requires(Width > 0);
            Contract.Requires(Data.Length > 0);

            Contract.Ensures(Contract.Result<int>() > 1);
            //Contract.Assume(Data.Length > Width);

            return Data.Length / Width;
        }
    }
}

单元测试：

[TestFixture]
public class Tests
{
    [Test]
    public void Class1_ContractEnsures_IsEnforced()
    {
        var item = new Class1 { Width = 1, Data = new byte[1] };
        var h = item.Height;
    }
}

请注意，如果我重新启用Assume约束，那么这将首先触发（并失败），因此Ensures不会被测试。包含单元测试以创建对Height. 没有这个，代码合同似乎检测到Height没有使用，因此不会应用确保约束。此外，我收到的错误消息CodeContracts: requires is false可能有点误导。

如果有帮助，我正在使用Code Contracts 1.4.50327.0？

于 2012-12-24T01:16:31.433 回答