title: Issues with Contract.Requires() and loop invariant
body: <p>I am following the codecontracts tutorial (<a href="https://docs.microsoft.com/en-us/dotnet/framework/debug-trace-profile/code-contracts#usage-guidelines" rel="nofollow noreferrer">https://docs.microsoft.com/en-us/dotnet/framework/debug-trace-profile/code-contracts#usage-guidelines</a>) and I seem to have trouble getting the simplest thing working. Given the method definition</p>
  
  <pre><code>public int Add(int x, int y)
  {
     Contract.Requires(x &gt; 0);
     Contract.Requires(y &gt; 0);
  
     return x+y;
  }
  </code></pre>
  
  <p>when I am calling <code>o.Add(0,0)</code> The method does not fail the pre-condition check. When I am in debugging mode, the <code>Contract.Requires()</code> statements are skipped. Where I am doing wrong?</p>
  
  <p>Second question can I use <code>Contract.Invariant()</code> to check loop invariant? According to the definition of object invariant <code>Object invariants are conditions that should be true for each instance of a class whenever that object is visible to a client.</code>which seems to be a little different from loop invariant since in each loop iteration the loop invariant may not be necessarily visible to a client so it may violates the property but not get checked. Is this understanding correct? </p>