9

次のコードを想定します。

[ContractClass(typeof(ICC4Contract))]
public interface ICC4
{
    bool IsFooSet { get; }
    string Foo { get; }
}

public class CC4 : ICC4
{
    private string _foo;

    public bool IsFooSet { get { return Foo != null; } }

    public string Foo { get { return _foo; } }
}

[ContractClassFor(typeof(ICC4))]
public abstract class ICC4Contract : ICC4
{
    public bool IsFooSet
    {
        get
        {
            Contract.Ensures((Contract.Result<bool>() && Foo != null)
                             || !Contract.Result<bool>());
            return false;
        }
    }

    public string Foo
    {
        get
        {
            Contract.Ensures((Contract.Result<string>() != null && IsFooSet)
                             || !IsFooSet);
            return null;
        }
    }
}

契約は次のように言おうとしています。

  1. IsFooSetそうでないtrue場合は戻ります。Foonull
  2. Foonull返された場合IsFooSetは返されませんtrue。

これはほとんど機能します。ただし、チェッカーはが常に と等しいことを認識していないため、 に
「証明されていないことを保証します」と表示されます。 return _foo;Foo_foo

Fooセッターを使用して自動プロパティに変更すると、privateその警告が削除されますが、私はそうしたくありません (プライベート セッターを使用した自動プロパティは好きではありません)。

_fooフィールドを保持しながら警告を消すには、上記のコードで何を変更する必要がありますか?

以下は機能しません。

  1. の代わりIsFooSetに使用するように変更します。で追加の「証明されていない保証」が発生します。_fooFooIsFooSet
  2. 不変式の追加Foo == _foo。これにより、暗黙のデフォルトコンストラクターで「不変の未証明」が発生します。さらに、実際のコードベースでは、静的チェッカーの処理時間は大幅に長くなります。
  3. この回答に従ってContract.Ensures(Contract.Result<string>() == _foo);のゲッターに追加しても、何も変わりません。Foo
4

1 に答える 1

2

短絡を使用して条件を単純化できますが、それは何らかの理由で機能します。

[ContractClassFor(typeof(ICC4))]
public abstract class ICC4Contract : ICC4
{
    public bool IsFooSet
    {
        get
        {
            Contract.Ensures(!Contract.Result<bool>() || Foo != null);
            return false;
        }
    }

    public string Foo
    {
        get
        {
            Contract.Ensures(!IsFooSet || Contract.Result<string>() != null);
            return null;
        }
    }
}
于 2013-03-10T11:31:08.930 に答える