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.
Besides, you can use it for model-based testing, too
"If I can't Eiffel in heaven, I won't go"
One option they talked about is an automatic conversion from Spec# to C#, essentially using the former to elimiate bugs and the latter because it is the 'official' language of the BCL.
Another option is to migrate the research done in Spec# over to C# in much the same way research from C-Omega and F# has been ported.
Another problem with Eiffel is that Microsoft Research doesn't own it. This severly limits their ability to alter the language as their research moves in new directions. That said, I would be very surprised to find that Eiffel wasn't a major inspiration for Spec#.
you don't happen to know whether eiffel does the same amount of static contract analysis as spec#? i think that's the most interesting aspect of the research - including runtime checks is not only less useful, but pretty easy to implement too.
but languages designed for the CLR will always have an advantage, however close others may get. for developing .net libraries, that's just not something you can ignore.
the truth is that we need both - integration of other good languages for flexibility, portability and just for the fun of exploring new languages; and native .net languages with great new features.
Mike Amundsen May 29, 2015
Ben Linders May 28, 2015