The manhood test
I came across an obscure and surprisingly interesting article by Cliff Jones [1], about the history of rely-guarantee but with the following extract:
It was perhaps not fully appreciated at the time of [Hoare’s 1969 axiomatic semantics paper] that the roles of pre and post conditions differ in that a pre condition gives permission to a developer to ignore certain possibilities; the onus is on a user to prove that a component will not be initiated in a state that does not satisfy its pre condition. In contrast a post condition is an obligation on the code that is created according to the specification. This Deontic view carries over [to rely-guarantee reasoning].
I use words more proletarian than “deontic”, but this view is exactly what stands behind the concepts of Design by Contract and has been clearly emphasized in all Eiffel literature ever since the first edition of OOSC. It remains, however, misunderstood outside of the Eiffel community; many people confuse Design by Contract with its opposite, defensive programming. The criterion is simple: if you have a precondition to a routine, are you willing entirely to forsake the corresponding checks (conditionals, exceptions…) in the routine body? If not, you may be using the word “contract” as a marketing device, but that’s all. The courage to remove the checks is the true test of adulthood.
The application of Microsoft’s “Code Contracts” mechanism to the .NET libraries fails that test: a precondition may say “buffer not full” or “insertions allowed”, but the code still checks the condition and triggers an exception. The excuse I have heard is that one cannot trust those unwashed developers. But the methodological discipline is lost. Now let me repeat this using clearer terminology: it’s not deontic.
Reference
[1] Cliff Jones: The role of auxiliary variables in the formal development of concurrent programs, in Reflections on the work of C. A. R. Hoare, eds. Jones, Roscoe and Wood, Springer Lecture Notes in Computer Science, 2009, technical report version available here.
Eiffel Software
Home page at ETH
Informatics Europe
LASER summer school
Propulsion Academy
It’s probably a bit unfair, really, to criticise the existing .NET code for applying defensive programming given that these “code contracts” have been added retrospectively to existing code. The design by contract methodology wasn’t in place when that code was written. Or are you referring to some fresh, recently-written .NET code?
Also, I would question whether it would be wise for them to remove those defensive checks yet. Few .NET programmers are using Code Contracts. You have to go to considerable effort to install support for Code Contracts into Visual Studio 2010. I went through this process myself last year; if it weren’t for the fact that I’m a long-term aficionado of design by contract, I probably wouldn’t have gone to the trouble. Unlike Eiffel, those contracts aren’t instantly available to most .NET programmers: you have to go out of your way to find them.
Once Microsoft has put Code Contracts front-and-centre in front of all programmers, as an unavoidable and obvious part of Visual Studio, then I would agree that the time is ripe to remove those defensive checks. But they just aren’t there yet.
Peter — could one argue that if one is applying code contracts in .NET that one ought to also remove the defensive bits as well? I have not added code contracts in .NET, but regardless of visibility and presentation, it seems reasonable that if one adds contracts, one ought to know enough to realize that the defensive parts are logically no longer required.
Interested to know your point of view.
Hi Larry, yes, whenever I’ve used contracts in any language (by whatever means contracts have been retrofitted by me or by someone else onto the language), I remove the defensive bits.
One of the first times I used contracts in a C system (back in 1992, using simple asserts), another developer approached me because a function that I had written was blowing up in a way that was strange to him. He had written a call to that function that violated the function’s precondition. I’m not sure whether he understood my explanation about contracts. Maybe he put some defensive code in.
Fast-fowarding to this century, however, in my experience a lot of developers seem to get the idea of preconditions. The word seems to have spread somehow.