Extreme Code Contracts

Design by Contract is a code quality construct familiar to Eiffel programmers as it forms an essential part of that language. It is a way to annotate programs with properties that must hold. These properties come in three groups: 1) Preconditions, the properties that a method require be true, 2) Postconditions, the properties a method ensures hold on exit and class invariants, properties which must hold between method calls. Together these these form Design by Contract, a strong formalism to enhance software quality by spreading out a finely masked web across the entire codebase.

One may see Design by Contract as a contract between the method caller and the callee: if the caller promises such and such then the callee will ensure such and such (division: “if you give me numbers a and b such that b is not equal to zero, then I promise to give you a divided by b”.) Another trivial example could be a function which maps from indices to values, for example an array lookup. One common requirement for such a function is that the index be non-negative*. If the language and libraries do not have a “native” non-negative number type, the function will only work across a part of its domain – it will not accept all integers. In effect the function can be seen as a partial function.

Design by Contract can therefore be seen as a way to specify the part of the domain, and range, that the function applies. It’s almost as if the function becomes total again because the contracts narrow the domain and range of functions declaratively as if new types were defined. Contracts can often be disabled in release builds such that there is no performance footprint when testing is done. Another interesting thing about contracts is that there is static verification software also known as theorem provers that is able to reason statically about the code and to form proofs. A failed proof could be that a function is called somewhere with a negative number (to use our example above). This would represent a bug in the software. To be able to find bugs statically is incredibly powerful and useful of course.

It is therefore very nice to see Design by Contract arrive in .Net in 2010. The way that it has arrived is not quite as nice as in Eiffel for example because in .Net it is a library and tool feature rather than a language feature. Eiffel has special syntactic support for preconditions, postconditions and invariants that make expressing them very elegant. To support Design by Contract, or Code Contracts as they’re called in .Net,  Microsoft invented a clever piece of software identifies calls to Contract.Requires, Contract.Ensures, etc. in the CLR Intermediate Language and rewrites these (either stripping them out or extending them for inheritance, for example).  I’m not intimately familar with how exactly the rewriter works but on an abstract level it is something of that nature.

It also looks as if Microsoft will not make full verification software available for free but run-time checks in debug builds is fine with me.

Now to the “Extreme” part of “Extreme Code Contracts”. I’ve been playing with Code Contracts for my Extensia Codeplex project and aggressively adding code contracts everywhere.  As an example, I have some new “bit fiddling” extension methods that allow easy manipulation of the bits of unsigned 8-bit integers (bytes) and unsigned 32-bit integers (uints).

I think the example I’ve concocted is very nice: it uses a declarative LINQ to Objects query as part of the code contract for the method.

The actual implementation here is by no means optimal in terms of performance but it does have a certain elegance to it. The most important criterion is correctness though. Something I think the contract will help maintain over time as the different algorithms are optimized and changed. I haven’t installed the code contracts verification software yet as I don’t know whether it will work with Visual Studio 2010 which is what I’m using but if it does it will be fun to see how many bugs it finds.

The subexpression value.Information() actually builds an enumeration of bits, which can be queried with LINQ; a further call to Reverse() then reverses the order of bits and at last the call ToUint() converts the bits back to a new uint value. This is a pretty abstract way of dealing with binary data, one that allows very high-level and easy manipulation of bits.

Have fun and do use and give feedback on Extensia if you like.

* I seem to remember that in Eiffel indices often start at 1 which mean that they neatly map to natural numbers. There is indeed also a native natural number type in Eiffel base.

Advertisements

About xosfaere

Software Developer
This entry was posted in Computer Science, Declarative, Imperative, Paradigm, Program, Software, Technical and tagged , , , , , , , , , , , , . Bookmark the permalink.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s