Code Contracts: How do I state in a post-condition that a field/property's value has not changed?
-
23-09-2019 - |
Question
I'll best just show with a code example what I would like to accomplish?
class SomeClass
{
public int SomeProperty;
public void SomeOperation()
{
Contract.Ensures( "SomeProperty's value has not changed." );
// ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
// How can I write this post-condition?
}
};
(The string passed to Contract.Ensures()
is of course just a placeholder for the real post-condition expression.)
How can I do this? Would Contract.OldValue<>()
be of any use here?
Solution
Contract.OldValue
should be enough:
Contract.Ensures(this.SomeProperty == Contract.OldValue(this.SomePropety));
Licensed under: CC-BY-SA with attribution
Not affiliated with StackOverflow