Should I execute Contract.Ensures for any method result?

Question

Say I have this:

[Pure] public static TimeSpan Seconds(this int i) { Contract.Ensures(Contract.Result<TimeSpan>() == TimeSpan.FromSeconds(i)); return TimeSpan.FromSeconds(i); } 

Do I guarantee that the result of the contract will be so strict, or is it not mandatory?

---

And in this case?

 [Pure] public static T IfTrue<T>(this bool b, T value) { Contract.Ensures(Contract.Result<T>().Equals(b ? value : default(T))); return b ? value : default(T); } 

---

My questions:

• Am I right when I point to an exact contract?
• Should I make such strict contracts and why?
• Is it okay that my contract guarantee repeats (in many cases in my application) the return ?

Answer 1

Think of the word "Contract" - that you, having written your code, want to guarantee your subscribers (or for Requires , that you want them to guarantee you).

For trivial examples, such as the ones you showed, I cannot think of what you would like to include as a contract. Perhaps for the first, I would go for:

 [Pure] public static TimeSpan Seconds(this int i) { Contract.Requires(i>0); Contract.Ensures(Contract.Result<TimeSpan>().TotalSeconds > 0.0); return TimeSpan.FromSeconds(i); } 

I guarantee my subscribers that I will get a positive result. Obviously, such a contract could be given if it included more complex mathematics in this method. I will give guarantees on the range, but I will not determine exactly how the result is calculated (since this can be changed).

Answer 2

The purity of the method means that the method call does not cause visible side effects of the calling object in the state of the object. All this.

Of course, a pure method may be publicly available and may define its own preconditions and post-conditions. It depends on the specific use cases of the method.