1

ビットマップをピクセルの配列としてカプセル化するオブジェクトに取り組んでいます。配列は 1 次元で、画像の幅を読み取り専用フィールドに格納します。また、ピクセル配列の長さと幅に基づいて高さを計算するプロパティも追加しました。高さに関して次の不変条件があります。

  • ピクセル配列 (プライベート データ フィールドを使用する Data プロパティ) が null ではなく、少なくとも 1 つの要素を持っています。
  • 幅がゼロより大きい

高さプロパティのコード:

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が使用されていないことを検出したように見えたため、ensure 制約が適用されませんでした。また、私が受け取ったエラーメッセージはCodeContracts: requires is false、少し誤解を招く可能性があるものでした.

Code Contracts 1.4.50327.0それが役立つ場合、私は使用していますか？

于 2012-12-24T01:16:31.433 に答える