Design by Contract in C# and Java

A Microsoft labs project called Spec# has developed a pre-compiler for C# that supports the design-by-contract feature of Eiffel, and adds the capability of the C/C++ "const" keyword. Interestingly, the same post highlights a 3 year old project I wasn't aware of called iContract that provides similar features for Java.

A little background: 12 years ago (back when Bertrand Meyer was the god of Object-Orientation, when Bjarne Stroustrup was at best the regent to the OO throne, and Java was an inkling in James Gosling's eye ;) I sampled but never seriously used the Eiffel language with it's unique focus on design by contract. Eiffel syntax directly allows the constraints or contract of a method to be expressed in a literate natural style within the implementation code. At first glance, the pre-conditions ("require" keyword), post-conditions ("ensure") and invariants ("invariant") seem like they are analogues of C's "assert.h" or even Java assertions, but they are an advance in two main ways:

• they automatically appear in the documentation, which helps the caller of a method to know what they should provide (pre-conditions) what they can expect to happen (post-conditions), and what should not go wrong (invariants)
• critically, the contract expressed in a base class is inherited and enforced for sub-classes

All of these constraints can be removed from the compiled code; Java has one important advantage here in that the assertions can be enabled or disabled at runtime.

So Spec# and iContract have similar features. Where they differ is in maturity (iContract has been around since 2001) and in syntax:

• Spec# essentially uses the Eiffel syntax, but it adds some sugar in the form of the "!" beside the name of a method parameter which asserts (or "require"s) that the parameter may not be null.
• iContract uses javadoc extensions

The advantage of iContract's use of javadoc comments is that the constraints are naturally ignored by a regular compiler. This is nice as you can adopt design-by-contract on a specific sub-project without changing the build environment for any container project. It also means they can be easily included in the javadoc-generated documentation, or used as part of a compile-time step to add the assertions into the output code. Here's a quick sample for the sqrt() method (note the use of "return" to enable the method's return value to be part of a post-condition):

/**
* @pre f >= 0.0
* @post Math.abs((return * return) - f) < 0.001
*/ 

So iContract looks like it's worth trying. If you want a blast of nostalgia, you can program in Eiffel and target the JRE - the SmartEiffel project includes a compiler for Java bytecode. I haven't looked at it too closely, but if it allows you to use Java API's from Eiffel, it could be worth looking at.

(2004-11-17 09:02:50.0) Permalink