August 2005 - Posts

Check it out over here: http://msdn.microsoft.com/library/default.asp?url=/library/en-us/dnbda/html/SOADesign.asp and http://msdn.microsoft.com/library/default.asp?url=/library/en-us/dnbda/html/SOADesignVer.asp. Nice to read, based on earlier webcasts.Del.icio.us | Digg It | Technorati | Blinklist | Furl | reddit | DotNetKicks

Take a look at this. In my very opinion, this Andy Martin guy hasn't ever written a piece of code nor dos he know about complexity of software nowadays. In fact, I want to quote the book "Exploiting software" by Hoglund and McGraw, Addison Wesley, 2004 on page 14 about "The Trinity of Trouble":

The number of bugs per thousand lines of code (KLOC) varies from system to system. Estimates are anywhere between 5 to 50 bugs per KLOC. Even a system that has undergone rigorous quality assurance (QA) testing will still contain bugs - around five bugs per KLOC. A software system that is only feature tested, like most commercial software, will have many more bugs - around 50 per KLOC [Voas and McGraw, 1999]. Most software products fall into the latter category.

Actually, I want to stress the fact that the latter sentence is based on research from 1999 and I do strongly believe that thanks to the "Trustworthy Computing Statement" by Microsoft and the various security pushes, things are becoming better. But let's continue.

To give you an idea of how much software lives within complex machinery, consider the following:

Lines of Code   System

400,000         Solaris 7
17 million      Netscape
40 million      Space Station
10 million      Space Shuttle
7 million       Boeing 777
35 million      NT5
1.5 million     Linux
3 million       Windows 3.1
<5 million      Windows 95
40 million      Windows XP

(...) One simple but unfortunate fact holds true for software: more lines, more bugs.

Now allow me to give you some up-to-date information about some products (source Secunia):

 
 
 
 
 
 
 
 
 
 

These are just some figures, live from Secunia but it gives some relevant information in my opinion. I know figures are risky things, so I do expect to get a lot of feedback :-). Also check out Steve Riley's Secunia dashboard on http://www.steveriley.ms/sbr/default.aspx.

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

That's the paraphrased summary of a mail I received yesterday... :-). Let me give a very short answer: read this stuff, check out the C# 3.0 stuff which is due to be made public later this year at the PDC in LA and you'll get an aha erlebnis. And watch the Channel 9 video with Anders Hejlsberg on Programming data in C# 3.0.

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

Come on guys, put yourself out there on http://myguestmap.lorca.eti.br/guestmap.jsp?id=c9&locale=en. Who will implement a MapPoint driven equivalent btw?Del.icio.us | Digg It | Technorati | Blinklist | Furl | reddit | DotNetKicks

Because of a low on disk space condition I just needed to move the .mdb and .stm files of the Exchange stores on a server I manage to another disk (partition). This KB article was extremely helpful to change the original paths to the new paths inside the Active Directory configuration partition: http://support.microsoft.com/?kbid=822676.

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

Since a couple of weeks now I'm involved in a SharePoint development project for a local company based in Belgium. Dedicated to this topic, I've create a post category called "IW stuff - Office, SharePoint, IBF" where I'll post some useful information in. Today I'll kick off with a very simple piece of code to obtain a collection of the lists on a Windows SharePoint Services site using the SharePoint Web Services.

First of all, if you've not done so yet, please download the SharePoint Products and Technologies 2003 SDK over here. This API contains a single chm file called spptsdk.chm with a lot of documentation in it. You'll certainly find this useful (I, as a SharePoint development newbie, do).

SharePoint provides a series of web services that can be used to interact with a SharePoint-driven website for administration and management tasks. I grabbed the following table directly from the API:

Service Description
Administration Provides methods for managing a deployment ofWindows SharePoint Services, such as for creating or deleting sites.
Alerts Provides methods for working with alerts for list items in a SharePoint site.
Document Workspace Exposes the Document Workspace Web service and its eleven methods for managing Document Workspace sites and the data they contain.
Forms Provides methods for returning forms used in the user interface when working with the contents of a list.
Imaging Provides methods that enable you to create and manage picture libraries.
List Data Retrieval Provides a method for performing queries against lists in Microsoft Windows SharePoint Services.
Lists Provides methods for working with lists and list data.
Meetings Provides methods that enable you to create and manage Meeting Workspace sites.
Permissions Provides methods for working with the permissions for a site or list.
Site Data Provides methods that return metadata or list data from sites or lists in Microsoft Windows SharePoint Services.
Sites Provides a method for returning information about the site templates for a site collection.
Users and Groups Provides methods for working with users, site groups, and cross-site groups.
Versions Provides methods for working with file versions.
Views Provides methods for working with views of lists.
Web Part Pages Provides the methods to send information to and retrieve information from XML Web services.
Webs Provides methods for working with sites and subsites.

As I'm currently interested in the Lists stuff, I'll focus on this in this first SharePoint-related post. On my development machine, I created a http://sharepointdev website for all of my experiments. The web services can be found in the _vti_bin folder which is actually a virtual directory to the %programfiles%\Common Files\Microsoft Shared\Web Server Extensions\60\isapi folder on your system. You won't find very useful information in the .asmx files over there, as these are just stubs for a code-behind implementation, but it's nice to know where these files physically reside on the system. Now, go to Visual Studio .NET and add a Web Reference to http://sharepointdev/_vti_bin/Lists.asmx (well, do substitute the host part of the URL as needed of course). Over here, I'm using a Windows Forms C# project to visualize the data as a first test. The following code assumes there is a DataGrid control on the form (Dock = Fill) named "dataGrid1":

//
//Create the proxy object
//
sharepointdev.Lists l = new
sharepointdev.Lists();

//
//Integrated Windows authentication credentials
//
l.Credentials = CredentialCache.DefaultCredentials;

//
//Query the service for a collection of lists
//
XmlNode node = l.GetListCollection();

//
//Create a reader to populate a DataSet
//
XmlTextReader r = new XmlTextReader(node.OuterXml, XmlNodeType.Document, null
);

