Geeks With Blogs
Chris Breisch   .NET Data Practices
Search this Blog!

There’s a new version of Spec# available on the Microsoft Research Downloads page.  I know there’s been a lot of discussion of LINQ, but I’m not entirely sold on it.  However, Spec# is also a direction for features that may appear in an official C#-like language some day and is worth checking out.

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.

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.

The Spec# programming system is being developed as a research project at Microsoft Research in Redmond, primarily by the Programming Languages and Methods group.

There are downloads available for VS .NET 2003 and for VS .NET 2005.

Posted on Friday, May 19, 2006 5:30 AM .NET Development | Back to top

Comments on this post: Spec#

No comments posted yet.
Your comment:
 (will show your gravatar)

Copyright © Chris J. Breisch | Powered by: