Code Contracts: How to Satisfy "Guaranteed Unproven" at Agent?

Question

I have the following interface:

[ContractClass(typeof(MyObjectContract))] public interface IMyObject { int CountOfItems { get; } } 

The following contract:

 [ContractClassFor(typeof(IMyObject))] public abstract class MyObjectContract { int IMyObject.CountOfItems { get { Contract.Ensures(Contract.Result<int>() > 0); return 1; } } } 

The following implementation:

 public class MyObject : IMyObject { private IEnumerable someEnumerable .... public int CountOfItems { get { return this.someEnumerable.Count(); } } } 

Now I get a warning: ensures unproven: Contract.Result<int>() > 0

How can I prove that the number is greater than zero? I don't want to throw an exception in the getter, what am I missing?

thanks

Answer 1

As already mentioned, you cannot statically prove that IEnumerable<T>.Count() returns a value greater than 0 due to limitations of the base class library (.NET Framework) and static validation. However, you can tell the static controller that you are assuming the fact is true. This is how you solve all such problems with contracts with base class libraries or with instructions that a static validator cannot prove.

 public int CountOfItems { get { int count = this.someEnumerable.Count(); Contract.Assume(count > 0); return count; } } 

Answer 2

I think you cannot prove it in statics.
Enumerable.Count<TSource> extension method does not define a contract about its return value (for example, what should this method return for an infinite sequence?).

So CC stais checker warns you about this.

Answer 3

Suppose your code is correct. It works, and you're just trying to get a code contract system to recognize this fact.

This means that calling CountOfItems on an instance of MyObject will always return a value greater than zero. It will not throw an exception, and it will not return a value equal to zero or less.

This means that someEnumerable will be assigned to some object, and someEnumerable.Count() will always return a value greater than zero for any object. These facts will be valid at all times (since there are no restrictions on when CountOfItems can be called.

This means that there is an invariant object (regardless of whether it is explicitly specified in the code or not) for MyObject , which includes these facts. And since your code is correct (by assumption), the MyObject implementation ensures that someEnumerable assigned, and its counter is always greater than zero.

Thus, in order to satisfy the contract for CountOfItems , the contract system must be aware of these invariants and how they are provided.

Answer 4

It seems that adding the ContractInvariant method to the implementation resolves the warning.