title: Awkward looking uses of Contract.ValueAtReturn()
body: <p>I am designing a method that will add an element to an internal list. The structure of the class is something along the lines of:</p>
  
  <pre><code>class MyCustomerDatabase {
      private IList&lt;Customer&gt; _customers = new List&lt;Customer&gt;();
  
      public int NumberOfCustomers { get { return _customers; } }    
  
      public void AddCustomer(Customer customer) {
          _customers.Add(customer);
      }
  }
  </code></pre>
  
  <p>Now, I was thinking of adding a <code>Contract.Ensures()</code> about the size of the _customers growing by 1 with this call. The problem is that I end up with some weird looking code:</p>
  
  <pre><code>public void AddCustomer(Customer customer) {
      int numberOfCustomersAtReturn;
      Contract.Ensures(Contract.ValueAtReturn&lt;int&gt;(out numberOfCustomersAtReturn) == 
  Contract.OldValue&lt;int&gt;(NumberOfCustomers) + 1);
  
  
      _customers.Add(customer);
      numberOfCustomersAtReturn = NumberOfCustomers;
  }
  </code></pre>
  
  <p>The main problem is that properties are in fact methods, so you can't just reference them direcly when using <code>Contract.ValueAtReturn()</code> as its only parameter accepts variables as <code>out</code>.
  The situation gets even odder if I want to achieve the same but this time with a method that should return a value:</p>
  
  <pre><code>public int MyReturningMethod() {
      ...
     return abc(); //abc will add by one the number of customers in list
  }
  //gets converted to
  public int MyReturningMethod() {
      int numberOfCustomersAtReturn;
      Contract.Ensures(Contract.ValueAtReturn&lt;int&gt;(out numberOfCustomersAtReturn) == Contract.OldValue&lt;int&gt;(NumberOfCustomers) + 1);
  
      int returnValue = abc();
      numberOfCustomersAtReturn = NumberOfCustomers;
      return returnValue;
  }
  </code></pre>
  
  <p>This seems pretty clumsy :( </p>
  
  <p>Code Contracts should aim to get things clearer and this seems right the opposite. Am I doing something wrong?</p>
  
  <p>Thanks</p>