title: Code Contracts: How to express these conditions?
body: <p>I'm playing around with Code Contracts at the moment and I'm not completely sure whether the static methods of the Contract class are powerful enough to compete with mathematical notation of conditions.</p>
  
  <p>Let's assume we got a simple factorial method</p>
  
  <pre><code>int Factorial(int n);
  </code></pre>
  
  <p>I would express the following conditions:</p>
  
  <pre><code>Precondition:
  n &gt;= 0
  
  Postconditions:
  Factorial(n) = 1, in case n = 0
  Factorial(n) = n*(n-1)*...*1, in case n &gt; 0
  </code></pre>
  
  <p>These conditions clearly specify the behavior of Factorial in a short and clean way. My question is, whether they can be expressed through Code Contracts.</p>
  
  <p>The precondition is trivial:</p>
  
  <pre><code>Contract.Requires(n &gt;= 0)
  </code></pre>
  
  <p>The conditional post condition might be expresses using </p>
  
  <pre><code>if(n==0)
      Contract.Ensures(Contract.Result&lt;int&gt;() == 1);
  if(n &gt; 0)
      ...
  </code></pre>
  
  <p>But I don't like the way I need the "if" statement here as it makes the plain list of pre- and postconditions harder to read. I hoped we would have something like</p>
  
  <pre><code>Contract.Ensures(...).InCase(...);
  </code></pre>
  
  <p>And last but not least, I do not have any idea how to express this, which is a common notation regarding math:</p>
  
  <pre><code>n*(n-1)*...*1
  </code></pre>
  
  <p>Guess I would need some kind of loop, but this would copy the whole implementation. Is there any smart way to express such notations?</p>
  
  <p>Thank you in advance.</p>