title: Post- and Preconditions
body: <p>I was just reading the documentation for the Bosque Programming Language and came across <a href="https://github.com/Microsoft/BosqueLanguage/blob/master/docs/language/overview.md#0.12-Errors-and-Checks" rel="nofollow noreferrer">section 12</a> about errors and checks </p>
  
  <p>I was wondering if C# has a similar concept to post and preconditions.
  At first glimpse, I thought that this looks like guard clauses but from a Language perspective, one isn't entering the method at all with these preconditions.</p>
  
  <p><em>Since the documentation is fairly new I will post the source code which I am talking about here:</em></p>
  
  <pre><code>entity Foo {
      field x: Int;
  
      invariant x &gt; 0; //check whenever a Foo is constructed
  
      method m(y: Int): Int
          requires y &gt;= 0; //precondition
          ensures _result_ &gt; 0; //postcondition
      {
          check this.x - y &gt; 0;   //sanity check - enabled on optimized builds
          assert this.x * y != 0; //diagnostic assert - only for test/debug
  
          return x * y;
      }
  }
  </code></pre>
  
  <p>In C# I would normally write something like this</p>
  
  <pre><code>internal class Foo 
  {
      private int x;
  
      public int  m(int y)
      {
          if(y&lt;0) //Negative guard clause
          {
              //throw an exception
          }
          //Assertions 
          int result = x * y;
  
          if(result&lt;0)
          {
              //throw an exception
          }
          return result;
      }
  }
  </code></pre>
  
  <p>While writing this question I came across code contracts in C# which act in a similar way than guard clauses it seems. <code>Contract.Requires</code> in C# looks to me more like the <code>check</code> and <code>assert</code> statements inside of the method.</p>
  
  <p>So my question is:
  Is there a similar concept which executes before entering the method or in the case of the postcondition afterwards?</p>