title: Code Contracts - ForAll - What is supported by static verification
body: <p>There are numerous information that static checking of <code>Contract.ForAll</code> has only limited or no support.</p>
  
  <p>I did lot of experimenting and found <strong>it can work with</strong>:</p>
  
  <ul>
  <li><code>Contract.ForAll(items, i =&gt; i != null)</code></li>
  <li><code>Contract.ForAll(items, p)</code> where <code>p</code> is of type <code>Predicate&lt;T&gt;</code></li>
  </ul>
  
  <p>it <strong>cannot</strong> work with:</p>
  
  <ul>
  <li>Field access</li>
  <li>Property access</li>
  <li>Method group (I think delegate is allocated here anyway)</li>
  <li>Instance method call</li>
  </ul>
  
  <p>My <strong>questions</strong> are:</p>
  
  <ul>
  <li>What are other types of code that <code>ForAll</code> can work with?</li>
  <li>Does the Code Contracts undertand that after <code>Contract.ForAll(items, i =&gt; i != null)</code> is proven, that when taking one item from the list later in code (i.e. by indexing), the item is not null?</li>
  </ul>
  
  <p>Here is full test code:</p>
  
  <pre><code>public sealed class Test
  {
      public bool Field;
      public static Predicate&lt;Test&gt; Predicate;
  
      [Pure]
      public bool Property
      {
          get { return Field; }
      }    
  
      [Pure]
      public static bool Method(Test t)
      {
          return t.Field;
      }
  
      [Pure]
      public bool InstanceMethod()
      {
          return Field;
      }
  
      public static void Test1()
      {
          var items = new List&lt;Test&gt;();
          Contract.Assume(Contract.ForAll(items, i =&gt; i != null));
          Contract.Assert(Contract.ForAll(items, i =&gt; i != null)); // OK
      }
  
      public static void Test2()
      {
          var items = new List&lt;Test&gt;();
          Contract.Assume(Contract.ForAll(items, Predicate));
          Contract.Assert(Contract.ForAll(items, Predicate)); // OK
      }
  
      public static void Test3()
      {
          var items = new List&lt;Test&gt;();
          Contract.Assume(Contract.ForAll(items, i =&gt; i.Field));
          Contract.Assert(Contract.ForAll(items, i =&gt; i.Field)); // assert unproven
      }
  
      public static void Test4()
      {
          var items = new List&lt;Test&gt;();
          Contract.Assume(Contract.ForAll(items, i =&gt; i.Property));
          Contract.Assert(Contract.ForAll(items, i =&gt; i.Property)); // assert unproven
      }
  
      public static void Test5()
      {
          var items = new List&lt;Test&gt;();
          Contract.Assume(Contract.ForAll(items, Method));
          Contract.Assert(Contract.ForAll(items, Method)); // assert unproven
      }
  
      public static void Test6()
      {
          var items = new List&lt;Test&gt;();
          Contract.Assume(Contract.ForAll(items, i =&gt; i.InstanceMethod()));
          Contract.Assert(Contract.ForAll(items, i =&gt; i.InstanceMethod()));// assert unproven
      }
  }
  </code></pre>