Using Code Contracts to ensure collection remains unchanged
I'm trying to implement the post-condition of a method. I want to guarantee that it doesn't change a particular part of the internal state (I fixed a bug, as it used to do so. For refression purposed, I'm adding the post-condition in code). My best attempt was as follows:
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])));
The problem with this code is that Contract.OldValue(PropertyA.Collection) caused a null reference exception in the second line. In the manual of Code Contracts in section 11.8 (http://research.microsoft.com/en-us/projects/contracts/userdoc.pdf) is stated that this particular Contract.ForAll ought to work with Contract.OldValue , but another overload doesn't.
Is there another way how I can perform the check that the items in PropertyA.Collection haven't changed in value, nor have been reordered in some way?
It is unclear from your question, but I expect that PropertyA.Collection and PropertyB.Collection are reference types. One gotcha with Contracts.OldValue() and reference types is, that Contracts.OldValue() doesn't save the old object pointed at, but rather the pointer itself.
For this reason, your first contract will always be true, since you effectively compare the value to itself. The proper way to write it would be
Contract.Ensures(PropertyA.Collection.Count == Contract.OldValue(PropertyA.Collection.Count));
I'm not sure why your second contract fails. Normally when trying to compare a collection before and after a method call, you need to save the collection as an enumerable:
Contract.OldValue(PropertyA.Collection.ToList())
// or
Contract.OldValue(PropertyA.Collection.ToArray())
This will evaluate the expression and save the reverence to the list/array, which can then be indexed.
Sorry to answer so late, but there are not too much activity in code contracts.
I think there are two sides of the problem:
1) To ensure the condition, as you ask, I think that can be done using a [Pure] function to do it, and calling this function in the Contract.Ensures
2) Unfortunately it only solves the problem locally. Note this situation:
1- Call a function which ensures a condition on de collection 2- Call a function which ensures no change in the collection 3- Call a function which has as precondition the condition ensured in (1)
The [Pure] function in (2) to ensure no change is done in the collection does not allow CodeContracts to infer that the postcondition in (1) ensures the precondition in (3).
I think that CodeContracts should offer a functionality to ensure no change in an object, but taking the object as the "deep object"; something that lets you write something like
proposal code Contract.Ensures(PureArgument(PropertyA.Collection))
As the functionality PureArgument should be part of CodeContracts, it could be an attribute:
proposal code [PureArgument(PropertyA.Collection)]
Note that CodeContracts could check that the PureArgument property is fulfilled, as it can do a deep compare; really complex and expensive to check (it needs a deep copy), but it can be done. But the checking won't be the question, but to check the code to ensure that the parameter is not deep changed, which is not always possible.
Anyway, I'm sure that a feature like that will be great, even without checking it fullfils the assertion, and without checking the code to ensure the parameter is not changed (which is more interesting than checking the assertion is fullfiled, but impossible to cover at all).
Turning back to the question, a solution to ensure that a collection doesn't change could be to use new ReadOnlyCollection(PropertyA.Collection) as parameter, instead of using PropertyA, but it is a change in the code.
链接地址: http://www.djcxy.com/p/59604.html上一篇: Sandcastle：有什么方法显示继承成员而不显示基类？
下一篇: 使用代码合约确保收集保持不变