//
//Create a DataSet and populate it using the constructed XmlReader
//
DataSet ds = new
DataSet();
ds.ReadXml(r);

//
//For sake of demo, just bind the DataSet's first (and only) table to a DataGrid control
//
dataGrid1.DataSource = ds.Tables[0];

What this does is pretty basic: it just populates a DataSet with information about the lists on the SharePoint website. Not so exciting but nevertheless pretty cool as a first SharePoint Web Services development adventures sample. I already have some nice ideas to interact with SharePoint through these services. Check out my "IW stuff - Office, SharePoint, IBF" blog post category regularly to keep on track!

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

Sriram Krishnan blogs about using the anonymous delegates in C# 2.0 to implement a form of currying in C#. You can find it over here: http://blogs.msdn.com/sriram/archive/2005/08/07/448722.aspx. I guess this deserves a little (???) explanation...

So first, what are these anonymous delegates? Let's show a little example of this. We'll start with C# 1.x code:

using System;
using System.Threading;

class Demo
{
   public void Do()
   {
      //thread's background work code
   }

   public static void Main()
   {
      Thread t = new Thread(new ThreadStart(Do));
      t.Start();
      //...
   }
}

This piece of code uses the ThreadStart delegate to point to function Do in order to create a thread that can be started for background processing of the method Do. You can think of similar examples with event handlers for various kinds of objects (e.g. a FileSystemWatcher, a Button control, etc). The point I want to make is that you really need an existing method to point at in order to instantiate the delegate. So, we need to have a method Do that matches the signature of the Do delegate, which is: void return type + no parameters.

In C# 2.0 it's allowed to do the following:

using System;
using System.Threading;

class Demo
{
   public static void Main()
   {
      Thread t = new Thread(
        
new ThreadStart(
            delegate () {
                //thread's background work code
            }
         )
      );

      t.Start();
      //...
   }
}

or even this

using System;
using System.Threading;

class Demo
{
   public static void Main()
   {
      Thread t = new Thread(
         delegate () {
             //thread's background work code
         }
      );

      t.Start();
      //...
   }
}

This is just a very simple example to show the basic idea of these anonymous delegates. For the full syntactical sugar, check out the C# 2.0 Specification documents. More interesting for us is the underlying IL to see how this works. We'll kick off with the classic Thread t = new Thread(new ThreadStart(Do)); approach's IL compilation result.

<Note>
Yesterday I received a comment of an interested reader on my IL adventures asking to dive a little deeper into the meaning of the various instructions. In this post I aim to do so, but for geeks I want to recommend the book
"The Common Language Infrastructure Annotated Standard" part "6. Partition III: CIL instruction Set" pages 473-600.
</Note>

.method public hidebysig static void  Main() cil managed
{
  .entrypoint
  // Code size       24 (0x18)
  .maxstack  8
  IL_0000:  ldnull                                                                                                           //load null, used for further newobj call that requires two parameters of which we only use one
  IL_0001:  ldftn      void AnonDel::Do()                                                                                    //Thread t = new Thread(new ThreadStart(Do));
  IL_0007:  newobj     instance void [mscorlib]System.Threading.ThreadStart::.ctor(object,
                                                                                   native int)                               //Thread t = new Thread(new ThreadStart(Do));
  IL_000c:  newobj     instance void [mscorlib]System.Threading.Thread::.ctor(class [mscorlib]System.Threading.ThreadStart)  //Thread t = new Thread(new ThreadStart(Do));
  IL_0011:  call       instance void [mscorlib]System.Threading.Thread::Start()                                              //t.Start();
  IL_0016:  nop
  IL_0017:  ret
} // end of method AnonDel::Main

Next, consider the alternative C# approach using the new Thread(delegate() {Console.WriteLine("Test");}).Start(); syntax:

.method public hidebysig static void  Main() cil managed
{
  .entrypoint
  // Code size       43 (0x2b)
  .maxstack  8
  IL_0000:  ldsfld     class [mscorlib]System.Threading.ThreadStart AnonDel::'<>9__CachedAnonymousMethodDelegate1'          //load ThreadStart delegate from field <>9_CachedAnonymousDelegate1
  IL_0005:  brtrue.s   IL_001a                                                                                              //do we have the delegate instance already? if yes, continue at IL_001a; otherwise, fall through
  IL_0007:  ldnull                                                                                                          //null value needed for further constructor call with non-used parameter
  IL_0008:  ldftn      void AnonDel::'b__0'()                                                                               //load function pointer to b__0 (aha, there still is a function pointer)
  IL_000e:  newobj     instance void [mscorlib]System.Threading.ThreadStart::.ctor(object,
                                                                                   native int)                              //instantiate the ThreadStart delegate using the function pointer
  IL_0013:  stsfld     class [mscorlib]System.Threading.ThreadStart AnonDel::'<>9__CachedAnonymousMethodDelegate1'          //store the instance in the <>9_CachedAnonymousDelegate1 field
  IL_0018:  br.s       IL_001a                                                                                              //up to the next statement
  IL_001a:  ldsfld     class [mscorlib]System.Threading.ThreadStart AnonDel::'<>9__CachedAnonymousMethodDelegate1'          //load ThreadStart delegate from field <>9_CachedAnonymousDelegate1
  IL_001f:  newobj     instance void [mscorlib]System.Threading.Thread::.ctor(class [mscorlib]System.Threading.ThreadStart) //create a new Thread instance using our ThreadStart instance
  IL_0024:  call       instance void [mscorlib]System.Threading.Thread::Start()                                             //and finally, start the thread
  IL_0029:  nop
  IL_002a:  ret
} // end of method AnonDel::Main

The stsfld and ldsfld instructions are used to store to and load from a field respectively. The field being used in the code above is the following one:

.field private static class [mscorlib]System.Threading.ThreadStart '<>9__CachedAnonymousMethodDelegate1'

As you can see, there still is a method called b__0 that's being passed to the ThreadStart constructor. This method's IL is the following:

.method private hidebysig static void  'b__0'() cil managed
{
  // Code size       12 (0xc)
  .maxstack  8
  IL_0000:  ldstr      "Test"
  IL_0005:  call       void [mscorlib]System.Console::WriteLine(string)
  IL_000a:  nop
  IL_000b:  ret
} // end of method AnonDel::'b__0'

No tricks involved over here...

Now, what's a closure? Allow me to point to some useful resources for this, being Martin Fowler's blog and Wikipedia. Simply stated, a closure is a way to pass a piece of code as an argument to a function in order to use it over there for further processing. But there's more, as a closure in its strict meaning can be parameterized, meaning that you can do something like this (however, see further - also marked in red -, anonymous methods are not closures but to some extent they have the feeling to be closures):

Adder CreateAdder(int a)
{
   return delegate(int b) { return a + b; };
}

This way, you can call the CreateAdder method and construct a parameterized piece of code that's returned through a delegate for further usage. For example:

Adder f = CreateAdder(2);
for (int i = 0; i < 10; i++)
   Console.Write("{0} ", f(i));

will print:

2 3 4 5 6 7 8 9 10 11

This is still pretty straightforward, but assume the following:

Accumulator CreateAccumulator(int start)
{
   int sum = start;
   return delegate(int b) { sum += b; return sum; };
}

Now, without compiling, try to guess what will appear on the screen using this code:

Accumulator g = CreateAccumulator(2);
for (int i = 0; i < 10; i++)
   Console.Write("{0} ", g(i));

If you think you've found out, here's the complete code which you can compile with C# 2.0:

using System;

class Accu
{
   delegate RETURN Adder(PARAM a);
   delegate RETURN Accumulator(PARAM a);

   static Adder CreateAdder(int a)
   {
      return delegate(int b) { return a + b; };
   }

   static Accumulator CreateAccumulator(int start)
   {
      int sum = start;
      return delegate(int b) { sum += b; return sum; };
   }

   public static void Main()
   {
      Adder f = CreateAdder(2);
      for (int i = 0; i < 10; i++)
         Console.Write("{0} ", f(i));

      Console.WriteLine();

      Accumulator g = CreateAccumulator(2);
      for (int i = 0; i < 10; i++)
         Console.Write("{0} ", g(i));
   }
}

As an addition, you can use generics on the methods CreateAdder and CreateAccumulator too in order to specify the type of the underlying Adder and Accumulator. Try this as a little exercise :-). The application as shown above should produce the following output:

C:\temp>accu
2 3 4 5 6 7 8 9 10 11
2 3 5 8 12 17 23 30 38 47

So, as you can see, the second row of numbers is really accumulating (an even better example would be a demo of the mathematical faculty operator "!", which just requires a little change in the code, try it yourself).

What's import to see however is that we have returned an anonymous delegate but we need to keep track of the sum variable, so where is this hold? The answer is that at runtime a heap-allocated frame is constructed to hold all of the data needed for that frame (called an "activation").

To keep good habits going on, let's dive into the IL behind this little sample application to see what's going on. We'll start with the Main method, shown below an annotated in green:

.method public hidebysig static void  Main() cil managed
{
  .entrypoint
  // Code size       101 (0x65)
  .maxstack  3
  .locals init (class Accu/'Adder`2' V_0,                                         //place to hold local variable for the adder
           int32 V_1,                                                             //counter value for loop --> for (int i = 0; i < 10; i++)
           class Accu/'Accumulator`2' V_2,                                        //place to hold local variable for the accumulator
           bool V_3)                                                              //condition check boolean value for loop --> for (int i = 0; i < 10; i++)
  IL_0000:  ldc.i4.2                                                              //Adder = CreateAdder(2)
  IL_0001:  call       class Accu/'Adder`2' Accu::CreateAdder(int32)              //Adder = CreateAdder(2)
  IL_0006:  stloc.0                                                               //Adder = CreateAdder(2)
  IL_0007:  ldc.i4.0                                                              //for (int i = 0; i < 10; i++)
  IL_0008:  stloc.1                                                               //for (int i = 0; i < 10; i++)
  IL_0009:  br.s       IL_0026                                                    //jump to loop condition check
  IL_000b:  ldstr      "{0} "                                                     //Console.WriteLine("{0} ", f(i));
  IL_0010:  ldloc.0                                                               //Console.WriteLine("{0} ", f(i));
  IL_0011:  ldloc.1                                                               //Console.WriteLine("{0} ", f(i));
  IL_0012:  callvirt   instance !1 class Accu/'Adder`2'::Invoke(!0)               //Console.WriteLine("{0} ", f(i));
  IL_0017:  box        [mscorlib]System.Int32                                     //boxing of int parameter
  IL_001c:  call       void [mscorlib]System.Console::Write(string,
                                                            object)               //Console.WriteLine("{0} ", f(i));
  IL_0021:  nop
  IL_0022:  ldloc.1                                                               //for (int i = 0; i < 10; i++) ==> for (int i = 0; i < 10; i = i + 1)
  IL_0023:  ldc.i4.1                                                              //for (int i = 0; i < 10; i++) ==> for (int i = 0; i < 10; i = i + 1)
  IL_0024:  add                                                                   //for (int i = 0; i < 10; i++) ==> for (int i = 0; i < 10; i = i + 1)
  IL_0025:  stloc.1                                                               //for (int i = 0; i < 10; i++) ==> for (int i = 0; i < 10; i = i + 1)
  IL_0026:  ldloc.1                                                               //for (int i = 0; i < 10; i++)
  IL_0027:  ldc.i4.s   10                                                         //for (int i = 0; i < 10; i++)
  IL_0029:  clt                                                                   //for (int i = 0; i < 10; i++)
  IL_002b:  stloc.3                                                               //store boolean value for i < 10 --> for (int i = 0; i < 10; i++)
  IL_002c:  ldloc.3                                                               //load boolean value for i < 10 --> for (int i = 0; i < 10; i++)
  IL_002d:  brtrue.s   IL_000b                                                    //loop, goto next round
  IL_002f:  call       void [mscorlib]System.Console::WriteLine()                 //Console.WriteLine();
  IL_0034:  nop
  IL_0035:  ldc.i4.2
  IL_0036:  call       class Accu/'Accumulator`2' Accu::CreateAccumulator(int32)
  IL_003b:  stloc.2
  IL_003c:  ldc.i4.0
  IL_003d:  stloc.1
  IL_003e:  br.s       IL_005b
  IL_0040:  ldstr      "{0} "
  IL_0045:  ldloc.2
  IL_0046:  ldloc.1
  IL_0047:  callvirt   instance !1 class Accu/'Accumulator`2'::Invoke(!0)
  IL_004c:  box        [mscorlib]System.Int32
  IL_0051:  call       void [mscorlib]System.Console::Write(string,
                                                            object)
  IL_0056:  nop
  IL_0057:  ldloc.1
  IL_0058:  ldc.i4.1
  IL_0059:  add
  IL_005a:  stloc.1
  IL_005b:  ldloc.1
  IL_005c:  ldc.i4.s   10
  IL_005e:  clt
  IL_0060:  stloc.3
  IL_0061:  ldloc.3
  IL_0062:  brtrue.s   IL_0040
  IL_0064:  ret
} // end of method Accu::Main

