B# .NET Blog

Introduction

I've been blogging about the Comega language on my blog earlier (and will continue to do so in the near future), which is a superset of the C# language that focuses primarily on object/relational/hierarchical data manipulation and mapping on the one hand and concurrency language extensions on the other hand. Part of the features of Comega are already available in C# 2.0 (e.g. the yield statement, anonymous delegates and more deeply closures).

In this post I'm introducing you to another Microsoft Research project called Spec#, which is a superset of the C# language too. The idea of Spec# is to introduce the concept of pre-conditions, post-conditions and object invariants in the code (much like Eiffel does). More information can be found on:

• Microsoft Research homepage for Spec#
• MSDN Webcast about Spec# by Mike Barnett

Today's software is typically of a large complexity and therefore a specification of the software is needed in order to be successful. However, specifications are far too often words or diagrams and are not reflected in a clear way in the code of the application itself. Of course, there are approaches today that can assist to bring clearness to a software development project, using UML tools or even unit testing which can serve as a kind of minor specification of the software. Spec# however introduces specification declarations and enforcement inside the code itself, making the code more robust and self-describing.

Generally spoken, Spec# focuses on four fields:

• non-null types
• enhanced exception support
• pre- and post-conditions
• object invariants

I'll cover these in the rest of this post in somewhat more detail. Just to wrap up the introduction, let's stress on the fact that Spec# is a superset of the C# language and therefore any valid C# application should compile in Spec# too (if there are no conflicts with the new keywords introduced in Spec#).

To summarize Spec# in three words, remember these: "Design by contract"

How to start?

Go to the MSR homepage for Spec# and download the Visual Studio .NET 2003 or Visual Studio 2005 plug-in to support the Spec# language inside the VS IDE. When you start VS after the installation of Spec# a new set of project types should appear in the list. Spec# projects have an extension of .sscproj and the code files have an .ssc extension. Included with the Spec# package are some samples which are also accessible through the New Project dialog window in VS.

Non-null types

One classic problem that occurs in a lot of applications is the possiblity that a reference type variable is null. In such a case, it's not valid to access or call members of the variable through the dot (.) operator. Assume you have a class like the following:

class A
{
   B b;

   public A(B b)
   {
      this.b = b;
   }

   public int C()
   {
      return b.D(); //what if b == null?
   }
}

When you try to compile this in Spec#, you'll get a warning by the Spec# compiler, telling there is a "possible null dereference" on the line return b.D();. Adding code like

if (b != null) { ... }

will make the warning disappear for the guarded statements (that is, the block that is protected by the null-check). Another way to "solve" the problem is to throw an exception:

if (b == null) throw new NullArgumentException();

However, Spec# allows you to enforce the "non-nullness" of a variable by using a precondition (will cover this in more detail later). The basic code looks like this:

   public A(B b)
   requires b != null;
   {
      this.b = b;
   }

An alternative syntax in Spec# is the use of the "bang" symbol (!) as an annotation for a declaration, as follows:

   B! b;

   public A(B! b)
   {
      this.b = b;
   }

which means "it should never be possible to get null in this variable". The runtime will guarantee against exceptions by enforcing the preconditions for you, by having the compiler add additional statements to ensure this and by generating compile-time errors ("unsatified requires ...").

Let's show a far more extensive and concrete sample. Go to the Spec# command line and create a file called test.ssc in which you paste the following code:

using System;

class Test
{
   public static void Main()
   {
      Do("test");
   }

   private static void Do(string s)
   {
      Console.WriteLine(s.Length);
   }
}

When compiling this using ssc.exe test.ssc, you'll get the following warning:

C:\temp\specsharp\test>ssc test.ssc
test.ssc(12,19): warning CS2614: Receiver might be null

Which obviously is true. However, when you run the application, you'll get a correct result of course:

C:\temp\specsharp\test>test
4

Now, change the code as follows:

using System;

class Test
{
   public static void Main()
   {
      Do(null);
   }

   private static void Do(string s)
   {
      Console.WriteLine(s.Length);
   }
}

When you do compile, you'll still get the same warning message, but when you run an exception is thrown.

