Code Contracts - should private methods be checked for pre and post conditions?

Question

I am trying to get up to speed on Code Contracts. I like the concept, but in practice, I don't see the value of adding Contract.Requires on numerous private methods, some of which are only a line or two long.

I can see the point on Public methods, but on private class methods, it seems like overkill.

Answer 1

The main reason you'd want to apply contracts to private methods is if you're taking advantage of static analysis. You will often write code that makes implicit assumptions about your private methods (this method never returns null, for instance) and the static prover will point this out to you. You can then either put the assumption in the body of your public method or you can add it as a contract on the private method. The latter is generally cleaner, as it allows you to reuse the assumption implied by contract throughout multiple uses of that private method.

Personally, I've given up on Code Contracts until it gets a chance to mature some more. The syntax is awkward (we really need a simple representation for non-nullable parameters in particular) and you can go through a lot of gyrations trying to make complicated systems statically prove. It's a very good idea, though and I think it's only a matter of time until proper contract support for sophisticated static analysis is baked into .NET (actual CIL metadata), with native language support in C#, rather than bolted on as an awkward extension.

One other aside is that I think it's very valuable to go through the process of applying contracts to a small application, from top to bottom, including private and public methods. As you work through the process of making everything prove, it reveals a lot of the implicit assumptions you make every day without even realizing it. You also often discover failure cases you'd never considered, as the mindset you cultivate when designing contracts highlights the points where you're making assumptions and encourages you to consider whether your assumptions may sometimes be violated. I don't have the schedule time to do this on my day-to-day jobs, but I definitely learned a lot from the period where I did experiment with Code Contracts.

Answer 2

Contracts are usually only checked before/after public methods. Private methods are only called as part of a call to a public method, so they need not be checked separately.

http://en.wikipedia.org/wiki/Class_invariant