3

コード コントラクトを使用して順序を強制する、不変の順序付き単一リンク リスト クラスを設定しようとしています。この例に要約されるいくつかの問題に遭遇しています。

[Pure, ContractVerification(true)]
public class Hierarchy
{
    private readonly object _data;
    private readonly Hierarchy _childField;

    public Hierarchy() { }

    public Hierarchy(object data, Hierarchy childParameter) {
        Contract.Requires<ArgumentNullException>(childParameter != null);

        _data = data;
        _childField = childParameter;

        Contract.Assert(HasChild);

        Contract.Assert(_childField == childParameter);
        Contract.Assert(_childField.Data == childParameter.Data);

        Contract.Assert(ChildProperty == _childField);
        Contract.Assert(ChildProperty.Data == _childField.Data);  //Warning -- CodeContracts: assert unproven
    }

    public bool HasChild { get { return _childField != null; } }

    public object Data {
        get {
            Contract.Ensures(Contract.Result<object>() == _data);
            return _data;
        }
    }

    public Hierarchy ChildProperty {
        get {
            Contract.Requires<InvalidOperationException>(HasChild);
            Contract.Ensures(Contract.Result<Hierarchy>() == _childField);

            //un-commenting this line causes the assertion to succeed.
            //Contract.Ensures(Contract.Result<Hierarchy>().Data == _childField.Data);

            return _childField;
        }
    }

    [ContractInvariantMethod]
    private void Invariant() {
        Contract.Invariant(HasChild == (ChildProperty != null));
    }
}

コード コントラクトは、アサーションを証明できる必要があるように思えますChildProperty.Data == _childField.Data。以前のアサーションChildProperty == _childFieldは成功し、同じオブジェクトに対して純粋なDataプロパティ ゲッターを 2 回呼び出すと、同じ結果が返されます。

と という (成功した) 以前のアサーションにも注意して_childField == childParameterください_childField.Data == childParameter.Data。

上記の 2 番目のコメントで述べたように、問題は事後条件Contract.Ensures(Contract.Result<Hierarchy>().Data == _child.Data);をChildPropertyゲッターに追加することで解決されます。必要な作業はこれだけであることに注意してください。この場合、コード コントラクトは、 whenが x と y で getter をx == y呼び出しても同じ結果が得られることを認識します。Data

この回避策は、この小さな例では問題ありませんが、大規模なクラスの場合、型のプロパティごとに事後条件を追加する必要があるのは面倒です (ややばかげていることは言うまでもありません)。

バグですか？アサーションChild.Data == _child.Dataを証明できるコントラクト アノテーションなどを見逃していませんか? 言い換えれば、問題を解決する他の方法はありますか?

4

2 に答える 2

3

あなたは、絶対に正しい。これは証明できるはずですが、静的チェッカーの制限によるものではありません。

于 2013-04-24T22:09:08.763 に答える
0

Dataプロパティがの内容を変更しないという保証をしないためでしょうか_data(ただしreadonly、その内容は潜在的に変更可能です)。

たとえば、次のようなものがあるとします。

public object Data {
    get {
        Contract.Ensures(Contract.Result<object>() == _data);
        ((SomeClass)_data).SomeProperty += 1;
        return _data;
    }
}

その後、2 回連続して を呼び出すとData、異なる結果が得られます。

Dataこれをのget作業に追加しますか?

Contract.Ensures(_data == Contract.OldValue<object>(_data));
于 2013-04-12T21:52:07.510 に答える