title: Preconditions and Postconditions in CodeContracts
body: <p>If I write  </p>
  
  <pre><code> [Pure]
   static string s10 {get;set;}
  
   static void Main(string[] args)
   {
       Contract.Ensures(s10.Length &lt;= 10); //Contract fails
       s10 = ";uhlakushdflausgdflasgdfljgaskdjgfasd";
   }
  </code></pre>
  
  <p>As I don't have Premium edition of VS, so no static checking, after run program VS reports me problem: <code>Postcondition failed: s10.Length &lt;= 10</code>, good. </p>
  
  <p>if I write, instead </p>
  
  <pre><code> [Pure]
   static string s10 {get;set;}
  
   static void Main(string[] args)
   {
      Contract.Requires(s10.Length &lt;= 10); //NullReferenceException
      s10 = ";uhlakushdflausgdflasgdfljgaskdjgfasd";
   }
  </code></pre>
  
  <p>VS reports me Null reference exception. </p>
  
  <p>Does it actually mean, that as <code>Ensures</code> is postcondition dirrective, even if I put its call like a first line of my method, it will be validated like last one, just before exiting the function ?</p>