Skip to main content

Impressions of Code Contracts

Embroiled in a few projects right now, but one gave me the chance to explore Microsoft's code contracts a little. I was initially excited about the prospect of contracts when they were first announced, hence my crude API-compatible implementation in Sasa.Contracts which allowed me to prepare my codebases for contracts. I've now had a chance to play with the real thing, so we'll see how it holds up to reality.

Going Above and Beyond

As usual, I decided to push the boundaries and try to prove properties beyond what C# and .NET can do natively via their type systems. One common nuisance on the CLR is that you can't specify a default constructor for value types. While even code contracts can't prevent someone from creating an empty struct value, you can possibly prevent the use of such an empty value:

public struct NonNull<T>
    where T : class
{
    readonly T value;
    public NonNull(T value)
    {
        Contract.Requires(value != null);
        this.value = value;
    }
    public T Value
    {
        get
        {
            Contract.Requires(Value != null);
            return value;
        }
    }
}

We have here a simple class that wraps a nullable reference type. The preconditions specified on the constructor ensure that no NonNull instance can be created with an explicit null value. The only remaining possibility is to create a value via default(NonNull<T>), so contracts haven't bought us much there.

However, check out the precondition on the NonNull.Value property: before you can call the property, you have to ensure the property is itself not null. This ensures that only values of NonNull created via the provided constructor can use any value of NonNull!

Here's the failure that Visual Studio reports when it can't prove that the contracts are statically satisfied:

Code Contract Failure in Visual Studio

Mission accomplished! Through some clever application of preconditions, you can probably ensure all sorts of behavioural properties on objects you couldn't verify before, so this is fertile ground for experimentation and optimization.

No Free Lunch

There's always a downside of course, and in this case it's the long contract check times. Visual Studio has an option to check contracts in the background after a build completes, which helps a little.

Also, there are a few limitations and bugs remaining in the MS's static checker. For instance, according to the docs, invariants declared on structs are supposedly ignored (section 6.6.1), but I discovered this isn't completely true (Microsoft Connect bug reported).

I also found another bug while testing the interface contracts, so caveat emptor!

Still, it's a promising framework and I plan to make use of it where I can to improve the reliability of my code. Sasa v0.9.4 will probably be the last release for .NET 3.5, so subsequent releases will exploit contracts as much as possible. In particular, Sasa.NonNull<T> will finally get a static analysis to ensure that property is respected!

Labels:

Comments

Post a Comment

Popular posts from this blog

async.h - asynchronous, stackless subroutines in C

The async/await idiom is becoming increasingly popular. The first widely used language to include it was C#, and it has now spread into JavaScript and Rust. Now C/C++ programmers don't have to feel left out, because async.h is a header-only library that brings async/await to C! Features: It's 100% portable C. It requires very little state (2 bytes). It's not dependent on an OS. It's a bit simpler to understand than protothreads because the async state is caller-saved rather than callee-saved. #include "async.h" struct async pt; struct timer timer; async example(struct async *pt) { async_begin(pt); while(1) { if(initiate_io()) { timer_start(&timer); await(io_completed() || timer_expired(&timer)); read_data(); } } async_end; } This library is basically a modified version of the idioms found in the Protothreads library by Adam Dunkels, so it's not truly ground bre...
1 comment
Read more

Easy Automatic Differentiation in C#

I've recently been researching optimization and automatic differentiation (AD) , and decided to take a crack at distilling its essence in C#. Note that automatic differentiation (AD) is different than numerical differentiation . Math.NET already provides excellent support for numerical differentiation . C# doesn't seem to have many options for automatic differentiation, consisting mainly of an F# library with an interop layer, or paid libraries . Neither of these are suitable for learning how AD works. So here's a simple C# implementation of AD that relies on only two things: C#'s operator overloading, and arrays to represent the derivatives, which I think makes it pretty easy to understand. It's not particularly efficient, but it's simple! See the "Optimizations" section at the end if you want a very efficient specialization of this technique. What is Automatic Differentiation? Simply put, automatic differentiation is a technique for calcu...
Post a Comment
Read more

Building a Query DSL in C#

I recently built a REST API prototype where one of the endpoints accepted a string representing a filter to apply to a set of results. For instance, for entities with named properties "Foo" and "Bar", a string like "(Foo = 'some string') or (Bar > 99)" would filter out the results where either Bar is less than or equal to 99, or Foo is not "some string". This would translate pretty straightforwardly into a SQL query, but as a masochist I was set on using Google Datastore as the backend, which unfortunately has a limited filtering API : It does not support disjunctions, ie. "OR" clauses. It does not support filtering using inequalities on more than one property. It does not support a not-equal operation. So in this post, I will describe the design which achieves the following goals: A backend-agnostic querying API supporting arbitrary clauses, conjunctions ("AND"), and disjunctions ("OR"). Implemen...
Post a Comment
Read more