No magic going on in here, we're just calling the Create* methods with the right parameters (the explanation for lines IL_0035 to IL_0062 is completely analogue to the explanation of lines IL_0000 to IL_002f). Let's concentrate on the Accumulator now, so open up the CreateAccumulator static method. Remember that on entry of this method we have one argument passed in (see IL_0000 of Main's IL).

.method private hidebysig static class Accu/'Accumulator`2'
        CreateAccumulator(int32 start) cil managed
{
  // Code size       30 (0x1e)
  .maxstack  3
  .locals init (class Accu/'<>c__DisplayClass4' V_0,                                              //place to keep the instance of <>c__DisplayClass4 (see further)
           class Accu/'Accumulator`2' V_1)                                                        //place to keep the instance of Accumulator`2 (see further)
  IL_0000:  newobj     instance void Accu/'<>c__DisplayClass4'::.ctor()                           //create an instance of <>c__DisplayClass4; no parameters needed
  IL_0005:  stloc.0                                                                               //store the instance of <>c__DisplayClass4 in the .locals' V_0 reserved space
  IL_0006:  ldloc.0                                                                               //load the instance of <>c__DisplayClass4 from the .local' V_0 reserved space
  IL_0007:  ldarg.0                                                                               //load the argument passed in to the CreateAccumulator method (see IL_0000 of Main)
  IL_0008:  stfld      int32 Accu/'<>c__DisplayClass4'::sum                                       //store the argument (on top of the stack, see IL_0007) to the <>c__DisplayClass4 class' sum field
  IL_000d:  ldloc.0                                                                               //load the instance of <>c__DisplayClass4 from the .local' V_0 reserved space
  IL_000e:  ldftn      instance int32 Accu/'<>c__DisplayClass4'::'b__3'(int32)                    //load function pointer to the b__3 method of <>c__DisplayClass4
  IL_0014:  newobj     instance void class Accu/'Accumulator`2'::.ctor(object,
                                                                                    native int)   //create an instance of Accumulator`2 which is a delegate
  IL_0019:  stloc.1                                                                               //store the instance of Accumulator`2 in the .local' V_1 reserved space
  IL_001a:  br.s       IL_001c                                                                    //just go on to the next statement
  IL_001c:  ldloc.1                                                                               //load the instance of Accumulator`2 from the .local' V_1 reserved space
  IL_001d:  ret
} // end of method Accu::CreateAccumulator

So, which code do we recognize in here? Remember the original code was the following:

   static Accumulator CreateAccumulator(int start)
   {
      int sum = start;
      return delegate(int b) { sum += b; return sum; };
   }

On line IL_0008 we find the sum variable field that's being hold by the <>c_DisplayClass4 class:

.field public int32 sum

The code on line IL_0007 simply stores the argument (start) to that location, which clearly is the translation of the line

      int sum = start;

In IL_001d we return what was loaded in line IL_001c, i.e. the V_1 local of type Accumulator`2'. The initialization of this object happens in line IL_0014 based on two parameters: one is the <>c__DisplayClass4 instance and the other one is a pointer to the function b__3 on that same instance. So, what we have is a class called <>c__DisplayClass4 that wraps the sum variable and the logic that's found in:

      return delegate(int b) { sum += b; return sum; };

The rest of CreateAccumulator's code is straightforward. So, what's up in that strange <>c__DisplayClass4 thing? First of all we have a field:

.field public int32 sum

Second, there is a simple constructor without parameters (not displayed in here). Third, there's the method IL for the anonymous delegate used in our code, stored in b__3:

.method public hidebysig instance int32  'b__3'(int32 b) cil managed
{
  // Code size       25 (0x19)
  .maxstack  3
  .locals init (int32 V_0)                                   //place to hold return value for the function temporarily
  IL_0000:  ldarg.0                                          //load the argument of the function call --> delegate(int b)
  IL_0001:  dup                                              //duplicate the argument; we'll need it more than once
  IL_0002:  ldfld      int32 Accu/'<>c__DisplayClass4'::sum  //load the current value of the sum field --> sum += b ==> sum = sum + b
  IL_0007:  ldarg.1                                          //get our (duplicated) argument --> sum += b ==> sum = sum + b
  IL_0008:  add                                              //add the argument and the sum --> sum += b ==> sum = sum + b
  IL_0009:  stfld      int32 Accu/'<>c__DisplayClass4'::sum  //store the result in the sum field --> sum += b ==> sum = sum + b
  IL_000e:  ldarg.0                                          //get our argument
  IL_000f:  ldfld      int32 Accu/'<>c__DisplayClass4'::sum  //load the current value of the sum field (contains accumulated value)
  IL_0014:  stloc.0                                          //store the sum to .local V_0
  IL_0015:  br.s       IL_0017                               //just continue
  IL_0017:  ldloc.0                                          //load the V_0 value --> return sum;
  IL_0018:  ret                                              //return sum;
} // end of method '<>c__DisplayClass4'::'b__3'

Pretty clear I hope? Last but not least, what about the Accumulator`2' class? To show this, open up the MetaInfo view for the assembly using CTRL-M.

<Intermezzo>
Readers of "Applied .NET Framework Programming" (J. Richter) will remember the ildasm.exe /Adv hook to show the View, MetaInfo, Show (CTRL-M) menu in ildasm.exe. When you did launch ildasm.exe without the /Adv flag (which was not mentioned in the ildasm.exe /? output btw :o), there was no way to get the meta info of the assembly. Being one of the crucial contents of an assembly, you might be interested in the assembly's metadata, so this (hidden) option might be intersting. However, in .NET v2.0 the /Adv flag is gone and the View, MetaInfo, Show (CTRL-M) menu appears always. A little mysterious has been demystified :-). Notice that the Help included with ildasm still mentiones an "advanced mode" thingie:

    Statistics (advanced mode only)    - show PE file statistics in a disassembly window
    MetaInfo (advanced mode only)
</Intermezzo>

You should find the following:

TypeDef #3 (02000004)
-------------------------------------------------------
 TypDefName: Accumulator`2  (02000004)
 Flags     : [NestedPrivate] [AutoLayout] [Class] [Sealed] [AnsiClass]  (00000103)
 Extends   : 01000002 [TypeRef] System.MulticastDelegate
 EnclosingClass : Accu (02000002)
 2 Generic Parameters
  (0) GenericParamToken : (2a000003) Name : PARAM flags: 00000000 Owner: 02000004 Kind: 02000000
   1 Constraint(s)
   01000001 
  (1) GenericParamToken : (2a000004) Name : RETURN flags: 00000000 Owner: 02000004 Kind: 02000000
   1 Constraint(s)
   01000001 

 Method #1 (06000009)
 -------------------------------------------------------
  MethodName: .ctor (06000009)
  Flags     : [Public] [HideBySig] [ReuseSlot] [SpecialName] [RTSpecialName] [.ctor]  (00001886)
  RVA       : 0x00000000
  ImplFlags : [Runtime] [Managed]  (00000003)
  CallCnvntn: [DEFAULT]
  hasThis
  ReturnType: Void
  2 Arguments
   Argument #1:  Object
   Argument #2:  I
  2 Parameters
   (1) ParamToken : (0800000a) Name : object flags: [none] (00000000)
   (2) ParamToken : (0800000b) Name : method flags: [none] (00000000)

 Method #2 (0600000a)
 -------------------------------------------------------
  MethodName: Invoke (0600000A)
  Flags     : [Public] [Virtual] [HideBySig] [NewSlot]  (000001c6)
  RVA       : 0x00000000
  ImplFlags : [Runtime] [Managed]  (00000003)
  CallCnvntn: [DEFAULT]
  hasThis
  ReturnType: Var!1
  1 Arguments
   Argument #1:  Var!0
  1 Parameters
   (1) ParamToken : (0800000c) Name : a flags: [none] (00000000)

 Method #3 (0600000b)
 -------------------------------------------------------
  MethodName: BeginInvoke (0600000B)
  Flags     : [Public] [Virtual] [HideBySig] [NewSlot]  (000001c6)
  RVA       : 0x00000000
  ImplFlags : [Runtime] [Managed]  (00000003)
  CallCnvntn: [DEFAULT]
  hasThis
  ReturnType: Class System.IAsyncResult
  3 Arguments
   Argument #1:  Var!0
   Argument #2:  Class System.AsyncCallback
   Argument #3:  Object
  3 Parameters
   (1) ParamToken : (0800000d) Name : a flags: [none] (00000000)
   (2) ParamToken : (0800000e) Name : callback flags: [none] (00000000)
   (3) ParamToken : (0800000f) Name : object flags: [none] (00000000)

 Method #4 (0600000c)
 -------------------------------------------------------
  MethodName: EndInvoke (0600000C)
  Flags     : [Public] [Virtual] [HideBySig] [NewSlot]  (000001c6)
  RVA       : 0x00000000
  ImplFlags : [Runtime] [Managed]  (00000003)
  CallCnvntn: [DEFAULT]
  hasThis
  ReturnType: Var!1
  1 Arguments
   Argument #1:  Class System.IAsyncResult
  1 Parameters
   (1) ParamToken : (08000010) Name : result flags: [none] (00000000)

The parts indicated in blog show what's relevant to us. Basically, this class is just a subclass of the MulticastDelegate BCL class, which is hidden as a private class in the Accu class and is sealed (no further inheritance possible. Note that the generic parameters are listed as well (2a000003 and 2a000004) as a translation of

   delegate RETURN Accumulator(PARAM a);

This also explains the backquote `2 inside the method name, which indicates the number of generic parameters.

Another example that can be interesting is the use of delegates to filter a list using the FindAll method. The System.Collections.Generic.List class has a method FindAll that accepts a delegate like this:

class List
{
   public List FindAll(Predicate match);
}

The generic Predicate type is a delegate with the following signature:

public delegate bool Predicate (T obj);

In the following demo we'll also use the ForEach method to do an action for every element in the list, i.e. printing the value to the screen. The signature of this delegate (Action) looks as follows:

public delegate void Action (T obj);

Let's do something cool. Assume a List filled with ints that we want to filter for prime numbers. The following code will do:

using System;
using System.Collections.Generic;

class PrimeFilter
{
   public static void Main()
   {
      List<int> l = new List<int>();

      for (int i = 2; i < 100; i++)
         l.Add(i);

      PrintList("Original values", l);

      List<int> p = l.FindAll(
         delegate (int a)
         {
            for (int i = 2; i <= Math.Sqrt(a); i++)
               if (a % i == 0)
                  return false;
            return true;
         }
      );

      PrintList("Primes", p);
   }

   private static void PrintList(string msg, List<int> l)
   {
      Console.WriteLine(msg);
      l.ForEach(
         delegate (int a)
         {
            Console.Write("{0}\t", a);
         }
      );
      Console.WriteLine();
   }
}

Note that this is a very naive implementation of prime search but it will do for the sake of the demo. Compile and run. You should see the following output:

C:\temp>primefilter
Original values
2       3       4       5       6       7       8       9       10      11
12      13      14      15      16      17      18      19      20      21
22      23      24      25      26      27      28      29      30      31
32      33      34      35      36      37      38      39      40      41
42      43      44      45      46      47      48      49      50      51
52      53      54      55      56      57      58      59      60      61
62      63      64      65      66      67      68      69      70      71
72      73      74      75      76      77      78      79      80      81
82      83      84      85      86      87      88      89      90      91
92      93      94      95      96      97      98      99
Primes
2       3       5       7       11      13      17      19      23      29
31      37      41      43      47      53      59      61      67      71
73      79      83      89      97

Well, in my very opinion this is really cool.

To be complete one quote of Brad Adams on anonymous methods versus closures (source):

Anonymous methods are not closures or completions. They are anonymous methods. They allow sharing of variables with the outer method (not copy in, or copy out, or copy in-out, or even by ref).

And indeed, that's all I've been showing in this post, but nevertheless it's cool.

Now, after writing this post for a couple of hours now (you can't believe how fast the time goes by) I won't cover the currying stuff anymore, but you can find information on http://blogs.msdn.com/sriram/archive/2005/08/07/448722.aspx as aforementioned. Currying, named after Haskell Curry (cf. Haskell), allows to transform a function with multiple parameters in a function with only the first parameter left, by kind of "instantiating the function" with the other parameters and returning the "curried function" to the caller. More information can be found on Wikepedia. Have fun with it!

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

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

Posted Tuesday, August 09, 2005 2:11 AM by bart | with no comments
Filed under:

Introduction

I just deployed a self-written request logger HTTP Module to my blogs website to have a better picture about the activity on my blog over here. Through this post, I'd like to share information with you on how to create such a logger HTTP Module.

 

What's an HTTP Module?

ASP.NET processes requests through a so-called HTTP request pipeline. A common example of such a request is browsing to an .aspx page. First of all, the request reaches the IIS machine on a some website (based on the IP and possibly a host header). In there, an ISAPI called aspnet_isapi.dll is configured for the .aspx extension, therefore sending the request to that ISAPI dll for further processing. In here, the HTTP pipeline of ASP.NET comes into play. Based on the configuration of the web server and the web application, the request is sent further to the right party for further processing. In the case of an .aspx page, the System.Web.UI.PageHandlerFactory class takes over the request for further processing.

This "further processing" is based on two principles:

  • HTTP Modules
  • HTTP Handlers

An HTTP Module can be seen as a filter (and is somewhat equivalent to an ISAPI filter). All requests pass through the configured modules before further processing is done. Samples of modules include caching, authentication, authorization modules and also a logging module as I'll show you later on.

HTTP Handlers are the equivalent of an ISAPI extension and are responsible to handle certain requests. Examples include the processing logic for .aspx, .asmx, .cs, ... files. By writing a custom HTTP Handler you can extend the ASP.NET runtime with your own logic to process certain requests. An simple example is a handler for .jpg images that supports image resizing as I explained earlier in an article of mine (http://www.microsoft.com/belux/nl/msdn/community/columns/desmet/httphandler.mspx).

In the machine.config file (%windir%\Microsoft.NET\Framework\v1.1.4322\CONFIG\machine.config) you'll find a section and that contains preconfigured HTTP Handlers and HTTP Modules, as shown below:

    <httpHandlers>
      <add verb="*" path="*.vjsproj" type="System.Web.HttpForbiddenHandler" />
      <add verb="*" path="*.java" type="System.Web.HttpForbiddenHandler" />
      <add verb="*" path="*.jsl" type="System.Web.HttpForbiddenHandler" />
      <add verb="*" path="trace.axd" type="System.Web.Handlers.TraceHandler" />
      <add verb="*" path="*.aspx" type="System.Web.UI.PageHandlerFactory" />
      <add verb="*" path="*.ashx" type="System.Web.UI.SimpleHandlerFactory" />
      <add verb="*" path="*.asmx" type="System.Web.Services.Protocols.WebServiceHandlerFactory, System.Web.Services, Version=1.0.5000.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a" validate="false" />
      <add verb="*" path="*.rem" type="System.Runtime.Remoting.Channels.Http.HttpRemotingHandlerFactory, System.Runtime.Remoting, Version=1.0.5000.0, Culture=neutral, PublicKeyToken=b77a5c561934e089" validate="false" />
      <add verb="*" path="*.soap" type="System.Runtime.Remoting.Channels.Http.HttpRemotingHandlerFactory, System.Runtime.Remoting, Version=1.0.5000.0, Culture=neutral, PublicKeyToken=b77a5c561934e089" validate="false" />
      <add verb="*" path="*.asax" type="System.Web.HttpForbiddenHandler" />
      <add verb="*" path="*.ascx" type="System.Web.HttpForbiddenHandler" />
      <add verb="GET,HEAD" path="*.dll.config" type="System.Web.StaticFileHandler" />
      <add verb="GET,HEAD" path="*.exe.config" type="System.Web.StaticFileHandler" />
      <add verb="*" path="*.config" type="System.Web.HttpForbiddenHandler" />
      <add verb="*" path="*.cs" type="System.Web.HttpForbiddenHandler" />
      <add verb="*" path="*.csproj" type="System.Web.HttpForbiddenHandler" />
      <add verb="*" path="*.vb" type="System.Web.HttpForbiddenHandler" />
      <add verb="*" path="*.vbproj" type="System.Web.HttpForbiddenHandler" />
      <add verb="*" path="*.webinfo" type="System.Web.HttpForbiddenHandler" />
      <add verb="*" path="*.asp" type="System.Web.HttpForbiddenHandler" />
      <add verb="*" path="*.licx" type="System.Web.HttpForbiddenHandler" />
      <add verb="*" path="*.resx" type="System.Web.HttpForbiddenHandler" />
      <add verb="*" path="*.resources" type="System.Web.HttpForbiddenHandler" />
      <add verb="GET,HEAD" path="*" type="System.Web.StaticFileHandler" />
      <add verb="*" path="*" type="System.Web.HttpMethodNotAllowedHandler" />
    </httpHandlers>
    <httpModules>
      <add name="OutputCache" type="System.Web.Caching.OutputCacheModule" />
      <add name="Session" type="System.Web.SessionState.SessionStateModule" />
      <add name="WindowsAuthentication" type="System.Web.Security.WindowsAuthenticationModule" />
      <add name="FormsAuthentication" type="System.Web.Security.FormsAuthenticationModule" />
      <add name="PassportAuthentication" type="System.Web.Security.PassportAuthenticationModule" />
      <add name="UrlAuthorization" type="System.Web.Security.UrlAuthorizationModule" />
      <add name="FileAuthorization" type="System.Web.Security.FileAuthorizationModule" />
      <add name="ErrorHandlerModule" type="System.Web.Mobile.ErrorHandlerModule, System.Web.Mobile, Version=1.0.5000.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a" />
    </httpModules>

Take a close look at these and try to understand what the role of each handler/module is. On a non-production box, feel free to play with these defaults.

 

Developing a custom HTTP Module

Let's take a look at the development of our logging module, step by step:

  1. Start Visual Studio .NET 2003 and create a new Class Library project in C# and give it the name WebLogger.
  2. Right click the References node in the Solution Explorer and choose Add Reference. Go to the .NET tab and select System.Web.dll (version 1.0.5000.0) and click OK.
  3. Now go to Class1.cs and change the code as follows:
using System;
using System.Configuration;
using System.Data;
using System.Data.SqlClient;
using System.Web;

namespace BdsSoft
{
   public class WebLogger : IHttpModule
   {
      //
      //Holds the connection string to the logging database
      //
      private string dsn;

      ///
      /// Default constructor. Initializes the logger with configuration read from web.config.
      ///

      public WebLogger()
      {
         //
         //Grab the connection string from in web.config
         //
         dsn = ConfigurationSettings.AppSettings["dsn"];
      }

      #region IHttpModule Members

      ///
      /// Initialization routine for the module.
      ///

      /// Context object for the current web application
      public void Init(HttpApplication context)
      {
         //
         //We're only interested in incoming requests for logging purposes
         //
         context.BeginRequest += new EventHandler(context_BeginRequest);
      }

      ///
      /// Implementation of IDisposable.
      ///

      public void Dispose()
      {
      }

      #endregion

      ///
      /// Event handler for the beginning of a web request.
      ///

      /// HttpApplication object
      /// Event arguments
      private void context_BeginRequest(object sender, EventArgs e)
      {
         //
         //Get access to the request context
         //
         HttpApplication context = sender as HttpApplication;
         
         //
         //Connect to the database
         //
         using (SqlConnection conn = new SqlConnection(dsn))
         {
            //
            //Stored procedure to insert an entry in our web log
            //
            SqlCommand cmd = new SqlCommand("InsertLogEntry", conn);
            cmd.CommandType = CommandType.StoredProcedure;

            //
            //Parameterization of the SqlCommand
            //
            cmd.Parameters.Add("@agent", SqlDbType.NVarChar, 100);
            cmd.Parameters.Add("@rawUrl", SqlDbType.NVarChar, 1000);
            cmd.Parameters.Add("@userHostAddress", SqlDbType.NVarChar, 15);
            cmd.Parameters.Add("@userHostName", SqlDbType.NVarChar, 1000);
            cmd.Parameters.Add("@httpMethod", SqlDbType.NVarChar, 10);

            //
            //Query the stuff we need and set the parameters
            //
            cmd.Parameters["@agent"].Value = context.Request.UserAgent;
            cmd.Parameters["@rawUrl"].Value = context.Request.RawUrl;
            cmd.Parameters["@userHostAddress"].Value = context.Request.UserHostAddress;
            cmd.Parameters["@userHostName"].Value = Dns.Resolve(context.Request.UserHostAddress).HostName; //this can cause a significant slowdown because of DNS reverse lookup queries!!!
            cmd.Parameters["@httpMethod"].Value = context.Request.HttpMethod;

            //
            //Open connection and execute the stored procedure
            //
            conn.Open();
            cmd.ExecuteNonQuery();
         }
      }
   }
}

As you can see, the HTTP Module is nothing more than an implementation of the System.Web.IHttpModule interface. In the Init method, we register an event handler for the BeginRequest event of the HttpApplication which is passed to use by the ASP.NET runtime through the context parameter. The rest of the code is pretty straightforward and just plain vanilla ADO.NET magic. Build the project by hitting CTRL-SHIFT-B.

Now, for the database:

  1. Open SQL Server 2000 Query Analyzer.
  2. Connect to the database where you want to put the logs; make sure you have administrative privileges over that database in order to add a table and a stored procedure.
  3. Execute the following script:

create table RequestLog
(
[ID] INT IDENTITY(1,1) PRIMARY KEY,
[agent] nvarchar(100) NOT NULL,
[rawUrl] nvarchar(1000) NOT NULL,
[userHostAddress] nvarchar(15) NOT NULL,
[userHostName] nvarchar(1000) NOT NULL,
[httpMethod] nvarchar(10) NOT NULL,
[dateTime] datetime DEFAULT GetDate()
)
go

create proc InsertLogEntry
@agent nvarchar(100),
@rawUrl nvarchar(1000),
@userHostAddress nvarchar(15),
@userHostName nvarchar(1000),
@httpMethod nvarchar(10)
as
insert into RequestLog (agent, rawUrl, userHostAddress, userHostName, httpMethod) values (@agent, @rawUrl, @userHostAddress, @userHostName, @httpMethod)
go

Very straightforward, isn't it?

 

Deployment

Time to deploy. Connect to the webserver by means of FrontPage Server Extensions or FTP or file share or ... and open up the folder that contains the web application. Do the following:

  1. Copy the WebLogger.dll file from the bin\Debug folder of your project (that's the location where the module was compiled to) to the bin folder on the server.
  2. Edit the web.config file in the root folder of the web application as follows:

<configuration>
 
<appSettings>
    <!--Web logger -->  
    <add key="dsn" value = "server=localhost;uid=Blogs_BartDeSmet;pwd=8BhWx9CB73;database=Blogs_BartDeSmet" />
  </appSettings>

  <system.web>
   
<httpModules>
      <add name="RequestLogger" type= "BdsSoft.WebLogger, WebLogger" />
    </httpModules>

  </system.web>
</configuration>

Of course, maintain all the other stuff needed in your web.config file. The code displayed above just indicates the changes needed, including the registration of the HTTP Module and the configuration of it through the dsn-setting under , which needs to be adapted to reflect your configuration (user name, password and database name). Once you have saved the web.config file, the logging should start. While writing this post (took me about 10 minutes or so), I got already 239 rows in my event log table. Analysis can start! In particular I'm interested to see which kind of user agents are visiting my blog. Currently I have:

  • Abilon
  • Bloglines/2.0 (http://www.bloglines.com; 29 subscribers)
  • BlogPulse (ISSpider-3.0)
  • FeedDemon/1.5 (http://www.bradsoft.com/; Microsoft Windows XP)
  • Feed-Directory/0.1 (+http://www.feed-directory.com/bot.html)
  • http://www.feedtagger.com/rss-fetcher.php
  • JetBrains Omea Pro 2.0 Release Candidate 2 (http://www.jetbrains.com/omea/)
  • JetBrains Omea Pro 2.0 Release Candidate 4 (http://www.jetbrains.com/omea/)
  • JetBrains Omea Reader 1.0.4 (http://www.jetbrains.com/omea_reader/)
  • Mozilla/4.0 (compatible; MSIE 5.5; Windows NT 5.0) Fetch API Request
  • Mozilla/4.0 (compatible; MSIE 5.5; Windows NT 5.0; .NET CLR 1.0.3705)
  • Mozilla/4.0 (compatible; MSIE 6.0; Windows 98)
  • Mozilla/4.0 (compatible; MSIE 6.0; Windows 98; .NET CLR 1.1.4322)
  • Mozilla/4.0 (compatible; MSIE 6.0; Windows NT 5.1; SV1)
  • Mozilla/4.0 (compatible; MSIE 6.0; Windows NT 5.1; SV1; .NET CLR 2.0.50215)
  • Mozilla/4.0 (compatible; MSIE 6.0; Windows NT 5.1; SV1; .NET CLR 2.0.50215; .NET CLR 1.1.4322)
  • Mozilla/4.0 (compatible; MSIE 6.0; Windows NT 5.2; .NET CLR 1.1.4322; .NET CLR 2.0.50215)
  • Mozilla/4.0 (compatible; MSIE 6.0; Windows NT 5.2; SV1; (R1 1.3); .NET CLR 1.1.4322)
  • Mozilla/4.0 (compatible; MSIE 6.0; Windows NT 5.2; SV1; .NET CLR 1.1.4322; .NET CLR 2.0.40607)
  • Mozilla/4.0 (compatible; MSIE 7.0b; Windows NT 5.1; Maxthon; .NET CLR 1.1.4322)
  • Mozilla/5.0 (compatible; Yahoo! Slurp; http://help.yahoo.com/help/us/ysearch/slurp)
  • Mozilla/5.0 (Windows; U; Windows NT 5.1; en-US; rv:1.7.10) Gecko/20050716 Thunderbird/1.0.6
  • Mozilla/5.0 (Windows; U; Windows NT 6.0; en-US; rv:1.7.10) Gecko/20050716 Firefox/1.0.6
  • NewsGator/2.0 (http://www.newsgator.com; Microsoft Windows NT 5.1.2600.0; .NET CLR 1.1.4322.2032)
  • NewsGatorOnline/2.0 (http://www.newsgator.com; 1 subscribers)
  • NewsGatorOnline/2.0 (http://www.newsgator.com; 24 subscribers)
  • RssBandit/1.3.0.26 (.NET CLR 1.1.4322.2032; WinNT 5.1.2600.0; http://www.rssbandit.org)
  • RssBandit/1.3.0.29 (.NET CLR 1.1.4322.2032; WinNT 5.1.2600.0; http://www.rssbandit.org)
  • RssReader/1.0.88.0 (http://www.rssreader.com) Microsoft Windows NT 5.2.3790.0
  • SharpReader/0.9.5.1 (.NET CLR 1.1.4322.2032; WinNT 5.1.2600.0)
  • SharpReader/0.9.5.1 (.NET CLR 1.1.4322.2300; WinNT 5.2.3790.0)
  • Waggr_Fetcher)
  • YahooSeeker-Testing/v3.9 (compatible; Mozilla 4.0; MSIE 5.5; http://search.yahoo.com/)

Pretty cool. Hope you enjoy it too!

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

Longhorn and Vista introduce a new kind of Start Menu which includes a search textbox to find your programs faster. However, I'm a WinKey, P, A, arrow left, arrow down, arrow down, ENTER guy to open something (in this case Active Directory Users and Computers). However, due to the introduction of the search textbox, it's impossible to do this, as the P key starts searching for apps that contain the letter P (Paint, etc). So, I switched back to the classic start menu (which I also did on Windows Server 2003 on my primary machine). The classic start menu looks like this:

Look at the left-hand side of the menu ... weird, isn't it? It's a well-known fact that every Windows build starts with the last stable build, which is in this case Windows Server 2003 + SP1, but over here it seems to be the case that the embedded resources that contain these logos are still from the pre-RTM W2K3 phase (where the Windows Server 2003 product had names such as Windows .NET Server, Windows Server .NET 2003). Or the teams just were trying to make things even more mysterious around Longhorn Server by taking some silly old image from the archives and putting it in Longhorn :-).

Wondering whether I should report this as a bug or a feature? :d

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

More Posts « Previous page - Next page »