C:\temp\specsharp\test>ssc test.ssc
test.ssc(12,25): warning CS2614: Receiver might be null

C:\temp\specsharp\test>test

Unhandled Exception: System.NullReferenceException: Object reference not set to
an instance of an object.
   at System.String.get_Length()
   at Test.Main()

Nothing special at first sight, C# has the same behavior at runtime except for the compile-time warning about a "possibly null value".

Now, change the code as follows:

using System;

class Test
{
   public static void Main()
   {
      Do("test");
   }

   private static void Do(string! s)
   {
      Console.WriteLine(s.Length);
   }
}

And compile. All warnings are gone now and running the application goes well, as we expect. However, when you change the code like this:

using System;

class Test
{
   public static void Main()
   {
      Do(null);
   }

   private static void Do(string! s)
   {
      Console.WriteLine(s.Length);
   }
}

The compiler tells us were making a mistake against the contract of the target method Do: a non-null value is expected.

C:\temp\specsharp\test>ssc test.ssc
test.ssc(7,10): warning CS2612: Null cannot be used where a non-null value is expected

Now, how does Spec# enforce this not-null requirement at runtime? The answer can be found using ildasm.exe. The Do method itself does not contain something special, exception for the method header:

.method private hidebysig static void  Do(string modopt([System.Compiler.Runtime]Microsoft.Contracts.NonNullType) s) cil managed
{
  // Code size       12 (0xc)
  .maxstack  8
  IL_0000:  ldarg.0
  IL_0001:  call       instance int32 [mscorlib]System.String::get_Length()
  IL_0006:  call       void [mscorlib]System.Console::WriteLine(int32)
  IL_000b:  ret
} // end of method Test::Do

This indicates the Spec# compiler to insert not-null enforcement code before calling the Do method. When you take a look at Main, you can see the result of this:

.method public hidebysig static void  Main() cil managed
{
  .entrypoint
  // Code size       17 (0x11)
  .maxstack  8
  IL_0000:  ldnull
  IL_0001:  call       object [System.Compiler.Runtime]Microsoft.Contracts.NonNullType::IsNonNull(object)
  IL_0006:  castclass  string modopt([System.Compiler.Runtime]Microsoft.Contracts.NonNullType)
  IL_000b:  call       void Test::Do(string modopt([System.Compiler.Runtime]Microsoft.Contracts.NonNullType))
  IL_0010:  ret
} // end of method Test::Main

As the matter in fact, what I've shown you is pretty straightforward. There are however more complicated cases where the use of a non-null type system is not as simple as this. Consider for example this:

class B : A
{
   C! c;

   public B(...) : base(...)
   {
      c = ...;
   }
}

In here, c needs to be not null. But when the constructor is being executed, c is temporarily null because of the first call to the base constructor which doesn't know about the existence of c. This clearly is a violation against the type safety of Spec#'s non-null type system. For this very reason, Spec# allows this:

class B : A
{
   C! c;

   public B(...) : c(...), base(...)
   {
   }
}

Which is derived from the C++ syntax. However, the base constructor call is happening after field initialization statements now. For every not-null field, such an initializer is needed in order to be able to guarantee type safety. Spec# allows the use of non-null types for local variables, class attributes, parameters and return types but not for elements inside an array (the array itself can be declared as non-null though).

<PermissionToRead Groups="Geeks">

You might wonder why we need to be able to do stuff before calling the base class constructor when using non-null types in a class hierarchy. Well, the answer is the following. Assume you have some base class A that looks like this:

abstract class A
{
   public A()
   {
      Init();
   }

   public abstract void Init();
}

Okay for now. Now let's create a subclass of A, call it B:

class B : A
{
   C! c; //non-null value of type C

   public B(C! c) : base()
   {
      this.c = c;
   }

   public override void Init()
   {
      c.DoSomething();
   }
}

