Can I execute Contract.Ensures on IQueryable and IEnumerable?

Question

Let's look at this code:

public IQueryable<Category> GetAllActive() { Contract.Ensures(Contract.Result<IQueryable<Category>>() != null); return dataSource.GetCategories(T => T.IsActive); } 

There is a small question. Everything is fine with code contracts writing this:

 public IQueryable<Category> GetAllActive() { Contract.Ensures(Contract.Result<IQueryable<Category>>() != null); Contract.Ensures(Contract.Result<IQueryable<Category>>().All(T => T.IsActive)); return dataSource.GetCategories(T => T.IsActive); } 

Or no?

Will such a thing produce unnecessary sequence numbering, which is highly undesirable?

Answer 1

Assuming you are using a binary rewriter and applying contracts at runtime, you should not do this.

When you use Contract.Ensures like this:

 Contract.Ensures(Contract.Result<T>() <operation>); return expression; 

It is transformed, and the operation is removed in the following:

 T expression = <expression>; // Perform checks on expression. if (!(expression <operation>) <throw appropriate exception>; // Return value. return expression; 

In this case, this means your code is being disabled:

 IQueryable<Category> temp = dataSource.GetCategories(T => T.IsActive); // Perform checks. if (!(temp != null)) throw new Exception(); if (!temp.All(T => T.IsActive)) throw new Exception(); // Return values. return temp; 

In this case, your IQueryable<Category> will be passed through and will lead to sending another request to the underlying data store.

Depending on the operation, you may not notice it, but the request will definitely be executed twice, which is bad for performance.

For things of this nature, you should check at the IQueryable<T> consumption point if you have any elements (you can do this with a boolean flag that is specified as foreach through it, or when you materialize it).

However, if you do not use a binary rewriting file on your compiled assemblies, Contract.Result<T> contracts of this nature cannot be respected; in this case, it is noop and probably should not be there, as it does nothing.