使用代码合同确保收集保持不变

我试图实现方法的后置条件。我想保证它不会改变内部状态的某个特定部分（我修正了一个bug，因为它曾经这样做过，为了达到目的，我在代码中添加了后置条件）。我最好的尝试是如下：使用代码合同确保收集保持不变

Contract.Ensures(PropertyA.Collection.Count == Contract.OldValue(PropertyA.Collection).Count); 
Contract.Ensures(Contract.ForAll(0, PropertyA.Collection.Count, index => this.PropertyA.Collection[index].Equals(Contract.OldValue(this.PropertyA.Collection)[index])));

这段代码的问题是，Contract.OldValue(PropertyA.Collection)导致在第二行一个空引用异常。在第11.8节（http://research.microsoft.com/en-us/projects/contracts/userdoc.pdf）中的代码合同手册中声明，这个特定的Contract.ForAll应该与Contract.OldValue一起使用，但另一个超载不适用。

是否有另一种方式，我可以执行检查PropertyA.Collection中的项目没有改变价值，也没有以某种方式重新排序？

来源

2014-04-16 Xilconic

我可能会写一个测试，而不是使用前置/后置条件来跟踪回归没有，好吧，再次倒退。这样你仍然会注意到，你不会每次都检查你的呼叫者。 – Joey

@Јοеу：我已经写了一个测试，所以它也覆盖了那里。来电者没有义务检查发布条件。被调用的方法保证PropertyA的Collection不受影响。 – Xilconic

我的意思是性能上的负担，而不是调用者每次都需要做点什么:-) – Joey

目前还不清楚你的问题，但我预计PropertyA.Collection和PropertyB.Collection是引用类型。与Contracts.OldValue()和引用类型的一个陷阱是，那Contracts.OldValue()不保存指向的旧对象，而是指针本身。

因此，您的第一份合同将始终为真，因为您将该值有效地与自身进行了比较。正确的方式来写这将是

Contract.Ensures(PropertyA.Collection.Count == Contract.OldValue(PropertyA.Collection.Count));

我不知道为什么你的第二个合同失败。通常尝试之前和方法调用之后，比较了集合时，你需要收集保存为一个枚举：

Contract.OldValue(PropertyA.Collection.ToList()) 
// or 
Contract.OldValue(PropertyA.Collection.ToArray())

这将计算表达式和崇敬保存到列表/数组，然后可以被索引。

来源

2016-03-30 17:19:31

很抱歉回答这么晚，但代码合同中没有太多的活动。

我觉得有问题的两面：

1）为保证的条件下，如你问，我认为可以用[纯]功能做到这一点，并调用这个函数中完成合同。保证

2）不幸的是，它只能在本地解决问题。注意这样的情况：

1-呼叫其确保对德收集 2-呼叫这确保了收集 3-呼叫，其具有作为先决条件的条件确保了功能中没有改变的功能的状态的功能（1）

（2）中的[Pure]函数确保集合中未做任何更改不允许CodeContracts推断（1）中的后置条件确保（3）中的前提条件。

我认为CodeContracts应该提供一种功能，以确保对象没有变化，但将对象视为“深层对象”;的东西，可以让你喜欢写东西

建议代码 Contract.Ensures（PureArgument（PropertyA。集））

由于功能PureArgument应该CodeContracts的一部分，它可能是一个属性：

建议代码 [PureArgument（PropertyA.Collection）

注CodeContracts可以检查PureArgument属性是否已完成，因为它可以进行深入比较;检查非常复杂且昂贵（需要深层复制），但可以完成。但是检查不会是问题，而是检查代码以确保参数没有发生深刻变化，这并非总是可行。

无论如何，我敢肯定，即使没有检查完全填充断言，并且不检查代码以确保参数未被更改（这比检查断言是否全满，但根本不可能覆盖）。

再回到这个问题，一个解决方案，以确保集合不会改变可能是使用新的ReadOnlyCollection（PropertyA.Collection）作为参数，而不是使用PropertyA，但它是在代码中的变化。

来源

2016-10-28 18:15:38 Cesc

使用代码合同确保收集保持不变

回答

相关问题