Awkward looking uses of Contract.ValueAtReturn()

Posted by devoured elysium on Stack Overflow See other posts from Stack Overflow or by devoured elysium
Published on 2010-05-06T10:46:45Z Indexed on 2010/05/06 10:58 UTC
Read the original article Hit count: 307

Filed under:
|
|
|

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

© Stack Overflow or respective owner

Related posts about c#

Related posts about code-contracts