Spec# Puts an End to Null Reference Exceptions

Version 1 of Spec# has been released. Spec# in a variant of C# that supports design by contract features such as a non-null type system, pre and post conditions, loop invariants, and object invariants.

Null reference exceptions are probably the most common exception discovered in C#, Java, and VB programs. In an effort to eliminate this class of error, Spec# supports a non-null type system. In this, the compiler guarantees that variables declared with the "!" symbol such as "private Customer! _customer;" will never be null. In order to facilitate this, it allows member variables to be initialized even before base class constructors.

The non-null type system also extends to parameters, local variables, and return values. The one area it does not work in is elements of an array, as it would cause problems with array initialization and C#’s covariant arrays.

Preconditions specify the required state of the object and the parameters being passed in prior to the method being called. For example, a developer can require that a collection is not read-only and that the index being used is valid prior to calling an Insert method via the "requires" clause. Unlike runtime exceptions that are currently being used in C#, Spec# will try to ensure these conditions are met at compile time. An "otherwise" clause can be used to indicate what exception will be thrown if the preconditions cannot be statically checked and are subsequently violated.

Post conditions, specified with the "ensures" clause, make sure that class invariants are not broken and that the return value is within an acceptable range. It has access to the values of the object prior to the method being called so developers can ensure things such as a count variable always being incremented by one. Again, this is statically guaranteed by the compiler.

Spec# uses checked exceptions in a manner similar to Java. The key difference is that post conditions may still be made in the event an exception occurs. In this case, a developer would normally put an ensures clause on a throws clause to make certain changes to state have been properly rolled back.

Something not mentioned is how Spec# handles versioning and inheritance with checked exceptions. In Java, it is often hard to extend a class by adding functionality or subclassing if it means an exception may be thrown that wasn't defined in the base class.

Invariants are like post-conditions, but they apply to all methods in a class. Specified with the "invariant" statement, they ensure that the object is in a "stable" condition at the end of each method call.

Spec# relies heavily of the sort of contracts mentioned above. But since they are not part of the Base Class Library (BCL), Spec# allows for contracts for pre-compiled libraries to be specified in a separate repository that is referenced at compile time.