Contract.ValueAtReturn() 的使用看起来很尴尬

Question

我正在设计一种将元素添加到内部列表的方法。类的结构大致如下：

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

    public int NumberOfCustomers { get { return _customers; } }    

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

现在，我正在考虑添加一个 Contract.Ensures()，它的大小与 _customers 的大小在此调用中增长了 1。问题是我最终得到了一些看起来很奇怪的代码：

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


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

主要问题是属性实际上是方法，所以当使用Contract.ValueAtReturn() 时不能直接引用它们，因为它的唯一参数接受变量为out。 如果我想达到同样的效果，情况会变得更加奇怪，但这次使用应该返回值的方法：

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;
}

这看起来很笨拙:(

代码契约应该旨在让事情变得更清晰，而这似乎恰恰相反。我做错了吗？

谢谢

Answer 1

您似乎无缘无故地把事情复杂化了。 ValueAtReturn 用于谈论方法的 out 参数，仅此而已 - 而且您没有任何 out 参数！

你要找的是OldValue。

假设这一行：

public int NumberOfCustomers { get { return _customers; } }   

意味着：

public int NumberOfCustomers { get { return _customers.Count; } }

你所要做的就是：

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

    public int NumberOfCustomers { get { return customers.Count; } }

    public void AddCustomer(Customer customer)
    {
        Contract.Ensures(NumberOfCustomers ==
                         Contract.OldValue(NumberOfCustomers) + 1);

        customers.Add(customer);
    }
}

得益于IList<T> 中的后置条件，静态检查器可以很好地证明这一点：)

Answer 2

我认为你做的一切都是对的。

尽管我觉得您通过描述调用该方法的确切输出含义将合同发挥到了极致。恕我直言，合同的基本理念更多的是确保基本保证，例如积极、完全返回值等等。