10

私は C# 4.0 と Code Contracts を使用しており、独自のカスタムGameRoomCollection : IEnumerable<GameRoom>.

のインスタンスに値要素GameRoomCollectionが含まれないようにしたいと思います。nullしかし、私はこれができないようです。一般的なルールを作成する代わりに、わかりやすく単純な例を作成しようとしました。はのAllGameRoomsインスタンスですGameRoomCollection

private void SetupListeners(GameRoom newGameRoom) {
  Contract.Requires(newGameRoom != null);
  //...
}
private void SetupListeners(Model model) {
    Contract.Requires(model != null);
    Contract.Requires(model.AllGameRooms != null);
    Contract.Assume(Contract.ForAll(model.AllGameRooms, g => g != null));
    foreach (GameRoom gameRoom in model.AllGameRooms)
        SetupListeners(gameRoom);//<= Warning: Code Contracts: Requires unproven: newGameRoom != null 
}

なぜ私が証明していないのか、誰にもわかりますgameRoomnull?

編集:

反復する前にオブジェクトの参照を追加しても機能しません。

IEnumerable<IGameRoom> gameRooms = model.AllGameRooms;
Contract.Assume(Contract.ForAll(gameRooms, g => g != null));
foreach (IGameRoom gameRoom in gameRooms)
    SetupListeners(gameRoom);//<= Warning: Code Contracts: Requires unproven: newGameRoom != null 

EDIT2:

ただし: ゲーム ルームのコレクション タイプを配列に変換すると、正常に動作します。

IGameRoom[] gameRoomArray = model.AllGameRooms.ToArray();
Contract.Assume(Contract.ForAll(gameRoomArray, g => g != null));
foreach (IGameRoom gameRoom in gameRoomArray)
    SetupListeners(gameRoom);//<= NO WARNING

IEnumerable<T>これは、インターフェイスのメソッドのルールを定義できないことが原因ですか?

EDIT3:問題はこの質問に何らかの形で関連している可能性がありますか?

4

2 に答える 2

2

これは GetEnumerator メソッドの純度に関係しているのではないかと思います。PureAttribute

コントラクトは、[Pure] (副作用なし) として定義されているメソッドのみを受け入れます。

いくつかの追加情報コード コントラクト、純粋さを探す

引用:

純度

コントラクト内で呼び出されるすべてのメソッドは純粋でなければなりません。つまり、既存の状態を更新してはなりません。純粋メソッドは、純粋メソッドに入った後に作成されたオブジェクトを変更できます。

コード コントラクト ツールは現在、次のコード要素が純粋であると想定しています。

PureAttribute でマークされたメソッド。

PureAttribute でマークされた型 (属性はすべての型のメソッドに適用されます)。

プロパティ get アクセサー。

演算子 (名前が「op」で始まり、1 つまたは 2 つのパラメーターと void 以外の戻り値の型を持つ静的メソッド)。

完全修飾名が「System.Diagnostics.Contracts.Contract」、「System.String」、「System.IO.Path」、または「System.Type」で始まるメソッド。

デリゲート型自体が PureAttribute に関連付けられている場合、呼び出されたデリゲート。デリゲート型 System.Predicate および System.Comparison は純粋と見なされます。

于 2011-03-02T01:47:37.510 に答える
0

プロパティへのアクセスごとに異なる可能性のある をmodel.AllGameRooms返すためだと思います。IEnumerable<GameRoom>

使用してみてください:

var gameRooms = mode.AllGameRooms;
Contract.Assume(Contract.ForAll(gameRooms, g => g != null));
foreach (IGameRoom gameRoom in gameRooms)
    SetupListeners(gameRoom);    
于 2011-02-17T22:50:35.093 に答える