You thought this is type safe? Well, it isn't. Track down the execution path for "new B(some_c)". First we do initialize A because of the base() call (which needs to be the first call in a subtype's constructor in C#). Inside the constructor of A, we do call the abstract method Init, so we end up in B::Init. Over there, c is used to call DoSomething, but c isn't initialized. Crash boom bang :-). This is why we need to be able to defer the base constructor call to a later point and why non-null values need to be initialized upfront, before calling base(). Note that this is only valid in Spec#. C# simply doesn't allow deferred base() constructor calls. A sample looks like this:

   public B(C! c)
   {
      this.c = c;
      base();
   }

</PermissionToRead>

Preconditions

As mentioned in the introduction, Spec# is all about design by contract. One crucial aspect of this are so-called "method contracts". In such as contract, the developer specifies a contract between the caller and the implementation of a method, a constructor, a property or an indexer (which are in the end all translated to methods in IL). Spec# focuses on different fields to accomplish this, including preconditions (in which state can the method be called?), postconditions (in which state is the method allowed to return?), extended exception handling mechanisms (see further), frame conditions (see further).

Let's kick off with preconditions. In the previous sample, I already did show a precondition through the ! syntax and using the "requires" keyword. However, these predconditions can take far more complex forms:

public void AssignToPos(int pos, string! val)
requires 0 <= pos && pos < max;
requires string != "";
{ ... }

and you can have more than one requires statement as you can see. However, the Base Class Library does not contain this kind of contracts today. Examples of where this might be useful include the Array class, where bound checking is important (e.g. Array.Copy). In order to support this kind of scenarios, Spec# ships with an assembly Mscorlib.Contracts that contains this kind of checks on the BCL classes. Therefore, wrong calls to e.g. Array.Copy will result in compile-time warnings.

Spec# realizes this very powerful program verification system to validate preconditions using a built-in theorem prover, which is fed by information from the code.

Let's show some examples, starting with a pretty simple one first. Assume we want to count the number of occurrences of a certain value in an array, let's say an array of ints for simplicity's sake. Consider the following piece of code. Just past it into a Notepad and try to find the first compiler warning you should get without running ssc.exe:

using System;

class Test2
{
   public static void Main()
   {
      Console.WriteLine(Do (new int[] {1,2,3,4,2,3,4,3,4,4}, 2));
   }

   private static int Do(int[] array, int val)
   {
      int n = 0;
      for (int i = 0; i < array.Length; i++)
         if (array[i] == val) n++;
      return n;
   }
}

Got it? Indeed, array.Length will cause a warning to be generated about the possibility for array to be null. So, you should change the code as follows:

using System;

class Test2
{
   public static void Main()
   {
      Console.WriteLine(Do (new int[] {1,2,3,4,2,3,4,3,4,4}, 2));
   }

   private static int Do(int[]! array, int val)
   {
      int n = 0;
      for (int i = 0; i < array.Length; i++)
         if (array[i] == val) n++;
      return n;
   }
}

Nothing new yet. Now, let's say we only want to search some region of the array by specifying bounds in the Do method's parameter list.

using System;

class Test2
{
   public static void Main()
   {
      Console.WriteLine(Do (new int[] {1,2,3,4,2,3,4,3,4,4}, 2, 1, 5));
   }

   private static int Do(int[]! array, int val, int from, int to)
   {
      int n = 0;
      for (int i = from; i < to; i++)
         if (array[i] == val) n++;
      return n;
   }
}

This will certainly fail with an IndexOutOfRangeException if the specified values for the third and fourth parameter are invalid. So, Spec# allows us to specify some conditions:

using System;

class Test2
{
   public static void Main()
   {
      Console.WriteLine(Do (new int[] {1,2,3,4,2,3,4,3,4,4}, 2, 1, 5));
   }

   private static int Do(int[]! array, int val, int from, int to)
   requires to >= 0;
   requires from >= 0 && from < array.Length;
   {
      int n = 0;
      for (int i = from; i < to; i++)
         if (array[i] == val) n++;
      return n;
   }
}

Now, when you run this code but with a call to Do with the following arguments:

      Console.WriteLine(Do (new int[] {1,2,3,4,2,3,4,3,4,4}, 2, -1, 20));

You should get something like this:

C:\temp\specsharp\test>test2

