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