3

私はこれを次のテストケースに要約することができましたが、これがC＃コードコントラクトの静的チェッカーの制限なのか、それとも私が見逃しているものなのか疑問に思っています。あるスタイルのコードを使用してコントラクトを証明しようとすると、不変の証明されていない警告がスローされますが、それでも（私が思うに）それを証明する同等の方法は問題なく機能します。

当初、これはPureプロパティを持つオブジェクトを使用していなかったため（したがって、コードコントラクトはプロパティが決定論的であるかどうかを評価できなかったため）、オブジェクトの周りにPureラッパーを作成したためだと思いました（Nullable <Int64>になる可能性があります）助けにはならなかった。

最初のテストケースと3番目のテストケースに違いはありますか、それとも同等であると信じて正しいのでしょうか。静的チェッカーが3番目のケースを正しく評価できないというだけですか。

//Works

private Int64? _violations = null;

[ContractInvariantMethod]
private void ObjectInvariant()
{
    Contract.Invariant(CheckIsValid(_violations));
}

[Pure]
public static Boolean CheckIsValid(Int64? value)
{
    return (value.HasValue ? value.Value >= 0 : true);
}

public Class1(Int64 violations)
{
    Contract.Requires(violations >= 0);
    Contract.Ensures(CheckIsValid(_violations));
    _violations = violations;
}


//Doesn't work, not provably deterministic

private Int64? _violations = null;

[ContractInvariantMethod]
private void ObjectInvariant()
{
    Contract.Invariant(_violations.HasValue ? _violations.Value >= 0 : true);
}

public Class1(Int64 violations)
{
    Contract.Requires(violations >= 0);
    Contract.Ensures(_violations.HasValue ? _violations.Value >= 0 : true);
    _violations = violations;
}

//Also doesn't work, even though it's provably deterministic

private PureNullableInt64 _violations = null; //A wrapper class around Int64? with [Pure] getters

[ContractInvariantMethod]
private void ObjectInvariant()
{
    Contract.Invariant(_violations.HasValue ? _violations.Value >= 0 : true);
}

public Class1(Int64 violations)
{
    Contract.Requires(violations >= 0);
    Contract.Ensures(_violations.HasValue ? _violations.Value >= 0 : true);
    _violations = violations;
}
4

1 に答える 1

2

3つのバージョンはすべて同じであり、最初のバージョンも機能しません。警告レベルが十分に低く設定されているため、警告がマスクされるため、そのように見えます。警告レベルを最高に設定してみてください。「証明されていないことを確認します」という警告が表示されます。

問題は、という契約がないことnew Nullable<T>(x).Value == xです。と言う契約だけがありますnew Nullable<T>(x).HasValue。それはあなたの不変条件を証明するのに十分ではありません。基本クラスに指定する必要があるが、まだ指定されていない多くのコントラクトがあります。これをコード契約フォーラムに持ち込み、追加をリクエストできます。

于 2012-09-03T13:13:18.753 に答える