使用代码契约来确保集合保持不变

本文关键字：集合 确保 代码 契约 | 更新日期: 2023-09-27 17:58:37

我正在尝试实现一个方法的post条件。我想保证它不会改变内部状态的某个特定部分（我修复了一个错误，就像以前一样。为了进行重构，我在代码中添加了post条件）。我的最佳尝试如下：

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)在第二行中导致了null引用异常。规范合同手册第11.8节(http://research.microsoft.com/en-us/projects/contracts/userdoc.pdf)声明这个特定的Contract.ForAll应该与Contract.OldValue一起工作，但另一个过载则不能。

有没有其他方法可以检查PropertyA.Collection中的项的值没有更改，也没有以某种方式重新排序？

使用代码契约来确保集合保持不变

您的问题不清楚，但我认为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())

这将评估表达式并保存对列表/数组的尊重，然后可以对其进行索引。

很抱歉这么晚才回答，但代码契约中没有太多活动。

我认为问题有两个方面：

1） 为了确保条件，正如你所问的，我认为可以使用[Pure]函数来完成，并在合同中调用该函数。确保

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

1-调用一个函数以确保取消收集的条件2-调用一个确保集合中没有更改的函数3-调用以（1）中确保的条件为前提的函数

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

我认为CodeContracts应该提供一种功能，以确保对象不会发生更改，而是将对象作为"深层对象"；可以让你写类似的东西

方案代码 Contract.Ensures（PureArgument（PropertyA.Collection））

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

方案代码 [PureArgument（PropertyA.Collection）]

请注意，CodeContracts可以检查PureArgument属性是否满足，因为它可以进行深入比较；检查起来非常复杂且昂贵（需要深度复制），但它是可以做到的。但检查不是问题，而是检查代码以确保参数不会发生深刻更改，这并不总是可能的。

无论如何，我相信这样的功能会很好，即使不检查它是否完整地填充断言，也不检查代码以确保参数没有更改（这比检查断言是否完整更有趣，但根本不可能涵盖）。

回到问题上来，确保集合不会更改的解决方案可以是使用new ReadOnlyCollection（PropertyA.collection）作为参数，而不是使用PropertyA，但这是代码中的更改。

相关文章：