Digging into Spec# - 1

  • [アーティクル]

A lunch conversation with Roshan lead me to download and play with Spec# from MSR. To quote the website

The Spec# programming system is a new attempt at a more cost effective way to develop and maintain high-quality software. Spec# is pronounced "Spec sharp" and can be written (and searched for) as the "specsharp" or "Spec# programming system". The Spec# system consists of:

The Spec# programming language. Spec# is an extension of the object-oriented language C#. It extends the type system to include non-null types and checked exceptions. It provides method contracts in the form of pre- and postconditions as well as object invariants.

**

The Spec# compiler. Integrated into the Microsoft Visual Studio development environment for the .NET platform, the compiler statically enforces non-null types, emits run-time checks for method contracts and invariants, and records the contracts as metadata for consumption by downstream tools.

The Spec# static program verifier. This component (codenamed Boogie) generates logical verification conditions from a Spec# program. Internally, it uses an automatic theorem prover that analyzes the verification conditions to prove the correctness of the program or find errors in it.

An interface to the Spec Explorer tool for test generation and model-based testing.

A unique feature of the Spec# programming system is its guarantee of maintaining invariants in object-oriented programs in the presence of callbacks, threads, and inter-object relationships.

 

Spec# is a superset of C# which lets you express Eiffel-like pre-conditions and post-conditions as well as specifying object invariants and a bunch of other stuff. You can pretty much ensure the state of your objects throughout the lifetime of your program. All this is very much possible with normal C# code but would probably require reams and reams of code. For example, the video on the Spec# site talks of how the BCL team perform lots of checks over and over again while calling other BCL code - and using Spec# to do these checks would give them a big perf boost as well as ensuring they don't miss anything.

And if you're not convinced of Spec#'s usefulness,maybe the fact that they wrote an operating system using it might change your mind.

There's not too much documentation for Spec# but there's a free online video linked to from the Spec# page. Unfortunately, support for VS 2005 isn't available yet so I couldn't get to see red squizzlies in my code when I made a mistake. However, the Spec# compiler works very well with the .NET 2.0 Beta2 build on my system - so all is not lost.

Let's start off with a very simple example - a function that takes a string and an integer N and returns the Nth char of the string (pretty much what the String class's default indexer does).

using System;

public class Program
{
  public static void Main(string[] args)
{

   char c=GetNthChar("Hello",4);
Console.WriteLine(c);

}

  static char GetNthChar(string s,int n)
{
 return s[n];
}

}

There are a bunch of things that GetNthChar assumes. For example, the string variable s should not be null otherwise s[n] will throw a NullReferenceException. Similarly, exceptions will be thrown if n is not in a valid range.

Now, we could write a lot of code and wrap everything in try-catch blocks but such an approach is not going to scale very well. Also, it screws up the intent of our code - instead of worrying about what the code is supposed to do, we'll be spending more time writing error handling code.  All this is a lot easier in Spec#. So, rewriting this in Spec# [1]

  static char GetNthChar(string s,int n)
