Databases
StackOverflow2013
Postsdbo
POCode contracts, forall and custom enumerable
Body
 

Note that there are some explanatory texts on larger screens.

plurals
  1. POCode contracts, forall and custom enumerable
    text
    copied!<p>I am using C# 4.0 and Code Contracts and I have my own custom <code>GameRoomCollection : IEnumerable&lt;GameRoom&gt;</code>.</p> <p>I want to ensure, that no instances of <code>GameRoomCollection</code> will ever contain a <code>null</code> value element. I don't seem to be able to this, though. Instead of making a general rule, I have tried to do a plain and simple example. The <code>AllGameRooms</code> is an instance of <code>GameRoomCollection</code>.</p> <pre><code>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 =&gt; g != null)); foreach (GameRoom gameRoom in model.AllGameRooms) SetupListeners(gameRoom);//&lt;= Warning: Code Contracts: Requires unproven: newGameRoom != null } </code></pre> <p>Can anyone see, why I haven't proven, that <code>gameRoom</code> is not <code>null</code>?</p> <p><strong>EDIT:</strong></p> <p>Adding a reference for the object before iterating does not work either:</p> <pre><code>IEnumerable&lt;IGameRoom&gt; gameRooms = model.AllGameRooms; Contract.Assume(Contract.ForAll(gameRooms, g =&gt; g != null)); foreach (IGameRoom gameRoom in gameRooms) SetupListeners(gameRoom);//&lt;= Warning: Code Contracts: Requires unproven: newGameRoom != null </code></pre> <p><strong>EDIT2:</strong></p> <p>However: If I convert the game room collection type to an array, it works fine:</p> <pre><code>IGameRoom[] gameRoomArray = model.AllGameRooms.ToArray(); Contract.Assume(Contract.ForAll(gameRoomArray, g =&gt; g != null)); foreach (IGameRoom gameRoom in gameRoomArray) SetupListeners(gameRoom);//&lt;= NO WARNING </code></pre> <p>Is this caused by the fact, that you cannot define a rule for methods of the <code>IEnumerable&lt;T&gt;</code> interface?</p> <p><strong>EDIT3:</strong> Can the problem somehow be related to <a href="https://stackoverflow.com/questions/3104856/using-contract-forall-in-code-contracts">this question</a>?</p>
 

Querying!

 
Guidance
An individual column

Larger individual text columns get their own page to allow for proper reading.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload