Tuesday, August 09, 2005 2:11 AM bart

An introduction to Spec#

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:

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):

Currently, Boogie uses the Simplify theorem prover [18], but we intend to switch to a new experimental theorem prover being developed at Microsoft Research.

To install Simplify, go to the Escjava\release\master\bin folder where you unzipped (e.g. using WinRAR) the download of EscJava from HP Labs and copy the Simplify-1.5.1.exe.win file to the bin folder of Spec# (typically located in %programfiles%\Microsoft\Spec#\bin) where you should rename it to Simplify.exe.

Now you can go to the Spec# command prompt and run Boogie against test2.exe:

C:\temp\specsharp\test>boogie test2.exe
Spec# Program Verifier Version 0.6, Copyright (c) 2003-2005, Microsoft.
Call of Test2.Do(int[]! array, int val, int from, int to): unsatisfied requires from >= 0 && from < array.Length;
Array index possibly below lower bound

Spec# Program Verifier finished with 2 errors

Now, go to Visual Studio and create a Spec# project, importing the same code as test2.ssc. You should see the result of verification in there too. Try to mess around with the System.Array class of the BLC too in order to see the contracts included with the Spec# installation (use the arraylist sample project of Spec#, e.g. line 66 or 221).

To make preconditions even more powerful, you can also specify an alternative exception to signal precondition violations at runtime, by means of the otherwise keyword:

<returntype> <methodname>(<paramlist>)
requires <precondition> otherwise <exceptiontype>;
...
{ ... }

Important note for people who know languages such as Ada. Preconditions are not the same as guards on procedures in Ada applications. Ada's guards are focusing on support for concurrency and can queue up the calls to a certain "entry" (till the guard "opens the door"), whileas Spec# is just about checking conditions to ensure execution correctness. If the criteria are not met, the runtime will throw an exception.

 

Postconditions

Where preconditions can be used to make sure an object is in a certain state ready to accept an incoming message for a certain method, postconditions can be seen as guard conditions that are checked when a method returns. Spec#'s postconditions are very powerful, as I'll show you using some samples right now. Let's start with some basic sample:

using System;

class Test3
{
   int i;

   public Test3(int i)
   requires i > 0;
   {
      this.i = i;
   }

   public void Increment()
   ensures I > 0;
   {
      i++;
   }

   public int I
   {
      get
      {
         return i;
      }
   }

   public static void Main()
   {
      Test3 t = new Test3(1);
      t.Increment();

      Console.WriteLine(t.I);
   }
}

In here we define a class called Test3 that accepts an integer valued parameter, that is required to be strictly positive. In the postcondition for the method Increment, we specify that this condition should still hold (I'll come back to this later on, when talking about invariants). When you compile and run this, it should print - as expected - the value 2 to the screen. In the code, notice the use of capital I in the postcondition whileas lower i is used in the precondition. Now, let's take a look at how this is implemented in IL, so jump to ildasm and open up test3.exe's Increment method definition:

.method public hidebysig instance void  Increment() cil managed
{
  .custom instance void [System.Compiler.Runtime]Microsoft.Contracts.EnsuresAttribute::.ctor(string) = ( 01 00 23 3A 3A 3E 28 69 33 32 2C 69 33 32 29 7B   // ..#::>(i32,i32){
                                                                                                         74 68 69 73 40 54 65 73 74 33 3A 3A 67 65 74 5F   //
this@Test3::get_
                                                                                                         49 7B 7D 2C 30 7D 06 00 53 0E 08 46 69 6C 65 6E   // I{},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 33   // sharp\test\test3
                                                                                                         2E 73 73 63 53 08 09 53 74 61 72 74 4C 69 6E 65   // .sscS..StartLine
                                                                                                         0E 00 00 00 53 08 0B 53 74 61 72 74 43 6F 6C 75   // ....S..StartColu
                                                                                                         6D 6E 0C 00 00 00 53 08 07 45 6E 64 4C 69 6E 65   // mn....S..EndLine
                                                                                                         0E 00 00 00 53 08 09 45 6E 64 43 6F 6C 75 6D 6E   // ....S..EndColumn
                                                                                                         11 00 00 00 53 0E 0A 53 6F 75 72 63 65 54 65 78   // ....S..SourceTex
                                                                                                         74 0E 65 6E 73 75 72 65 73 20 49 20 3E 20 30 3B ) // t.ensures I > 0;
  // Code size       97 (0x61)
  .maxstack  8
  .locals init (int32 V_0,
           class [mscorlib]System.Exception V_1,
           object V_2,
           class [System.Compiler.Runtime]Microsoft.Contracts.ContractMarkerException V_3)
  IL_0000:  ldarg.0
  IL_0001:  ldfld      int32 Test3::i
  IL_0006:  stloc.0
  IL_0007:  ldarg.0
  IL_0008:  ldloc.0
  IL_0009:  ldc.i4.1
  IL_000a:  add
  IL_000b:  stfld      int32 Test3::i
  IL_0010:  ldloc.0
  IL_0011:  pop
  .try
  {
    .try
    {
      IL_0012:  ldarg.0
      IL_0013:  call       instance int32 Test3::get_I() //get the (new) I value
      IL_0018:  ldc.i4.0
      IL_0019:  ble        IL_0023                       //check the postcondition ensures I > 0
      IL_001e:  leave      IL_0056
      IL_0023:  leave      IL_004b                       //throw the exception
    }  // end .try
    catch [mscorlib]System.Exception
    {
      IL_0028:  stloc.1
      IL_0029:  ldstr      "Exception occurred during evaluation of postcondit"
      + "ion in method 'Test3.Increment'"
      IL_002e:  ldloc.1
      IL_002f:  newobj     instance void [System.Compiler.Runtime]Microsoft.Contracts.InvalidContractException::.ctor(string,
                                                                                                                      class [mscorlib]System.Exception)
      IL_0034:  throw
      IL_0035:  leave      IL_004b
    }  // end handler
    catch [mscorlib]System.Object
    {
      IL_003a:  stloc.2
      IL_003b:  ldstr      "Exception occurred during evaluation of postcondit"
      + "ion in method 'Test3.Increment'"
      IL_0040:  newobj     instance void [System.Compiler.Runtime]Microsoft.Contracts.InvalidContractException::.ctor(string)
      IL_0045:  throw
      IL_0046:  leave      IL_004b
    }  // end handler
    IL_004b:  ldstr      "Postcondition violated from method 'Test3.Increment'"
    IL_0050:  newobj     instance void [System.Compiler.Runtime]Microsoft.Contracts.EnsuresException::.ctor(string)
    IL_0055:  throw
    IL_0056:  nop
    IL_0057:  leave      IL_005f
  }  // end .try
  catch [System.Compiler.Runtime]Microsoft.Contracts.ContractMarkerException
  {
    IL_005c:  stloc.3
    IL_005d:  rethrow
  }  // end handler
  IL_005f:  nop
  IL_0060:  ret
} // end of method Test3::Increment

In order to see the exception being thrown, we'll have to introduce a little hack because we simply can't create an instance of Test3 with a negative value (because of the constructor's precondition). So, change the code like this:

using System;

class Test3
{
   int i;

   public Test3(int i)
   requires i > 0;
   {
      this.i = i;
   }

   public void Increment()
   ensures I > 0;
   {
      i++;
   }

   public int I
   {
      get
      {
         return i;
      }
   }

   public void Hack()
   {
      i = -1;
   }

   public static void Main()
   {
      Test3 t = new Test3(1);

      t.Increment();
      Console.WriteLine(t.I);

      t.Hack();

      t.Increment();
      Console.WriteLine(t.I);
   }
}

Compile and run and you should see this:

C:\temp\specsharp\test>test3
2

Unhandled Exception: Microsoft.Contracts.EnsuresException: Postcondition violated from method 'Test3.Increment'
   at Test3.Increment()
   at Test3.Main()

Just as we expected.

Now, in quite some cases we want to do more, relying on the old and new value of some attribute for example. In order to support this, Spec# has a keyword called old that allows you to save original values for postcondition evaluation purposes. Here we go for a simple sample:

using System;

class Test4
{
   int i;

   public Test4(int i)
   {
      this.i = i;
   }

   public void Increment()
   ensures I == old(I) + 1;
   {
      i++;
   }

   public int I
   {
      get
      {
         return i;
      }
   }

   public static void Main()
   {
      Test4 t = new Test4(1);
      t.Increment();

      Console.WriteLine(t.I);
   }
}

No preconditions anymore, just a little sample of a postcondition that checks the Increment method for correctness in a trivial case. Run and compile, it should execute just fine. What's interesting to see now, is how the old operator affects the IL code being generated by the Spec# compiler. Let's take a look again:

.method public hidebysig instance void  Increment() cil managed
{
  .custom instance void [System.Compiler.Runtime]Microsoft.Contracts.EnsuresAttribute::.ctor(string) = ( 01 00 4C 3A 3A 3D 3D 28 69 33 32 2C 69 33 32 29   // ..L::==(i32,i32)
                                                                                                         7B 74 68 69 73 40 54 65 73 74 34 3A 3A 67 65 74   //
{this@Test4::get
                                                                                                         5F 49 7B 7D 2C 3A 3A 2B 28 69 33 32 2C 69 33 32   // _I{},::+(i32,i32
                                                                                                         29 7B 5C 6F 6C 64 28 74 68 69 73 40 54 65 73 74   // ){\old(
this@Test
                                                                                                         34 3A 3A 67 65 74 5F 49 7B 7D 29 2C 31 7D 7D 06   // 4::get_I{}),1}}.
                                                                                                         00 53 0E 08 46 69 6C 65 6E 61 6D 65 20 43 3A 5C   // .S..Filename C:\
                                                                                                         74 65 6D 70 5C 73 70 65 63 73 68 61 72 70 5C 74   // temp\specsharp\t
                                                                                                         65 73 74 5C 74 65 73 74 34 2E 73 73 63 53 08 09   // est\test4.sscS..
                                                                                                         53 74 61 72 74 4C 69 6E 65 0D 00 00 00 53 08 0B   // StartLine....S..
                                                                                                         53 74 61 72 74 43 6F 6C 75 6D 6E 0C 00 00 00 53   // StartColumn....S
                                                                                                         08 07 45 6E 64 4C 69 6E 65 0D 00 00 00 53 08 09   // ..EndLine....S..
                                                                                                         45 6E 64 43 6F 6C 75 6D 6E 1B 00 00 00 53 0E 0A   // EndColumn....S..
                                                                                                         53 6F 75 72 63 65 54 65 78 74 18 65 6E 73 75 72   // SourceText.ensur
                                                                                                         65 73 20 49 20 3D 3D 20 6F 6C 64 28 49 29 20 2B   // es I == old(I) +
                                                                                                         20 31 3B )                                        //  1;
  // Code size       117 (0x75)
  .maxstack  7
  .locals init (int32 V_0,                                                                  //space to keep original value
           class [System.Compiler.Runtime]Microsoft.Contracts.ContractMarkerException V_1,
           int32 V_2,
           class [mscorlib]System.Exception V_3,
           object V_4,
           class [System.Compiler.Runtime]Microsoft.Contracts.ContractMarkerException V_5)
  .try
  {
    IL_0000:  ldarg.0
    IL_0001:  call       instance int32 Test4::get_I()  //retrieve the original value
    IL_0006:  stloc.0                                   //save it
    IL_0007:  leave      IL_000f
  }  // end .try
  catch [System.Compiler.Runtime]Microsoft.Contracts.ContractMarkerException
  {
    IL_000c:  stloc.1
    IL_000d:  rethrow
  }  // end handler
  IL_000f:  nop
  IL_0010:  ldarg.0
  IL_0011:  ldfld      int32 Test4::i
  IL_0016:  stloc.2
  IL_0017:  ldarg.0
  IL_0018:  ldloc.2
  IL_0019:  ldc.i4.1
  IL_001a:  add
  IL_001b:  stfld      int32 Test4::i
  IL_0020:  ldloc.2
  IL_0021:  pop
  .try
  {
    .try
    {
      IL_0022:  ldarg.0
      IL_0023:  call       instance int32 Test4::get_I() //get current (new) value
      IL_0028:  ldloc.0

      IL_0029:  ldc.i4.1
      IL_002a:  add                                      //old value + 1

      IL_002b:  bne.un     IL_0035                       //compare
      IL_0030:  leave      IL_0069
      IL_0035:  leave      IL_005e                       //jump to throw exception
    }  // end .try
    catch [mscorlib]System.Exception
    {
      IL_003a:  stloc.3
      IL_003b:  ldstr      "Exception occurred during evaluation of postcondit"
      + "ion in method 'Test4.Increment'"
      IL_0040:  ldloc.3
      IL_0041:  newobj     instance void [System.Compiler.Runtime]Microsoft.Contracts.InvalidContractException::.ctor(string,
                                                                                                                      class [mscorlib]System.Exception)
      IL_0046:  throw
      IL_0047:  leave      IL_005e
    }  // end handler
    catch [mscorlib]System.Object
    {
      IL_004c:  stloc.s    V_4
      IL_004e:  ldstr      "Exception occurred during evaluation of postcondit"
      + "ion in method 'Test4.Increment'"
      IL_0053:  newobj     instance void [System.Compiler.Runtime]Microsoft.Contracts.InvalidContractException::.ctor(string)
      IL_0058:  throw
      IL_0059:  leave      IL_005e
    }  // end handler
    IL_005e:  ldstr      "Postcondition violated from method 'Test4.Increment'"
    IL_0063:  newobj     instance void [System.Compiler.Runtime]Microsoft.Contracts.EnsuresException::.ctor(string)
    IL_0068:  throw
    IL_0069:  nop
    IL_006a:  leave      IL_0073
  }  // end .try
  catch [System.Compiler.Runtime]Microsoft.Contracts.ContractMarkerException
  {
    IL_006f:  stloc.s    V_5
    IL_0071:  rethrow
  }  // end handler
  IL_0073:  nop
  IL_0074:  ret
} // end of method Test4::Increment

As you can see, the old value is evaluated and kept aside for later comparison. Again, Boogie can be used to check a lot of this stuff already at compile time. There is far more that you can do however, e.g. using the forall function. Let's show you using an array sort class:

using System;

class Test5
{
   int[]! array;
   int n;

   public Test5(int[]! a)
   {
      this.array = a;
      this.n = a.Length;
      base(); //needed for proper initialization of array attribute
   }

   public int this[int i]
   {
      get
      {
         return array[i];
      }
   }

   public void Sort()
   ensures forall { int i in (1:N); this[i-1] <= this[i] };
   {
      Array.Sort(array);
   }

   public int N
   {
      get
      {
         return n;
      }
   }

   public static void Main()
   {
      new Test5(new int[] {3,2,1} ).Sort();
   }
}

The ensures postcondition statement for the Sort method in here is pretty straightforward. I just loops over the array on positions 1 ... N-1 (the last parameter to the ':' range operator in forall denotes the upper bound, not included in the range) and checks the element in front of it to be lower than or equal than the current element. In this sample, I just used the Array.Sort method of the BCL to show the sorting. If you comment out the Array.Sort call and compile again, the application should not run anymore and throw an EnsuresException. In IL, the forall-check looks like this:

.method public hidebysig instance void  Sort() cil managed
{
  .custom instance void [System.Compiler.Runtime]Microsoft.Contracts.EnsuresAttribute::.ctor(string) = ( 01 00 80 D0 66 6F 72 61 6C 6C 7B 7C 7B 69 33 32   // ....forall{|{i32
                                                                                                         2C 24 62 6C 6F 63 6B 56 61 72 28 69 33 32 29 7B   // ,$blockVar(i32){
                                                                                                         69 7D 2C 28 3A 3A 3A 28 69 33 32 2C 69 33 32 29   // i},(:::(i32,i32)
                                                                                                         7B 31 2C 3A 3A 2D 28 69 33 32 2C 69 33 32 29 7B   // {1,::-(i32,i32){
                                                                                                         74 68 69 73 40 54 65 73 74 35 3A 3A 67 65 74 5F   //
this@Test5::get_
                                                                                                         4E 7B 7D 2C 31 7D 7D 29 7D 3B 3A 3A 3C 3D 28 69   // N{},1}})};::<=(i
                                                                                                         33 32 2C 69 33 32 29 7B 74 68 69 73 40 54 65 73   // 32,i32){this@Tes
                                                                                                         74 35 3A 3A 67 65 74 5F 49 74 65 6D 28 69 33 32   // t5::get_Item(i32
                                                                                                         29 7B 3A 3A 2D 28 69 33 32 2C 69 33 32 29 7B 24   // ){::-(i32,i32){$
                                                                                                         62 6C 6F 63 6B 56 61 72 28 69 33 32 29 7B 69 7D   // blockVar(i32){i}
                                                                                                         2C 31 7D 7D 2C 74 68 69 73 40 54 65 73 74 35 3A   // ,1}},this@Test5:
                                                                                                         3A 67 65 74 5F 49 74 65 6D 28 69 33 32 29 7B 24   // :get_Item(i32){$
                                                                                                         62 6C 6F 63 6B 56 61 72 28 69 33 32 29 7B 69 7D   // blockVar(i32){i}
                                                                                                         7D 7D 7C 7D 06 00 53 0E 08 46 69 6C 65 6E 61 6D   // }}|}..S..Filenam
                                                                                                         65 20 43 3A 5C 74 65 6D 70 5C 73 70 65 63 73 68   // e C:\temp\specsh
                                                                                                         61 72 70 5C 74 65 73 74 5C 74 65 73 74 35 2E 73   // arp\test\test5.s
                                                                                                         73 63 53 08 09 53 74 61 72 74 4C 69 6E 65 18 00   // scS..StartLine..
                                                                                                         00 00 53 08 0B 53 74 61 72 74 43 6F 6C 75 6D 6E   // ..S..StartColumn
                                                                                                         0C 00 00 00 53 08 07 45 6E 64 4C 69 6E 65 18 00   // ....S..EndLine..
                                                                                                         00 00 53 08 09 45 6E 64 43 6F 6C 75 6D 6E 3B 00   // ..S..EndColumn;.
                                                                                                         00 00 53 0E 0A 53 6F 75 72 63 65 54 65 78 74 38   // ..S..SourceText8
                                                                                                         65 6E 73 75 72 65 73 20 66 6F 72 61 6C 6C 20 7B   // ensures forall {
                                                                                                         20 69 6E 74 20 69 20 69 6E 20 28 31 3A 4E 29 3B   //  int i in (1:N);
                                                                                                         20 74 68 69 73 5B 69 2D 31 5D 20 3C 3D 20 74 68   //  this[i-1] <= th
                                                                                                         69 73 5B 69 5D 20 7D 3B )                         // is[i] };
  // Code size       149 (0x95)
  .maxstack  10
  .locals init (bool V_0,
           int32 V_1,
           class [mscorlib]System.Exception V_2,
           object V_3,
           class [System.Compiler.Runtime]Microsoft.Contracts.ContractMarkerException V_4)
  IL_0000:  ldarg.0
  IL_0001:  ldfld      int32[] modopt([System.Compiler.Runtime]Microsoft.Contracts.NonNullType) Test5::'array'
  IL_0006:  call       void [mscorlib]System.Array::Sort(class [mscorlib]System.Array)
  .try
  {
    .try
    {
      IL_000b:  ldc.i4.1
      IL_000c:  stloc.0
      IL_000d:  ldc.i4.1
      IL_000e:  stloc.1
      IL_000f:  ldloc.1                                          //begin of loop
      IL_0010:  ldarg.0
      IL_0011:  call       instance int32 Test5::get_N()
      IL_0016:  ldc.i4.1
      IL_0017:  sub
      IL_0018:  bgt        IL_004b
      IL_001d:  ldarg.0
      IL_001e:  ldloc.1
      IL_001f:  ldc.i4.1
      IL_0020:  sub
      IL_0021:  call       instance int32 Test5::get_Item(int32) //this[i-1]
      IL_0026:  ldarg.0
      IL_0027:  ldloc.1
      IL_0028:  call       instance int32 Test5::get_Item(int32) //this[i]
      IL_002d:  ble        IL_0038                               //<=
      IL_0032:  ldc.i4.0
      IL_0033:  br         IL_0039
      IL_0038:  ldc.i4.1
      IL_0039:  stloc.0
      IL_003a:  ldloc.0
      IL_003b:  brtrue     IL_0045
      IL_0040:  br         IL_004b                               //leave the loop
      IL_0045:  ldloc.1
      IL_0046:  ldc.i4.1
      IL_0047:  add                                              //loop counter i
      IL_0048:  stloc.1
      IL_0049:  br.s       IL_000f                               //end of loop
      IL_004b:  ldloc.0
      IL_004c:  brfalse    IL_0056                               //not what we expected to see, jump to leave .try and throw exception
      IL_0051:  leave      IL_0089
      IL_0056:  leave      IL_007e                               //time to throw exception
    }  // end .try
    catch [mscorlib]System.Exception
    {
      IL_005b:  stloc.2
      IL_005c:  ldstr      "Exception occurred during evaluation of postcondit"
      + "ion in method 'Test5.Sort'"
      IL_0061:  ldloc.2
      IL_0062:  newobj     instance void [System.Compiler.Runtime]Microsoft.Contracts.InvalidContractException::.ctor(string,
                                                                                                                      class [mscorlib]System.Exception)
      IL_0067:  throw
      IL_0068:  leave      IL_007e
    }  // end handler
    catch [mscorlib]System.Object
    {
      IL_006d:  stloc.3
      IL_006e:  ldstr      "Exception occurred during evaluation of postcondit"
      + "ion in method 'Test5.Sort'"
      IL_0073:  newobj     instance void [System.Compiler.Runtime]Microsoft.Contracts.InvalidContractException::.ctor(string)
      IL_0078:  throw
      IL_0079:  leave      IL_007e
    }  // end handler
    IL_007e:  ldstr      "Postcondition violated from method 'Test5.Sort'"
    IL_0083:  newobj     instance void [System.Compiler.Runtime]Microsoft.Contracts.EnsuresException::.ctor(string)
    IL_0088:  throw
    IL_0089:  nop
    IL_008a:  leave      IL_0093
  }  // end .try
  catch [System.Compiler.Runtime]Microsoft.Contracts.ContractMarkerException
  {
    IL_008f:  stloc.s    V_4
    IL_0091:  rethrow
  }  // end handler
  IL_0093:  nop
  IL_0094:  ret
} // end of method Test5::Sort

That's, I believe, enough for postconditions. You certainly can think about hundreds of other samples around this, so I invite you to brainstorm about this. Also take a look at the samples arraylist and bag which are included with Spec#. There is however an associated topic for postconditions which I'll explain in the context of exceptions in the next paragraph.

 

Exceptions

Normally, every one who's reading this blog should be aware of the concept of exceptions in languages such as C++, C#, Java, VB.NET in order to provide developers with a mechanism to handle runtime errors systematically (try ... catch ... finally ... structures and the throw statement). Where Spec#'s exception mechanism is different from the one we find in C# is the support for checked and unchecked exceptions, something that's present today in Java and derived from mechanisms employed in e.g. Modula-3. Let's start with C# exceptions, which is pretty straightforward. To start with, every exception dirives from the base class System.Exception (in contrast to C++ where every object can act as an exception). Because exceptions are objects, they can carry data with them to describe the error and other stuff. The basic mechanism of C# exceptions is this:

Caller

try
{
   DoSomething();
}
catch (SomeException ex)
{
   //perform cleanup
}
finally
{
   //release acquired resources (runs always)
}

Note: To be complete, I have to admit that "release acquired resources" is not possible in certain conditions (e.g. a rude appdomain unload). To support these scenarios, .NET v2.0 introduces the concept of constrained execution regions (CERs) which I'll cover in some other post on CLR Hosting later on.

Implementor

void DoSomething()
{
   //Normal work
   ...

   //Now we're in big troubles, let's tell the caller he has to help us; we're totally lost *SCREAM*
   throw new SomeException();
}

However, there is no such concept as a throws list that can be attached to a method declaration. So, a method in C# can throw any exception it wants to do, therefore relying on method comments (e.g. ///stuff) to tell consumers about the exception throwing policy of the method (read: tell callers what to catch). Java has this, C# hasn't, Spec# introduces it and extends it with "exceptional postconditions". But first, some terminology.

Spec# has two kinds of exception types:

  • checked exceptions are admissible failures that should be caught by the caller(s); Spec# provides the ICheckedException interface to create checked exceptions
  • unchecked exceptions signal client failures or observed program errors and are caught by the runtime default exception handler (or in main using a catch-all); in C#, all exceptions can be seen as unchecked as there is no "throws"-method signature contract

In fact, that's enough for you to know about this stuff in order to get the point of the following example:

public void DoSomething()
throws SomeException; //SomeException : ICheckedException
{ ... }

This tells the caller: you should catch this, it's possible that this exception occurs, we have code in here to throw it (and RTFM if you want to know more about when it gets thrown :-)). Exceptional postconditions allow you as a developer to specify postconditions that have to be checked in case of an exception being thrown. Let's show you an example:

using System;

class Test6
{
   private int i;

   public Test6(int i)
   {
      this.i = i;
   }

   public void Do()
   throws SomeException;
   {
      if (1 == 1) //this is really exceptional :o
         throw new SomeException();
   }

   public int I
   {
      get
      {
         return i;
      }
   }

   public static void Main()
   {
      try
      {
         new Test6(1).Do();
      }
      catch (SomeException)
      {
         Console.WriteLine("EXCEPTION");
      }
   }
}

class SomeException : Exception, Microsoft.Contracts.ICheckedException
{
}

Some important points include:

  • the semicolon after the throws statement in the Do method declaration
  • the SomeException derives-from and implements list which includes System.Exception and Microsoft.Contracts.ICheckedException

When you'd drop the red part in the code, you'd get to see the following compiler error:

C:\temp\specsharp\test>ssc test6.ssc
test6.ssc(12,21): error CS2627: 'Test6.Do' : Cannot specify an unchecked exception in a throws clause.

If you drop the purple colored piece of code, you'd see this:

C:\temp\specsharp\test>ssc test6.ssc
test6.ssc(28,10): error CS2609: The checked exception 'SomeException' can be thrown but is not listed in the throws clause for method 'Test6.Main()'.

Which indicates that the exception is propagating up to the Main method and should be caught over there (in a real application you'd like to catch it higher up the stack). Spec# uses a conservative control-flow analysis to detect this.

Now, what about "exceptional postconditions"? Change the code as follows:

using System;

class Test6
{
   private int i;

   public Test6(int i)
   {
      this.i = i;
   }

   public void Do()
   throws SomeException ensures old(I) == I;
   {
      i++;

      if (1 == 1) //this is really exceptional :o
         throw new SomeException();
   }

   public int I
   {
      get
      {
         return i;
      }
   }

   public static void Main()
   {
      try
      {
         new Test6(1).Do();
      }
      catch (SomeException)
      {
         Console.WriteLine("EXCEPTION");
      }
   }
}

class SomeException : Exception, Microsoft.Contracts.ICheckedException
{
}

Now we have some ensure statement (= postcondition) that should make sure the object's "i" field is in it's initial state when the exception occurs (ensures old(I) == I). Compile and run. You should get this:

C:\temp\specsharp\test>test6

Unhandled Exception: Microsoft.Contracts.EnsuresException: Postcondition violated from method 'Test6.Do'
   at Test6.Do()
   at Test6.Main()

Time to IL again to see what's happening in here:

.method public hidebysig instance void  Do() cil managed
{
  .custom instance void [System.Compiler.Runtime]Microsoft.Contracts.EnsuresAttribute::.ctor(string) = ( 01 00 3C 3A 3A 3D 3D 28 69 33 32 2C 69 33 32 29   // ..<::==(i32,i32)
                                                                                                         7B 5C 6F 6C 64 28 74 68 69 73 40 54 65 73 74 36   // {\old(
this@Test6
                                                                                                         3A 3A 67 65 74 5F 49 7B 7D 29 2C 74 68 69 73 40   // ::get_I{}),this@
                                                                                                         54 65 73 74 36 3A 3A 67 65 74 5F 49 7B 7D 7D 06   // Test6::get_I{}}.
                                                                                                         00 53 0E 08 46 69 6C 65 6E 61 6D 65 20 43 3A 5C   // .S..Filename C:\
                                                                                                         74 65 6D 70 5C 73 70 65 63 73 68 61 72 70 5C 74   // temp\specsharp\t
                                                                                                         65 73 74 5C 74 65 73 74 36 2E 73 73 63 53 08 09   // est\test6.sscS..
                                                                                                         53 74 61 72 74 4C 69 6E 65 0D 00 00 00 53 08 0B   // StartLine....S..
                                                                                                         53 74 61 72 74 43 6F 6C 75 6D 6E 21 00 00 00 53   // StartColumn!...S
                                                                                                         08 07 45 6E 64 4C 69 6E 65 0D 00 00 00 53 08 09   // ..EndLine....S..
                                                                                                         45 6E 64 43 6F 6C 75 6D 6E 2C 00 00 00 53 0E 0A   // EndColumn,...S..
                                                                                                         53 6F 75 72 63 65 54 65 78 74 29 74 68 72 6F 77   // SourceText)throw
                                                                                                         73 20 53 6F 6D 65 45 78 63 65 70 74 69 6F 6E 20   // s SomeException
                                                                                                         65 6E 73 75 72 65 73 20 6F 6C 64 28 49 29 20 3D   // ensures old(I) =
                                                                                                         3D 20 49 3B )                                     // = I;
  // Code size       127 (0x7f)
  .maxstack  6
  .locals init (int32 V_0,                                                                 //location to save original value of I
           class [System.Compiler.Runtime]Microsoft.Contracts.ContractMarkerException V_1,
           int32 V_2,
           class SomeException V_3,
           class [mscorlib]System.Exception V_4,
           class [mscorlib]System.Exception V_5)
  .try
  {
    IL_0000:  ldarg.0
    IL_0001:  call       instance int32 Test6::get_I()  //get the value of I which needs to be saved for old(I)
    IL_0006:  stloc.0                                   //store it on stack location 0
    IL_0007:  leave      IL_000f
  }  // end .try
  catch [System.Compiler.Runtime]Microsoft.Contracts.ContractMarkerException
  {
    IL_000c:  stloc.1
    IL_000d:  rethrow
  }  // end handler
  IL_000f:  nop
  .try
  {
    IL_0010:  ldarg.0
    IL_0011:  ldfld      int32 Test6::i
    IL_0016:  stloc.2
    IL_0017:  ldarg.0
    IL_0018:  ldloc.2
    IL_0019:  ldc.i4.1
    IL_001a:  add
    IL_001b:  stfld      int32 Test6::i
    IL_0020:  ldloc.2
    IL_0021:  pop
    IL_0022:  ldc.i4.1
    IL_0023:  brfalse    IL_002e
    IL_0028:  newobj     instance void SomeException::.ctor()  //exception is thrown in these two lines
    IL_002d:  throw
    IL_002e:  leave      IL_007d
  }  // end .try
  catch SomeException                                          //ola baby, we catch it ourselves?
  {
    IL_0033:  stloc.3
    .try
    {
      IL_0034:  ldloc.0                                        //load the old value from the stack
      IL_0035:  ldarg.0
      IL_0036:  call       instance int32 Test6::get_I()       //get the new value

      IL_003b:  bne.un     IL_0045                             //compare
      IL_0040:  leave      IL_007b
      IL_0045:  leave      IL_0070                             //we can get no satisfaction ;-)
    }  // end .try
    catch [mscorlib]System.Exception
    {
      IL_004a:  stloc.s    V_4
      IL_004c:  ldstr      "Exception occurred during evaluation of postcondit"
      + "ion in method 'Test6.Do'"
      IL_0051:  ldloc.s    V_4
      IL_0053:  newobj     instance void [System.Compiler.Runtime]Microsoft.Contracts.EnsuresException::.ctor(string,
                                                                                                              class [mscorlib]System.Exception)
      IL_0058:  throw
      IL_0059:  leave      IL_0070
    }  // end handler
    catch [mscorlib]System.Object
    {
      IL_005e:  stloc.s    V_5
      IL_0060:  ldstr      "Exception occurred during evaluation of postcondit"
      + "ion in method 'Test6.Do'"
      IL_0065:  newobj     instance void [System.Compiler.Runtime]Microsoft.Contracts.EnsuresException::.ctor(string)
      IL_006a:  throw
      IL_006b:  leave      IL_0070
    }  // end handler
    IL_0070:  ldstr      "Postcondition violated from method 'Test6.Do'"                                             //postcondition is not okay, this exception survives
    IL_0075:  newobj     instance void [System.Compiler.Runtime]Microsoft.Contracts.EnsuresException::.ctor(string)
    IL_007a:  throw                                                                                                  //throw EnsuresException for postcondition failure
    IL_007b:  rethrow                                                                                                //ola baby cont'd: yes, but we rethrow the exception
  }  // end handler
  IL_007d:  nop
  IL_007e:  ret
} // end of method Test6::Do

So, basically, the mechanism is not that difficult at all: we (the developer) throw the checked exception; Spec# emits code to catch it in order to check the postcondition; if the postcondition is not okay, an EnsuresException is thrown, otherwise the checked exception survives.

In order to have the sample work correctly, it should be changed as follows to restore the original state before throwing the exception:

using System;

class Test6
{
   private int i;

   public Test6(int i)
   {
      this.i = i;
   }

   public void Do()
   throws SomeException ensures old(I) == I;
   {
      i++;

      if (1 == 1) //this is really exceptional :o
      {
         i--;
         throw new SomeException();
      }
   }

   public int I
   {
      get
      {
         return i;
      }
   }

   public static void Main()
   {
      try
      {
         new Test6(1).Do();
      }
      catch (SomeException)
      {
         Console.WriteLine("EXCEPTION");
      }
   }
}

class SomeException : Exception, Microsoft.Contracts.ICheckedException
{
}

More information about exceptions in Spec# can be found in Exception safety in C# [PDF].

 

Frame conditions

I'm not going to cover this in much detail, as Spec# does not enforce frame conditions at runtime because of the overhead incurred and the aimed compatibility with C# (which is of course a very good thing). Simply stated, frame conditions allow you to decorate methods (and properties, indexers, ...) with a modifies clause to specify which fields of the object can be modified by the method when it's invoked. These declarations are used and enforced by Boogie, not the Spec# compiler itself (thus no enforcement at runtime as I explained earlier). A simple example is the following:

class A
{
   B b;
   C c;

   void D() modifies b;
   { ... }
}

I guess you can tell me now what Boogie will complain about if you try to change c inside D.

 

Object invariants

So far, we've been discussing tools in Spec# to specify a contract with the outside world: this method has the following preconditions and will result in the following set of postconditions to hold and if something goes wrong, we'll tell you Mr. Caller by throwing these checked exceptions which you should take care of. Invariants can be categorized as a class contract that keeps an eye on the internal state of the object. Spec# considers two different states for objects which have relation to the object invariants. First of all there is the so-called steady state in which all invariants hold. The second state is the exposed state in which it's not needed for the invariants to hold, because of intermediate stages during an update. An example (which is in the documentation but which I won't put in code over here) is a class that contains two arrays that should have the same length all the time. If you need to make the arrays bigger in size, you can't do this in one operation. Instead, you need to change the length of the two arrays one by one, which introduces an intermediate state in which the invariant can impossibly hold. Let's show how you do you use the expose keyword and the declaration of an invariant to do this kind of stuff:

using System;

class Test7
{
   int online;
   int offline;
   int total;

   bool[]! state;

   invariant online + offline == total;

   public Test7(int n)
   {
      offline = total = n;
      online = 0;
      state = new bool[n];

      base();
   }

   public void Login(int i)
   ensures 0 <= i && i < Total;
   {
      expose(this)
      {
         state[i] = true;
         online++;
         offline--;
      }
   }

   public void Logoff(int i)
   ensures 0 <= i && i < Total;
   {
      expose(this)
      {
         state[i] = false;
         online--;
         offline++;
      }
   }

   public int Total
   {
      get
      {
         return total;
      }
   }

   public static void Main()
   {
      Test7 t = new Test7(10);
      t.Login(3);
      t.Login(4);
   }
}

In this sample, you can see the invariant declaration on top of the class definition, which is pretty simple in this case. Second, you can see the expose block which is used to tell the system: in here, do not pay attention to the invariants, but check for correctness at the end of the block. We're using this to expose the current object, which will be the case in the majority of the cases. When you compile and run, it should just work fine (no output will be displayed however). Note: you could extend the Logon and Logoff methods in some way (fill in yourself) to make sure a user who is logged on can't log on (and similar for log off).

<PermissionToRead Groups="Everyone">

Why do we need invariants after all? That's a pretty good question. One could argue it's possible to have the invariant condition checked all the time when the variables that participate in it are being changed. But that would introduce a tremendous amount of additional code in your application, only to do this kind of checking. What about adding invariants to preconditions and postconditions? Not an option either, because preconditions and postconditions are meant to be contracts with the caller, so the caller should be able to know about elements that participate in the condition. It's clear that an invariant reflects the consistency of some internal state, and as we know information hiding is the key to survive in OO, thus we certainly don't want to expose internal state to the external world so that a caller can .... You get the point?

</PermissionToRead>

Time to take a look at how this works through IL inspection. First of all, take a look at the Test7 members which are displayed in ildasm.exe. You should notice the following strangers:

  • attribute SpecSharp:frameGuard
  • method CheckInvariant
  • method InitGuardSets
  • property getter get_FrameGuard
  • property getter get_ObjectGuard

Okay, this should draw a first picture of what's going on. There is something, called a guard, that wakes for the consistency of the object by checking the invariants. What about the CheckInvariant method, which has a pretty meaningful name by itself? Here's the IL:

.method public hidebysig instance bool  CheckInvariant(bool throwException) cil managed
{
  // Code size       72 (0x48)
  .maxstack  4
  .locals init (bool V_0,
           bool V_1)
  IL_0000:  ldarg.0
  IL_0001:  ldfld      int32 Test7::online
  IL_0006:  ldarg.0
  IL_0007:  ldfld      int32 Test7::offline
  IL_000c:  add
  IL_000d:  ldarg.0
  IL_000e:  ldfld      int32 Test7::total
  IL_0013:  beq        IL_001e
  IL_0018:  ldc.i4.0
  IL_0019:  br         IL_001f
  IL_001e:  ldc.i4.1
  IL_001f:  brtrue     IL_003d
  IL_0024:  ldarg.1
  IL_0025:  brfalse    IL_0035
  IL_002a:  newobj     instance void [System.Compiler.Runtime]Microsoft.Contracts.ObjectInvariantException::.ctor()
  IL_002f:  throw
  IL_0030:  br         IL_003d
  IL_0035:  ldc.i4.0
  IL_0036:  stloc.0
  IL_0037:  br         IL_0044
  IL_003c:  nop
  IL_003d:  ldc.i4.1
  IL_003e:  stloc.0
  IL_003f:  br         IL_0044
  IL_0044:  ldloc.0
  IL_0045:  stloc.1
  IL_0046:  ldloc.0
  IL_0047:  ret
} // end of method Test7::CheckInvariant

I've not added personal comments to the method's IL as I think it should be pretty clear what's going on. The method takes a boolean parameter to indicate whether an exception should be thrown when the invariant does not match or not. The method itself contains the logic to check the invariant and to return true or false to indicate the invariant's correctness. No magic in here...

InitGuardSets won't learn us anything either, it's just empty. The get_FrameGuard and get_ObjectGuard methods are self-explaining as well, just returning some object that's called the "guard" with some casting where needed. What's more interesting however is to see what happens with the methods we've declared ourselves. Let's start with something which we don't suspect of being dramatically changed by the introduction of an invariant, being the get_Total property:

.method public hidebysig specialname instance int32
        get_Total() cil managed
{
  // Code size       99 (0x63)
  .maxstack  5
  .locals init (class [mscorlib]System.Exception V_0,
           object V_1,
           class [System.Compiler.Runtime]Microsoft.Contracts.ContractMarkerException V_2,
           int32 V_3,
           int32 V_4)
  .try
  {
    .try
    {
      IL_0000:  ldarg.0
      IL_0001:  call       instance class [System.Compiler.Runtime]Microsoft.Contracts.Guard modopt([System.Compiler.Runtime]Microsoft.Contracts.NonNullType) Test7::get_FrameGuard()  //get the frame guard
      IL_0006:  call       instance bool [System.Compiler.Runtime]Microsoft.Contracts.Guard::get_CanStartWriting()  //get the property value for CanStartWriting (boolean)
      IL_000b:  brfalse    IL_0015
      IL_0010:  leave      IL_0048
      IL_0015:  leave      IL_003d  //hmm, we can't do safe play, let's throw an exception
    }  // end .try
    catch [mscorlib]System.Exception
    {
      IL_001a:  stloc.0
      IL_001b:  ldstr      "Exception occurred during evaluation of preconditi"
      + "on in method 'Test7.get_Total'"
      IL_0020:  ldloc.0
      IL_0021:  newobj     instance void [System.Compiler.Runtime]Microsoft.Contracts.InvalidContractException::.ctor(string,
                                                                                                                      class [mscorlib]System.Exception)
      IL_0026:  throw
      IL_0027:  leave      IL_003d
    }  // end handler
    catch [mscorlib]System.Object
    {
      IL_002c:  stloc.1
      IL_002d:  ldstr      "Exception occurred during evaluation of preconditi"
      + "on in method 'Test7.get_Total'"
      IL_0032:  newobj     instance void [System.Compiler.Runtime]Microsoft.Contracts.InvalidContractException::.ctor(string)
      IL_0037:  throw
      IL_0038:  leave      IL_003d
    }  // end handler
    IL_003d:  ldstr      "Precondition violated from method 'Test7.get_Total'"
    IL_0042:  newobj     instance void [System.Compiler.Runtime]Microsoft.Contracts.RequiresException::.ctor(string)  //create the exception
    IL_0047:  throw                                                                                                   //and throw
 
   IL_0048:  nop
    IL_0049:  leave      IL_0051
  }  // end .try
  catch [System.Compiler.Runtime]Microsoft.Contracts.ContractMarkerException
  {
    IL_004e:  stloc.2
    IL_004f:  rethrow
  }  // end handler
  IL_0051:  nop
  IL_0052:  ldarg.0
  IL_0053:  ldfld      int32 Test7::total
  IL_0058:  stloc.3
  IL_0059:  br         IL_005e
  IL_005e:  ldloc.3
  IL_005f:  stloc.s    V_4
  IL_0061:  ldloc.3
  IL_0062:  ret  //default execution path
} // end of method Test7::get_Total

Hmm, no changes as we'd expect? Wrong at first sight. But what's happening for godsake? There were no preconditions defined on the getter for property Total, and in IL we see one appear. Moreover, there is no call to CheckInvariant either, so it hasn't anything to do directly (!) with the invariant. So, let's skip this for now...

What about the Login method? There's much more in here, as you can see below:

.method public hidebysig instance void  Login(int32 i) cil managed
{
  .custom instance void [System.Compiler.Runtime]Microsoft.Contracts.EnsuresAttribute::.ctor(string) = ( 01 00 4D 3A 3A 26 26 28 62 6F 6F 6C 2C 62 6F 6F   // ..M::&&(bool,boo
                                                                                                         6C 29 7B 3A 3A 3C 3D 28 69 33 32 2C 69 33 32 29   // l){::<=(i32,i32)
                                                                                                         7B 30 2C 24 31 7D 2C 3A 3A 3C 28 69 33 32 2C 69   // {0,$1},::<(i32,i
                                                                                                         33 32 29 7B 24 31 2C 74 68 69 73 40 54 65 73 74   // 32){$1,this@Test
                                                                                                         37 3A 3A 67 65 74 5F 54 6F 74 61 6C 7B 7D 7D 7D   // 7::get_Total{}}}
                                                                                                         06 00 53 0E 08 46 69 6C 65 6E 61 6D 65 20 43 3A   // ..S..Filename C:
                                                                                                         5C 74 65 6D 70 5C 73 70 65 63 73 68 61 72 70 5C   // \temp\specsharp\
                                                                                                         74 65 73 74 5C 74 65 73 74 37 2E 73 73 63 53 08   // test\test7.sscS.
                                                                                                         09 53 74 61 72 74 4C 69 6E 65 17 00 00 00 53 08   // .StartLine....S.
                                                                                                         0B 53 74 61 72 74 43 6F 6C 75 6D 6E 0C 00 00 00   // .StartColumn....
                                                                                                         53 08 07 45 6E 64 4C 69 6E 65 17 00 00 00 53 08   // S..EndLine....S.
                                                                                                         09 45 6E 64 43 6F 6C 75 6D 6E 1F 00 00 00 53 0E   // .EndColumn....S.
                                                                                                         0A 53 6F 75 72 63 65 54 65 78 74 1C 65 6E 73 75   // .SourceText.ensu
                                                                                                         72 65 73 20 30 20 3C 3D 20 69 20 26 26 20 69 20   // res 0 <= i && i
                                                                                                         3C 20 54 6F 74 61 6C 3B )                         // < Total;
  // Code size       288 (0x120)
  .maxstack  13
  .locals init (class [mscorlib]System.Exception V_0,
           object V_1,
           class [System.Compiler.Runtime]Microsoft.Contracts.ContractMarkerException V_2,
           class [System.Compiler.Runtime]Microsoft.Contracts.Guard modopt([System.Compiler.Runtime]Microsoft.Contracts.NonNullType) V_3,  //place to hold the guard
           class [mscorlib]System.Exception V_4,
           int32 V_5,
           int32 V_6,
           class [mscorlib]System.Exception V_7,
           class [mscorlib]System.Exception V_8,
           object V_9,
           class [System.Compiler.Runtime]Microsoft.Contracts.ContractMarkerException V_10)
  .try
  {
    .try
    {
      IL_0000:  ldarg.0
      IL_0001:  call       instance class [System.Compiler.Runtime]Microsoft.Contracts.Guard modopt([System.Compiler.Runtime]Microsoft.Contracts.NonNullType) Test7::get_FrameGuard()
      IL_0006:  call       instance bool [System.Compiler.Runtime]Microsoft.Contracts.Guard::get_CanStartWriting()
      IL_000b:  brfalse    IL_0015
      IL_0010:  leave      IL_0048
      IL_0015:  leave      IL_003d
    }  // end .try
    catch [mscorlib]System.Exception
    {
      IL_001a:  stloc.0
      IL_001b:  ldstr      "Exception occurred during evaluation of preconditi"
      + "on in method 'Test7.Login(System.Int32)'"
      IL_0020:  ldloc.0
      IL_0021:  newobj     instance void [System.Compiler.Runtime]Microsoft.Contracts.InvalidContractException::.ctor(string,
                                                                                                                      class [mscorlib]System.Exception)
      IL_0026:  throw
      IL_0027:  leave      IL_003d
    }  // end handler
    catch [mscorlib]System.Object
    {
      IL_002c:  stloc.1
      IL_002d:  ldstr      "Exception occurred during evaluation of preconditi"
      + "on in method 'Test7.Login(System.Int32)'"
      IL_0032:  newobj     instance void [System.Compiler.Runtime]Microsoft.Contracts.InvalidContractException::.ctor(string)
      IL_0037:  throw
      IL_0038:  leave      IL_003d
    }  // end handler
    IL_003d:  ldstr      "Precondition violated from method 'Test7.Login(Sys"
    + "tem.Int32)'"
    IL_0042:  newobj     instance void [System.Compiler.Runtime]Microsoft.Contracts.RequiresException::.ctor(string)
    IL_0047:  throw
    IL_0048:  nop
    IL_0049:  leave      IL_0051
  }  // end .try
  catch [System.Compiler.Runtime]Microsoft.Contracts.ContractMarkerException
  {
    IL_004e:  stloc.2
    IL_004f:  rethrow
  }  // end handler
  IL_0051:  nop
  IL_0052:  ldarg.0
  IL_0053:  call       instance class [System.Compiler.Runtime]Microsoft.Contracts.Guard modopt([System.Compiler.Runtime]Microsoft.Contracts.NonNullType) Test7::get_FrameGuard()
  IL_0058:  call       instance class [System.Compiler.Runtime]Microsoft.Contracts.Guard [System.Compiler.Runtime]Microsoft.Contracts.Guard::StartWritingTransitively()  //here the guard is starting its mission
  IL_005d:  stloc.3  //store the guard
  IL_005e:  ldnull
  IL_005f:  stloc.s    V_4
  .try
  {
    .try
    {
      IL_0061:  ldarg.0
      IL_0062:  ldfld      bool[] modopt([System.Compiler.Runtime]Microsoft.Contracts.NonNullType) Test7::state
      IL_0067:  ldarg.1
      IL_0068:  ldc.i4.1
      IL_0069:  stelem.i1
      IL_006a:  ldarg.0
      IL_006b:  ldfld      int32 Test7::online
      IL_0070:  stloc.s    V_5
      IL_0072:  ldarg.0
      IL_0073:  ldloc.s    V_5
      IL_0075:  ldc.i4.1
      IL_0076:  add
      IL_0077:  stfld      int32 Test7::online
      IL_007c:  ldloc.s    V_5
      IL_007e:  pop
      IL_007f:  ldarg.0
      IL_0080:  ldfld      int32 Test7::offline
      IL_0085:  stloc.s    V_6
      IL_0087:  ldarg.0
      IL_0088:  ldloc.s    V_6
      IL_008a:  ldc.i4.1
      IL_008b:  sub
      IL_008c:  stfld      int32 Test7::offline
      IL_0091:  ldloc.s    V_6
      IL_0093:  pop
      IL_0094:  leave      IL_00c6
    }  // end .try
    catch [mscorlib]System.Exception
    {
      IL_0099:  stloc.s    V_7
      IL_009b:  ldloc.s    V_7
      IL_009d:  stloc.s    V_4
      IL_009f:  rethrow
      IL_00a1:  leave      IL_00c6
    }  // end handler
  }  // end .try
  finally
  {
    IL_00a6:  ldloc.s    V_4
    IL_00a8:  ldnull
    IL_00a9:  beq        IL_00bf
    IL_00ae:  ldloc.s    V_4
    IL_00b0:  isinst     [System.Compiler.Runtime]Microsoft.Contracts.ICheckedException //extra code to propagate unchecked exceptions without further invariant checking
    IL_00b5:  brtrue     IL_00bf
    IL_00ba:  br         IL_00c5
    IL_00bf:  ldloc.3  //get the guard
    IL_00c0:  call       instance void [System.Compiler.Runtime]Microsoft.Contracts.Guard::EndWritingTransitively()  //and here the guard's mission is completed
    IL_00c5:  endfinally
  }  // end handler
  .try
  {
    .try
    {
      IL_00c6:  ldc.i4.0
      IL_00c7:  ldarg.1
      IL_00c8:  bgt        IL_00de
      IL_00cd:  ldarg.1
      IL_00ce:  ldarg.0
      IL_00cf:  call       instance int32 Test7::get_Total()
      IL_00d4:  bge        IL_00de
      IL_00d9:  leave      IL_0114
      IL_00de:  leave      IL_0109
    }  // end .try
    catch [mscorlib]System.Exception
    {
      IL_00e3:  stloc.s    V_8
      IL_00e5:  ldstr      "Exception occurred during evaluation of postcondit"
      + "ion in method 'Test7.Login(System.Int32)'"
      IL_00ea:  ldloc.s    V_8
      IL_00ec:  newobj     instance void [System.Compiler.Runtime]Microsoft.Contracts.InvalidContractException::.ctor(string,
                                                                                                                      class [mscorlib]System.Exception)
      IL_00f1:  throw
      IL_00f2:  leave      IL_0109
    }  // end handler
    catch [mscorlib]System.Object
    {
      IL_00f7:  stloc.s    V_9
      IL_00f9:  ldstr      "Exception occurred during evaluation of postcondit"
      + "ion in method 'Test7.Login(System.Int32)'"
      IL_00fe:  newobj     instance void [System.Compiler.Runtime]Microsoft.Contracts.InvalidContractException::.ctor(string)
      IL_0103:  throw
      IL_0104:  leave      IL_0109
    }  // end handler
    IL_0109:  ldstr      "Postcondition violated from method 'Test7.Login(Sy"
    + "stem.Int32)'"
    IL_010e:  newobj     instance void [System.Compiler.Runtime]Microsoft.Contracts.EnsuresException::.ctor(string)
    IL_0113:  throw
    IL_0114:  nop
    IL_0115:  leave      IL_011e
  }  // end .try
  catch [System.Compiler.Runtime]Microsoft.Contracts.ContractMarkerException
  {
    IL_011a:  stloc.s    V_10
    IL_011c:  rethrow
  }  // end handler
  IL_011e:  nop
  IL_011f:  ret
} // end of method Test7::Login

In the code above I've indicated the real IL code for the method's body with italic formatting. The code in gray is the code we expect to see because of the postcondition ensures statement. The code displayed in purple contains an unknown precondition which was not explicitly introduced in our code, thus it has to be part of the invariant checking. This basic piece of code is the same we saw earlier with the get_Total IL code and is basically this:

  .try
  {
    .try
    {
      IL_0000:  ldarg.0
      IL_0001:  call       instance class [System.Compiler.Runtime]Microsoft.Contracts.Guard modopt([System.Compiler.Runtime]Microsoft.Contracts.NonNullType) Test7::get_FrameGuard()
      IL_0006:  call       instance bool [System.Compiler.Runtime]Microsoft.Contracts.Guard::get_CanStartWriting()
      IL_000b:  brfalse    IL_0015
      IL_0010:  leave      IL_0048
      IL_0015:  leave      IL_003d
    }  // end .try
    catch [mscorlib]System.Exception
    {
      IL_001a:  stloc.0
      IL_001b:  ldstr      "Exception occurred during evaluation of preconditi"
      + "on in method 'Test7.Login(System.Int32)'"
      IL_0020:  ldloc.0
      IL_0021:  newobj     instance void [System.Compiler.Runtime]Microsoft.Contracts.InvalidContractException::.ctor(string,
                                                                                                                      class [mscorlib]System.Exception)
      IL_0026:  throw
      IL_0027:  leave      IL_003d
    }  // end handler
    catch [mscorlib]System.Object
    {
      IL_002c:  stloc.1
      IL_002d:  ldstr      "Exception occurred during evaluation of preconditi"
      + "on in method 'Test7.Login(System.Int32)'"
      IL_0032:  newobj     instance void [System.Compiler.Runtime]Microsoft.Contracts.InvalidContractException::.ctor(string)
      IL_0037:  throw
      IL_0038:  leave      IL_003d
    }  // end handler
    IL_003d:  ldstr      "Precondition violated from method 'Test7.Login(Sys"
    + "tem.Int32)'"
    IL_0042:  newobj     instance void [System.Compiler.Runtime]Microsoft.Contracts.RequiresException::.ctor(string)
    IL_0047:  throw
    IL_0048:  nop
    IL_0049:  leave      IL_0051
  }  // end .try
  catch [System.Compiler.Runtime]Microsoft.Contracts.ContractMarkerException
  {
    IL_004e:  stloc.2
    IL_004f:  rethrow
  }  // end handler
  IL_0051:  nop

You can read this as: "Based on the frame guard, we make sure we can start writing to the object. If this is not the case, just throw a precondition RequiresException.". It's clear that the get_CanStartWriting is in relation to the StartWritingTransitively and the EndWritingTransitively methods on the guard.

  IL_0052:  ldarg.0
  IL_0053:  call       instance class [System.Compiler.Runtime]Microsoft.Contracts.Guard modopt([System.Compiler.Runtime]Microsoft.Contracts.NonNullType) Test7::get_FrameGuard()
  IL_0058:  call       instance class [System.Compiler.Runtime]Microsoft.Contracts.Guard [System.Compiler.Runtime]Microsoft.Contracts.Guard::StartWritingTransitively()


...

  IL_00bf:  ldloc.3
  IL_00c0:  call       instance void [System.Compiler.Runtime]Microsoft.Contracts.Guard::EndWritingTransitively()

<PermissionToRead Groups="Geeks">

Why is this extra precondition (see purple colored code above) introduced automatically on any public method? Simply put, it's just there to make sure no two exposes can happen at the same time. The extra precondition makes sure that an exposed object can't be re-exposed by another call to expose. As the documentation states:

Exposing an object is not idempotent. That is, it is a checked run-time error if expose (o) . . . is reached when o is already exposed. In this way, the expose mechanism is similar to thread-non-reentrant mutexes in concurrent programming, where monitor invariants [34] are the analog of our object invariants. If exposing were idempotent, then one would not be able to rely on the object invariant to hold immediately inside an expose block, in the same way that the idempotence of thread-reentrant mutexes means that one cannot rely on the monitor invariant to hold at the time the mutex is acquired.

Idempotence (yes, with -de- at the beginning) means you can apply the same operation on a given object more than once but applying it more than once won't have further effects. This default precondition is called the IsConsistent check and can be introduced explicitly as follows:

public ... SomeMethod(...)
requires this.IsConsistent;
{
   ...
}

Consistency means that the object is in a steady state which is the same as the postcondition of the constructor. Right after creating the object, the steady state is taken for granted. Now, assume we need to make our class implementation more structured by using a helper method to change the internal state during an exposed phase. This means the consistency check should not occur on this method because it will fail. An example to clarify:

public void Update()
{
   expose(this)
   {
      somevar++;
      Helper();
      someothervar--;
   }
}

Assume the invariant states that the sum of somevar and someothervar should stay the same. It's clear that when calling Helper this condition won't be true. Therefore, you need to declare the helper with a precondition of the object being mutable, as follows:

public void Helper()
requires this.IsMutable;
{
   ...
}

</PermissionToRead>

So, I guess it's clear the the Start... and End... methods are the translation of the curly braces of the expose(this) statement. I won't cover exposing objects in more detail anymore in this post, but I want to refer to the documentation for some interesting comments on the use of class frames and the use of the expose keyword in combination with a special keyword upto in special cases with class hierarchies.

Now, we've not seen the CheckInvariant method being called somewhere over here, have we? So, where does the actual check happen if we leave the expose-block? The answer can be found in the guard's initialization code which can be found in the IL for the constructor of our class:

.method public hidebysig specialname rtspecialname
        instance void  .ctor(int32 n) cil managed
{
  // Code size       101 (0x65)
  .maxstack  8
  .locals init (int32 V_0,
           class [System.Compiler.Runtime]Microsoft.Contracts.ContractMarkerException V_1)
  IL_0000:  ldarg.0
  IL_0001:  ldarg.1
  IL_0002:  stloc.0
  IL_0003:  ldarg.0
  IL_0004:  ldloc.0
  IL_0005:  stfld      int32 Test7::total
  IL_000a:  ldloc.0
  IL_000b:  stfld      int32 Test7::offline
  IL_0010:  ldarg.0
  IL_0011:  ldc.i4.0
  IL_0012:  stfld      int32 Test7::online
  IL_0017:  ldarg.0
  IL_0018:  ldarg.1
  IL_0019:  newarr     [mscorlib]System.Boolean
  IL_001e:  stfld      bool[] modopt([System.Compiler.Runtime]Microsoft.Contracts.NonNullType) Test7::state
  IL_0023:  ldarg.0
  IL_0024:  call       instance void [mscorlib]System.Object::.ctor()
  .try
  {
    IL_0029:  ldarg.0
    IL_002a:  ldarg.0
    IL_002b:  ldftn      instance void Test7::InitGuardSets()  //function pointer for initialization method
    IL_0031:  newobj     instance void [System.Compiler.Runtime]Microsoft.Contracts.InitGuardSetsDelegate::.ctor(object,
                                                                                                                 native int)  //initialization of the InitGuardSetsDelegate
    IL_0036:  ldarg.0
    IL_0037:  ldftn      instance bool Test7::CheckInvariant(bool)  //function pointer for invariant checking method
    IL_003d:  newobj     instance void [System.Compiler.Runtime]Microsoft.Contracts.CheckInvariantDelegate::.ctor(object,
                                                                                                                  native int)  //initialization of the CheckInvariantDelegate
    IL_0042:  newobj     instance void [System.Compiler.Runtime]Microsoft.Contracts.Guard::.ctor(class [System.Compiler.Runtime]Microsoft.Contracts.InitGuardSetsDelegate,
                                                                                                 class [System.Compiler.Runtime]Microsoft.Contracts.CheckInvariantDelegate)  //initialization of the guard
    IL_0047:  stfld      class [System.Compiler.Runtime]Microsoft.Contracts.Guard Test7::'SpecSharp::frameGuard'
    IL_004c:  leave      IL_0059
  }  // end .try
  catch [System.Compiler.Runtime]Microsoft.Contracts.ContractMarkerException
  {
    IL_0051:  stloc.1
    IL_0052:  rethrow
    IL_0054:  leave      IL_0059
  }  // end handler
  IL_0059:  ldarg.0
  IL_005a:  call       instance class [System.Compiler.Runtime]Microsoft.Contracts.Guard modopt([System.Compiler.Runtime]Microsoft.Contracts.NonNullType) Test7::get_FrameGuard()
  IL_005f:  call       instance void [System.Compiler.Runtime]Microsoft.Contracts.Guard::EndWriting()
  IL_0064:  ret
} // end of method Test7::.ctor

You can complete the story yourself I guess... Using the delegates, the guard calls the method to check the invariant when leaving the expose block (through a call of EndWritingTransitively). As a code guru, you certainly want to make sure this works by messing around in the code. As an example, change the Login method as follows:

   public void Login(int i)
   ensures 0 <= i && i < Total;
   {
      expose(this)
      {
         state[i] = true;
         online++;
//         offline--;
      }
   }

and try to compile and run. The result is this:

C:\temp\specsharp\test>test7

Unhandled Exception: Microsoft.Contracts.ObjectInvariantException: Object invari
ant does not hold.
   at Test7.CheckInvariant(Boolean throwException)
   at Microsoft.Contracts.Guard.EndWriting(Boolean transitively, Boolean reflexi
vely)
   at Microsoft.Contracts.Guard.EndWriting()
   at Test7..ctor(Int32 n)
   at Test7.Main()

So it really works as we expected. Notice that Boogie can statically detect problems with invariants too, at compile-time. Some experiments with Boogie can be useful, either through the command-line or using the integrated Visual Studio support.

<PermissionToRead Groups="Geeks">

Why doesn't Spec# use the scope of a method declaration as the expose-scope? Well, because that doesn't work in case of re-entrance. Assume you're in method B of an object of type A and it's exposing "this" automatically, which means the invariant can be temporarily broken. Now imagine a call to another object C that has a reference to the object of type A that has been exposed, like this:

class A
{
   C c;

   public A()
   {
      c = new C(this);
   }

   public void B()
   { //assume begin expose(this)
      c.Do();
   } //asume end expose(this)
}

class C
{
   A a;

   public C(A a)
   {
      this.a = a;
   }

   public void Do()
   {
      //assume a.<SomeMethod> is called in here
   }
}

In such a case the invisibility of intermediate state to the client is broken. Also the indivisibility of the operation inside (the implicit) expose itself is broken. So, the default of expose(this) should not be applied to a whole method by default. Instead we want to have finer grained scopes and to have the possibility to use something else than "this".

What about composite objects? Likely you'll be defining classes that rely on other classes to store information in. An example is a CookieCollection for a web application that uses a Hashtable internally to store its data in. Let's show the skeleton of this:

class CookieCollection
{
   Hashtable cookies;

   public void Add(string name, string val)
   {
      expose(this)
      {
         //stuff
         cookies.Add(name, val);
         //stuff
      }
   }
}

Okay, the expose(this) block makes sure (together with the IsConsistent implicit precondition) our object itself (a CookieCollection object that is) is consistent, but how can we be sure that the embedded Hashtable cookies is consistent too? What about a possible leak of the Hashtable?

class CookieCollection
{
   Hashtable cookies;

   public void Add(string name, string val)
   {
      expose(this)
      {
         //stuff
         cookies.Add(name, val);
         //stuff
      }
   }

   public Hashtable InternalTable
   {
      get
      {
         return cookies;
      }
   }

}

or what if we just pass the Hashtable to the constructor of our CookieCollection object? In that case, we certainly don't have any guarantee about the consistency of the embedded object "cookies". Why is this? Well, just because the client can modify the collection externally. In order to solve this, Spec# introduces the concept of ownership, which means the owner is in control of the object. By introducing an owned object in a class definition, as follows

class CookieCollection
{
   [Owned]
   Hashtable cookies;

   public void Add(string name, string val)
   {
      expose(this)
      {
         //stuff
         cookies.Add(name, val);
         //stuff
      }
   }

   public Hashtable InternalTable
   {
      get
      {
         return cookies;
      }
   }
}

we introduce consistency dependencies. What this means is that the CookieCollection can only be consistent if the embedded owned objects (in this case the cookies Hashtable) are consistent too. When working with ownership, the expose block has extra semantics:

expose(this)
{ //we give up all ownership of owned objects
   ...
} //now we re-obtain ownership of the relinquished ownership objects

This is the so-called exposure protocol. Read the following five times to understand this: If the owner is consistent, all embedded objects are consistent too and they are committed which means they are locked and nobody else can modify them. When the owner does expose itself, it becomes mutable. In that stage we're also sure about the consistency of the owned objects (which were locked) so we can start to manipulate these. The expose-block "releases" these owned objects so that these become mutable. When the change is made, the owned objects will be consistent again (because of the postconditions on these objects), so it's safe to commit the owned objects and lock these. By doing so, we're guaranteed to be consistent ourselves too and we stop the exposure, being committed again.

This means that someone who has a reference to an internal object, he/she can't expose it because he/she doesn't own it. That means someone else cannot unlock it, thus cannot modify it after all. In the end, the concept of ownership leads to ownership trees, which I won't discuss in detail right now.

</PermissionToRead>

Hope you enjoy Spec#. It has been a long post for me to write, hopefully it was worth the effort :-).

Del.icio.us | Digg It | Technorati | Blinklist | Furl | reddit | DotNetKicks

Filed under:

Comments

No Comments