0

コード コントラクトで装飾した簡単なグラフ操作メソッドを次に示します。

ensure クレームは証明されませんが、理由がわかりません! Remove() を呼び出した後、エッジがエッジ リストにないか、結果が false であると主張していると思います。結果が true の場合、グラフの状態については何も主張しません。静的チェッカーはそれを気に入らず、Pex にその方法を教えてもらっていません (ただし、おそらく使い方がわからないだけです)。

この例ではロックは無関係だと思いますが、念のためそのままにしておきます。また、OnRemoveEdge のデリゲートには何の保証もありませんが、ここでは、Graph コードに再入可能ではないと暗黙的に仮定します。その上、仮定はその後です。

public bool Remove(E edge)
{
  Contract.Requires(edge != null);
  Contract.Ensures(!Contract.Exists(edges, e => e == edge) || !Contract.Result<bool>());

  lock (sync)
  {
    if (!OnBeforeRemoveEdge(edge)) return false;

    if (!edges.Remove(edge)) return false;
  }

  OnRemoveEdge(edge);

  Contract.Assume(!Contract.Exists(edges, e => e == edge));

  return true;
}

更新: コードを変更して、イベント ハンドラー OnRemoveEdge() (ただし、デリゲート OnBeforeRemoveEdge は除く) をロックから外しました。しかし、これは、スレッドに関連するコントラクトの前提に対して何をするのでしょうか? コード コントラクトはシングル スレッド モデルを想定していますか? うーん。

4

1 に答える 1

1

同様の質問に対するJack Leitchの回答から：

Code Contracts User Manualには、「静的コントラクト チェッカーは、ForAll または Exists の量指定子をまだ処理していません」と記載されています。

真実。真実。

于 2011-02-03T17:25:53.283 に答える