How does Contract.Exists add value?

Question

I am just starting to learn about the code contracts library that comes standard with VS2010. One thing I am running into right away is what some of the contract clauses really mean.

For example, how are these two statements different?

Contract.Requires(!mycollection.Any(a => a.ID == newID));
Contract.Requires(!Contract.Exists(mycollection, a => a.ID == newID));

In other words, what does Contract.Exists do in practical purposes, either for a developer using my function, or for the static code analysis system?

Answer 1

The version that uses Contract.Exists is preferred due to its declarative nature. Another advantage is that the framework knows this contract and it has better chance of being "caught" in static analysis.

Answer 2

Ok, I found the answer. According to the Code Contracts User Manual, section 2.7.2:

"It is also possible to use the extension method System.Linq.Enumerable.Any instead of Contract.Exists ."

So they are equivalent. I will use Any instead of Exists, so it is consistent with the rest of our code.