Unhandled Exception: Microsoft.Contracts.RequiresException: Precondition violated from method 'Test2.Do(optional(Microsoft.Contracts.NonNullType) System.Int32[],System.Int32,System.Int32,System.Int32)'
   at Test2.Do(Int32[] array, Int32 val, Int32 from, Int32 to)
   at Test2.Main()

Hey, no IndexOutOfRangeException? Instead, we get an exception of the type Microsoft.Contracts.RequiresException. What's going on in the IL code? Let's take a look at Do's IL (personal comments in green):

.method private hidebysig static int32  Do(int32[] modopt([System.Compiler.Runtime]Microsoft.Contracts.NonNullType) 'array',
                                           int32 val,
                                           int32 from,
                                           int32 'to') cil managed
{
  .custom instance void [System.Compiler.Runtime]Microsoft.Contracts.RequiresAttribute::.ctor(string) = ( 01 00 13 3A 3A 3E 3D 28 69 33 32 2C 69 33 32 29   // ...::>=(i32,i32)
                                                                                                          7B 24 33 2C 30 7D 06 00 53 0E 08 46 69 6C 65 6E   // {$3,0}..S..Filen
                                                                                                          61 6D 65 20 43 3A 5C 74 65 6D 70 5C 73 70 65 63   // ame C:\temp\spec
                                                                                                          73 68 61 72 70 5C 74 65 73 74 5C 74 65 73 74 32   // sharp\test\test2
                                                                                                          2E 73 73 63 53 08 09 53 74 61 72 74 4C 69 6E 65   // .sscS..StartLine
                                                                                                          0B 00 00 00 53 08 0B 53 74 61 72 74 43 6F 6C 75   // ....S..StartColu
                                                                                                          6D 6E 0D 00 00 00 53 08 07 45 6E 64 4C 69 6E 65   // mn....S..EndLine
                                                                                                          0B 00 00 00 53 08 09 45 6E 64 43 6F 6C 75 6D 6E   // ....S..EndColumn
                                                                                                          14 00 00 00 53 0E 0A 53 6F 75 72 63 65 54 65 78   // ....S..SourceTex
                                                                                                          74 11 72 65 71 75 69 72 65 73 20 74 6F 20 3E 3D   // t.requires to >=
                                                                                                          20 30 3B )                                        //  0;
  .custom instance void [System.Compiler.Runtime]Microsoft.Contracts.RequiresAttribute::.ctor(string) = ( 01 00 5F 3A 3A 26 26 28 62 6F 6F 6C 2C 62 6F 6F   // .._::&&(bool,boo
                                                                                                          6C 29 7B 3A 3A 3E 3D 28 69 33 32 2C 69 33 32 29   // l){::>=(i32,i32)
                                                                                                          7B 24 32 2C 30 7D 2C 3A 3A 3C 28 69 33 32 2C 69   // {$2,0},::<(i32,i
                                                                                                          33 32 29 7B 24 32 2C 24 30 40 5B 6D 73 63 6F 72   // 32){$2,$0@[mscor
                                                                                                          6C 69 62 5D 53 79 73 74 65 6D 2E 41 72 72 61 79   // lib]System.Array
                                                                                                          3A 3A 67 65 74 5F 4C 65 6E 67 74 68 28 29 7B 7D   // ::get_Length(){}
                                                                                                          7D 7D 06 00 53 0E 08 46 69 6C 65 6E 61 6D 65 20   // }}..S..Filename
                                                                                                          43 3A 5C 74 65 6D 70 5C 73 70 65 63 73 68 61 72   // C:\temp\specshar
                                                                                                          70 5C 74 65 73 74 5C 74 65 73 74 32 2E 73 73 63   // p\test\test2.ssc
                                                                                                          53 08 09 53 74 61 72 74 4C 69 6E 65 0C 00 00 00   // S..StartLine....
                                                                                                          53 08 0B 53 74 61 72 74 43 6F 6C 75 6D 6E 0D 00   // S..StartColumn..
                                                                                                          00 00 53 08 07 45 6E 64 4C 69 6E 65 0C 00 00 00   // ..S..EndLine....
                                                                                                          53 08 09 45 6E 64 43 6F 6C 75 6D 6E 2D 00 00 00   // S..EndColumn-...
                                                                                                          53 0E 0A 53 6F 75 72 63 65 54 65 78 74 2A 72 65   // S..SourceText*re
                                                                                                          71 75 69 72 65 73 20 66 72 6F 6D 20 3E 3D 20 30   // quires from >= 0
                                                                                                          20 26 26 20 66 72 6F 6D 20 3C 20 61 72 72 61 79   //  && from < array
                                                                                                          2E 4C 65 6E 67 74 68 3B )                         // .Length;
  // Code size       218 (0xda)
  .maxstack  6
  .locals init (class [mscorlib]System.Exception V_0,
           object V_1,
           class [mscorlib]System.Exception V_2,
           object V_3,
           class [System.Compiler.Runtime]Microsoft.Contracts.ContractMarkerException V_4,
           int32 V_5,
           int32 V_6,
           int32 V_7,
           int32 V_8,
           int32 V_9,
           int32 V_10)
  .try
  {
    .try
    {
      IL_0000:  ldarg.3             //parameter to
      IL_0001:  ldc.i4.0            //0
      IL_0002:  blt        IL_000c  //requires to >= 0
      IL_0007:  leave      IL_003f
      IL_000c:  leave      IL_0034  //check not valid, leave .try block and jump to IL_0034 to throw exception
    }  // end .try
    catch [mscorlib]System.Exception
    {
      IL_0011:  stloc.0
      IL_0012:  ldstr      "Exception occurred during evaluation of preconditi"
      + "on in method 'Test2.Do(optional(Microsoft.Contracts.NonNullType) System"
      + ".Int32[],System.Int32,System.Int32,System.Int32)'"
      IL_0017:  ldloc.0
      IL_0018:  newobj     instance void [System.Compiler.Runtime]Microsoft.Contracts.InvalidContractException::.ctor(string,
                                                                                                                      class [mscorlib]System.Exception)
      IL_001d:  throw
      IL_001e:  leave      IL_0034
    }  // end handler
    catch [mscorlib]System.Object
    {
      IL_0023:  stloc.1
      IL_0024:  ldstr      "Exception occurred during evaluation of preconditi"
      + "on in method 'Test2.Do(optional(Microsoft.Contracts.NonNullType) System"
      + ".Int32[],System.Int32,System.Int32,System.Int32)'"
      IL_0029:  newobj     instance void [System.Compiler.Runtime]Microsoft.Contracts.InvalidContractException::.ctor(string)
      IL_002e:  throw
      IL_002f:  leave      IL_0034
    }  // end handler
    IL_0034:  ldstr      "Precondition violated from method 'Test2.Do(option"
    + "al(Microsoft.Contracts.NonNullType) System.Int32[],System.Int32,System."
    + "Int32,System.Int32)'"
    IL_0039:  newobj     instance void [System.Compiler.Runtime]Microsoft.Contracts.RequiresException::.ctor(string)
    IL_003e:  throw
    IL_003f:  nop
    .try
    {
      IL_0040:  ldarg.2                                                         //parameter from
      IL_0041:  ldc.i4.0                                                        //0
      IL_0042:  blt        IL_0058                                              //requires from >= 0 --> on failure goto IL_0058 to throw exception
      IL_0047:  ldarg.2                                                         //parameter from
      IL_0048:  ldarg.0                                                         //parameter array
      IL_0049:  call       instance int32 [mscorlib]System.Array::get_Length()  //find the length of the array (first variable on stack is passed as argument to get_Length)
      IL_004e:  bge        IL_0058                                              //requires from < array.Length
      IL_0053:  leave      IL_008b
      IL_0058:  leave      IL_0080                                              //check not valid, leave .try block and jump to IL_0034 to throw exception
    }  // end .try
    catch [mscorlib]System.Exception
    {
      IL_005d:  stloc.2
      IL_005e:  ldstr      "Exception occurred during evaluation of preconditi"
      + "on in method 'Test2.Do(optional(Microsoft.Contracts.NonNullType) System"
      + ".Int32[],System.Int32,System.Int32,System.Int32)'"
      IL_0063:  ldloc.2
      IL_0064:  newobj     instance void [System.Compiler.Runtime]Microsoft.Contracts.InvalidContractException::.ctor(string,
                                                                                                                      class [mscorlib]System.Exception)
      IL_0069:  throw
      IL_006a:  leave      IL_0080
    }  // end handler
    catch [mscorlib]System.Object
    {
      IL_006f:  stloc.3
      IL_0070:  ldstr      "Exception occurred during evaluation of preconditi"
      + "on in method 'Test2.Do(optional(Microsoft.Contracts.NonNullType) System"
      + ".Int32[],System.Int32,System.Int32,System.Int32)'"
      IL_0075:  newobj     instance void [System.Compiler.Runtime]Microsoft.Contracts.InvalidContractException::.ctor(string)
      IL_007a:  throw
      IL_007b:  leave      IL_0080
    }  // end handler
    IL_0080:  ldstr      "Precondition violated from method 'Test2.Do(option"
    + "al(Microsoft.Contracts.NonNullType) System.Int32[],System.Int32,System."
    + "Int32,System.Int32)'"
    IL_0085:  newobj     instance void [System.Compiler.Runtime]Microsoft.Contracts.RequiresException::.ctor(string)
    IL_008a:  throw
    IL_008b:  nop
    IL_008c:  leave      IL_0095
  }  // end .try
  catch [System.Compiler.Runtime]Microsoft.Contracts.ContractMarkerException
  {
    IL_0091:  stloc.s    V_4
    IL_0093:  rethrow
  }  // end handler
  IL_0095:  nop
  IL_0096:  ldc.i4.0
  IL_0097:  stloc.s    V_5
  IL_0099:  ldarg.2
  IL_009a:  stloc.s    V_6
  IL_009c:  ldloc.s    V_6
  IL_009e:  ldarg.3
  IL_009f:  bge        IL_00ca
  IL_00a4:  ldarg.0
  IL_00a5:  ldloc.s    V_6
  IL_00a7:  ldelem.i4
  IL_00a8:  ldarg.1
  IL_00a9:  bne.un     IL_00bb
  IL_00ae:  ldloc.s    V_5
  IL_00b0:  stloc.s    V_7
  IL_00b2:  ldloc.s    V_7
  IL_00b4:  ldc.i4.1
  IL_00b5:  add
  IL_00b6:  stloc.s    V_5
  IL_00b8:  ldloc.s    V_7
  IL_00ba:  pop
  IL_00bb:  ldloc.s    V_6
  IL_00bd:  stloc.s    V_8
  IL_00bf:  ldloc.s    V_8
  IL_00c1:  ldc.i4.1
  IL_00c2:  add
  IL_00c3:  stloc.s    V_6
  IL_00c5:  ldloc.s    V_8
  IL_00c7:  pop
  IL_00c8:  br.s       IL_009c
  IL_00ca:  ldloc.s    V_5
  IL_00cc:  stloc.s    V_9
  IL_00ce:  br         IL_00d3
  IL_00d3:  ldloc.s    V_9
  IL_00d5:  stloc.s    V_10
  IL_00d7:  ldloc.s    V_9
  IL_00d9:  ret
} // end of method Test2::Do

The orange part of the IL code shown above, contains the preconditions itself as metadata for further reference. Now, what's the big idea of this? We still do get an exception, so what's the benefit? The answer is that Spec# supports program verification at the side of the caller to see whether the contract is fulfilled or not. If not, developers are warned at development time that they're not working conform the contract. The technology to make these checks is called Boogie and comes with Spec# in the boogie.exe executable. More information about how Boogie works can be found on http://research.microsoft.com/~leino/papers/Leino-CASSIS2004.ppt. In order to run Boogie you'll need to install a tool called Simplify, as explained on http://www.research.microsoft.com/specsharp/simplify.htm. Link to the Module-3 source code download: http://www.hpl.hp.com/downloads/crl/jtk/download-simplify.html. Link to the release containing the .exe file: http://www.hpl.hp.com/downloads/crl/jtk/download-escjava.html. The use of Simplify is likely going to change in the future of the project, as mentioned in "The Spec# Programming System: An Overview" (PDF on the Spec# research home page):