Awkward looking uses of Contract.ValueAtReturn()

Question

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:

class MyCustomerDatabase {
    private IList<Customer> _customers = new List<Customer>();

    public int NumberOfCustomers { get { return _customers; } }    

    public void AddCustomer(Customer customer) {
        _customers.Add(customer);
    }
}

Now, I was thinking of adding a Contract.Ensures() about the size of the _customers growing by 1 with this call. The problem is that I end up with some weird looking code:

public void AddCustomer(Customer customer) {
    int numberOfCustomersAtReturn;
    Contract.Ensures(Contract.ValueAtReturn<int>(out numberOfCustomersAtReturn) == 
Contract.OldValue<int>(NumberOfCustomers) + 1);


    _customers.Add(customer);
    numberOfCustomersAtReturn = NumberOfCustomers;
}

The main problem is that properties are in fact methods, so you can't just reference them direcly when using Contract.ValueAtReturn() as its only parameter accepts variables as out. The situation gets even odder if I want to achieve the same but this time with a method that should return a value:

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<int>(out numberOfCustomersAtReturn) == Contract.OldValue<int>(NumberOfCustomers) + 1);

    int returnValue = abc();
    numberOfCustomersAtReturn = NumberOfCustomers;
    return returnValue;
}

This seems pretty clumsy :(

Code Contracts should aim to get things clearer and this seems right the opposite. Am I doing something wrong?

Thanks

Answer 1

I think you are doing everything right.

Altough I have the feeling you are taking Contracts to the extreme by describing the exact output implications of calling that method. Imho the basic idea of Contracts was more to ensure basic guarantees, like being positive, returning a value at all and so on.