2

コード コントラクトを使用した配列ベースのスタックの次の部分的な実装を静的に検証しようとしています。メソッドPop()は純粋な関数IsNotEmpty()を使用して、後続の配列アクセスが下限以上になるようにします。静的ベリファイアは失敗し、前提条件を追加するよう提案しますContract.Requires(0 <= this.top)。

検証者が、与えられたコントラクトの下限に関して配列アクセスが有効であることを証明できない理由を誰でも説明できますIsNotEmpty()か?

最初はContract.Requires(IsNotEmpty())、サブクラスが をオーバーライドする可能性があるため、このアプローチは正しくないのではないかと考えましたIsNotEmpty()。ただし、クラスを としてマークすると、ベリファイアは配列アクセスが有効であることを証明できませんsealed。

更新:IsNotEmpty()読み取り専用のプロパティに変更すると、検証は期待どおりに成功します。これは疑問を投げかけます:読み取り専用プロパティと純粋な関数はどのように/なぜ異なる方法で扱われるのでしょうか? 

class StackAr<T>
{
    private T[] data;
    private int capacity;

    /// <summary>
    /// the index of the top array element
    /// </summary>
    private int top;

    [ContractInvariantMethod]
    private void ObjectInvariant()
    {
        Contract.Invariant(data != null);
        Contract.Invariant(top < capacity);
        Contract.Invariant(top >= -1);
        Contract.Invariant(capacity == data.Length);
    }

    public StackAr(int capacity)
    {
        Contract.Requires(capacity > 0);
        this.capacity = capacity;
        this.data = new T[capacity];
        top = -1;
    }

    [Pure]
    public bool IsNotEmpty()
    {
        return 0 <= this.top;
    }

    public T Pop()
    {
        Contract.Requires(IsNotEmpty());

        //CodeContracts: Suggested precondition: 
        //Contract.Requires(0 <= this.top);

        T element = data[top];
        top--;
        return element;
    }
}
4

1 に答える 1

4

これで問題が解決するはずです。

[Pure]
public bool IsNotEmpty() {
    Contract.Ensures(Contract.Result<bool>() && 0 <= this.top || !Contract.Result<bool>() && 0 > this.top);
    return 0 <= this.top;
}

詳細については、コードコントラクトフォーラムのこのスレッドを参照してください：Contract.Requiresでメソッドを呼び出す

編集：

上記のリンク先のスレッドで説明されているように、この問題のもう1つの解決策は、-inferコマンドラインオプションです。

これで、このメソッドのpost条件を推測することが可能になり、実際にそうするオプションがあります。静的チェッカーのコントラクトプロパティペインの追加オプション行に-infersuresを追加してみてください。

私はチェックしました、そしてこれは問題を解決します。コードコントラクトのマニュアルを見ると、デフォルトのオプションはプロパティの事後条件のみを推測することであることがわかります。このスイッチを使用すると、メソッドの事後条件も推測するように指示できます。

-推論（requires + propertyensures + methodensures）（default = propertyensures）

于 2010-09-12T17:42:01.603 に答える