requires s!= null ;
requires n>=0 && n <s.Length;
{
 return s[n];
}

  
  What we've done here is to add 2 pre-conditions - one saying that the parameter 's' shouldn't be null and the other ensuring that 'n' falls in the right range. Let's compile this guy using the Spec# compiler. 
  
  C:\>ssc test.ssc

  
  All's well with the world and everything compiles cleanly. Since I'm in an evil mood, I'm going to induce errors in this small program.[2]

  Let's change Main to the following
  
  
   public static void Main(string[] args)
{

   char c = GetNthChar(null,4);
Console.WriteLine(c);

}

  When I compile this code, I get a pretty interesting error (if you're using VS 2003, just typing this code will throw up a squiggly).
  
 
C:\>ssc test.ssc
test.ssc(8,23): warning CS2612: Null cannot be used where a non-null value is expected

What's happening here is that the Spec# compiler is ensuring that a null reference isn't passed in as 's', thereby ensuring our first pre-condition. A lot of code analysis like this can happen at compile time itself.

Let's see what happens when the code can't be checked at compile-time.
 
public static void Main(string[] args)
{

      string input = Console.ReadLine();
      if(input!= null)
{
            char c = GetNthChar(input,4);
Console.WriteLine(c);
}
}

Here, we're making sure that the string variable 'input' can't be null. However, the string read in from the console could easily be shorter than 4 characters long - and this is something the Spec# compiler has no way of predicting. The code compiles cleanly (the static analyzer notices the null check). Let's run test.exe and type in a single character. You get an IndexOutOfRangeException as expected.

However, compile the code now with debug information (using ssc /debug) and run it.Type in a single character as before.

C:\>test
a

Unhandled Exception: System.Compiler.Contracts.RequiresException: Precondition
violated from method 'Program.GetNthChar(optional(System.Compiler.Contracts.NonNullType) System.String,System.Int32)'
   at Program.GetNthChar(String s, Int32 n) in C:\test.ssc:line 20
at Program.Main(String[] args) in C:\test.ssc:line 11

What's happening here is that Spec# is enforcing contracts at runtime too - and the contract of 'n' being lesser than the string's length has been
violated.

It's quite interesting to see how all this works underneath the covers. Spec# injects a bunch of code at the start of your function (for pre-conditions) and at the end (for post-conditions). When I disassemble this code using Lutz Roeder's .NET Reflector, here's what I get.

[Requires("::!=(optional([System.Compiler.Runtime]System.Compiler.Contracts.NonNullType,string),object){$0,null}", Filename=@"C:\test.ssc", StartLine=0x12, StartColumn=12, EndLine=0x12, EndColumn=20, SourceText="requires s!= null;"), Requires("::>=(i32,i32){$1,0}", Filename=@"C:\test.ssc", StartLine=0x13, StartColumn=12, EndLine=0x13, EndColumn=0x10, SourceText="requires n>=0 ;"), Requires("::<(i32,i32){$1,$0@string::get_Length(){}}", Filename=@"C:\test.ssc", StartLine=20, StartColumn=13, EndLine=20, EndColumn=0x19, SourceText="requires n < s.Length ;")]
private static char GetNthChar(string modopt(NonNullType) s, int n)
{
      char ch1;
      try
      {
<Lots of code omitted>
      Label_007F:;
            try
            {
                  if (n < s.Length)
{
                        goto Label_00D1;
}
}
            catch (Exception exception3)
{
                  throw new RequiresException("Exception occurred during evaluation of precondition in method 'Program.GetNthChar(optional(System.Compiler.Contracts.NonNullType) System.String,System.Int32)'", exception3);
}
            catch
            {
                  throw new RequiresException("Exception occurred during evaluation of precondition in method 'Program.GetNthChar(optional(System.Compiler.Contracts.NonNullType) System.String,System.Int32)'");
}
            throw new RequiresException("Precondition violated from method 'Program.GetNthChar(optional(System.Compiler.Contracts.NonNullType) System.String,System.Int32)'");
}
      catch (ContractMarkerException)
{
            throw;
}
Label_00D1:
ch1 = s[n];
      char ch2 = ch1;
      return ch1;
}
Spec# injects all the checks into your function's body and wraps them nicely in exception handlers for you as well. The actual conditions are expressed in metadata in the form of attributes for the function.

We've barely scratched the surface in terms of what Spec# can do. Next time - post-conditions, invariants,ownership and more!

Same Bat-time , same Bat-channel!

 

 

Notes

1. I could also write it as

  static char GetNthChar(string! s, int n)
requires n>=0 && n<s.Length;

  
  The bang (!) character after the type of a parameter is a short-hand form of specifying that the parameter shouldn't be null.
 
 
2.Of course, in the real world, my code never has any errors in it ; -)

Comments

  • Anonymous
    June 20, 2005
    The comment has been removed
  • Anonymous
    June 20, 2005
    Interesting... but somehow I feel this would've been more interesting if it was done on top of a dynamic language, that would be really something.
  • Anonymous
    June 24, 2005
    "Spec# injects all the checks into your function's body and wraps them nicely in exception handlers for you as well."

    What if I do not want a particular check to be automatically put into the compiled code? Would the programmer have any control on what checks get automatically injected in to the compiled code?
  • Anonymous
    June 24, 2005
    I was also wondering why is it called
    >> Spec << Sharp.
  • Anonymous
    June 29, 2005
    Swaroop - I'm not sure why you feel this would be more useful with dynamic languages - but anyway, I've seen stuff like this done with Python.
  • Anonymous
    June 29, 2005
    Sunil- if you don't want a check to be injected, don't write it in the first place :-)
  • Anonymous
    August 03, 2005
    Thanks for the link, Sriram. The Requires Keyword just belew my mind off:) And, hope it's extended to VB.NET and hope to get my hands on it as soon as i get Whidbey:)
  • Anonymous
    August 04, 2005
    Thanks Sriram for introducing me to Spec#. Would get it as soon as I get my hands on VS.NET:)