4

私は次のインターフェースを持っています：

[ContractClass(typeof(MyObjectContract))]
public interface IMyObject
{
    int CountOfItems { get; }
}

次の契約:

[ContractClassFor(typeof(IMyObject))]
public abstract class MyObjectContract
{
    int IMyObject.CountOfItems
    {
        get
        {
            Contract.Ensures(Contract.Result<int>() > 0);
            return 1;
        }
    }
}

次の実装:

public class MyObject : IMyObject
{
    private IEnumerable someEnumerable .... 

    public int CountOfItems
    {
        get
        {
            return this.someEnumerable.Count();
        }
    }
}

今、私は警告を受けていますensures unproven: Contract.Result<int>() > 0

count が 0 より大きいことをどのように証明すればよいですか? ゲッターで例外をスローしたくないのですが、何が欠けていますか?

ありがとう

4

4 に答える 4

2

IEnumerable<T>.Count()他の人が述べたように、基本クラス ライブラリ (.NET Framework) と静的チェッカーの制限により、0 より大きい値を返すことを静的に証明することはできません。ただし、その事実が真であると仮定することを静的チェッカーに示すことができます。これは、基本クラス ライブラリ、または静的チェッカーが証明できないステートメントを使用して、そのようなすべてのコントラクトの問題を解決する方法です。

public int CountOfItems
{
    get
    {
        int count = this.someEnumerable.Count();
        Contract.Assume(count > 0);
        return count;
    }
}
于 2012-08-06T21:26:48.130 に答える
0

実装にメソッドを追加するContractInvariantと、警告が解決されるようです。

于 2012-08-08T12:39:20.363 に答える
0

これを静的に証明することはできないと思います。
Enumerable.Count<TSource>拡張メソッドは、その戻り値に関する契約を定義していません (たとえば、このメソッドは無限シーケンスに対して何を返す必要がありますか?)。

そのため、CC stais チェッカーはこれについて警告します。

于 2012-08-03T12:04:29.220 に答える
0

あなたのコードが正しいとしましょう。それは機能し、コード コントラクト システムにその事実を認識させようとしているだけです。

これはCountOfItems、 のインスタンスを呼び出すと、MyObject常に 0 より大きい値が返されることを意味します。例外をスローせず、ゼロ以下の値を返しません。

これは、someEnumerableが何らかのオブジェクトに割り当てられ someEnumerable.Count()、どのオブジェクトが参照されても常に 0 より大きい値を返すことを意味します。これらの事実は常に true になります (いつCountOfItems呼び出されるかについて制限がないためです。

これは、MyObjectそれらの事実を含むオブジェクトの不変条件 (コードで明示的に綴られているかどうかにかかわらず) があることを意味します。そして、あなたのコードは（仮定により）正しいので、割り当てられMyObjectた保証の実装someEnumerableとそのカウントは常にゼロより大きくなります。

したがって、 のコントラクトを満たすためにCountOfItems、コントラクト システムは、これらの不変条件と、それらがどのように保証されるかを認識する必要があります。

于 2012-08-03T16:23:08.127 に答える