Code chains with call chains?

Question

Basically I look at two different situations:

A method call inside one class:

public class MyClass { public Bar GetDefaultBar(Foo foo) { Contract.Requires(foo != null); return GetSpecificBar(foo, String.Empty); } public Bar GetSpecificBar(Foo foo, string name) { Contract.Requires(foo != null); Contract.Requires(name != null); ... } } 

---

Method invocation in different classes:

 public class MyClass { private MyBarProvider { get; set; } public Bar GetDefaultBar(Foo foo) { Contract.Requires(foo != null); return BarProvider.GetSpecificBar(foo, String.Empty); } //Object-Invariant ensures that MyBarProvider is never null... } public class MyBarProvider { public Bar GetSpecificBar(Foo foo, string name) { Contract.Requires(foo != null); Contract.Requires(name != null); ... } } 

I am wondering if you need to have duplicate contracts for any of these situations? I suppose there might be a way to avoid this in the first example (all within the same class), but not in the second example (different classes). Also, should duplication be avoided or be there?

Answer 1

I assume that the duplication you are talking about is Contract.Requires(foo != null); .

You need to have this line in both methods in both cases. If you did not include it in the calling object, you will receive the message “Unproven required” on the call site because the calling method may pass a null value. If you do not include it in the called party, the call contract will not contain a non-zero requirement, and the contract analyzer will consider foo as a possible null value. This is because another call site will have the right to pass a null value.

EDIT

As Ɖiamond Ǥeeze points out, you can use ContractAbbreviatorAttribute to reuse contract callbacks in a separate method. The attribute is not part of the .NET Framework 4.0, but you can define it yourself. For more information, see Terje Sandstrom's blog post on reconciling code contracts with bugs with FXCop: http://geekswithblogs.net/terje/archive/2010/10/14.aspx