Spec# Puts an End to Null Reference Exceptions

Posted by Jonathan Allen on Apr 18, 2007

Sections

Development,

Architecture & Design

Topics

Programming ,

.NET

Tags

Spec#

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.

1. Back to top

   Besides, you can use it for model-based testing, too

   by Torreborre Eric

   Have a look at the following pdf:
   
   research.microsoft.com/research/pubs/view.aspx?...

   Reply

2. Back to top

   Sigh

   by Eirik Mangseth

   Why can't they just use Eiffel instead? Design By Contract was pioneered by Dr. Bertrand Meyer and implemented in Eiffel right from the start.
   
   Eirik M.
   
   "If I can't Eiffel in heaven, I won't go"

   Reply

3. Back to top

   Re: Sigh

   by Jonathan Allen

   From what I can tell, one of the goals is to improve C#.
   
   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#.

   Reply

4. Back to top

   Re: Sigh

   by Stefan Wenig

   why doesn't everyone see how stupid their tools are and use <insert your favorite technology here> ;-)
   
   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.

   Reply

5. Back to top

   Re: Sigh

   by Stefan Wenig

   i think they just want to provide the features they think programmers should have in a language that fits perfectly with .net. integration of existing languages into the CLR often works surprisingly well, eiffel is a good example for this (and it'll be interesting to see how far the dynamic language runtime is going to push that - watch MIX 07...)
   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.

   Reply

6. Back to top

   Re: Sigh

   by johan eijlders

   Then you don't go. Microsoft bought it.

   Reply

• Older >