Spec# and Boogie Released on CodePlex

You may have noticed that in the past that I’ve talked extensively about Spec#, an object-oriented .NET language based upon C# with contract-first features as well as a non-null type system.  This project has not only been covered by myself, but also my CodeBetter compatriot, Greg Young, and by the illustrious Tony Hoare at QCon London during his “Null References: The Billion Dollar Mistake” presentation.  This project, after gaining momentum in the .NET world, has now been made part of .NET 4.0 as Code Contracts for .NET.

Today, the big news is that both Spec# and the program verification system, Boogie have been released on CodePlex.  The Boogie project is released under the Microsoft Public License (Ms-PL) and Spec# has been released under the Microsoft Research Shared Source License Agreement (MSR-SSLA), which restricts Spec# usage to non-commercial uses only.

What is Spec#?

As I mentioned above, Spec# is a language approach to implementing contract-first development principles as well as a non-null type system on top of the C# language with additional constructs.  Mike Barnett and Rustan Leino of Microsoft Research worked on this project along with many others and finally released on CodePlex.  What does that buy for us exactly? 

It allows us to specify three main areas of concern:

  • What do we expect? (preconditions)
  • What do we guarantee? (postconditions)
  • What do we maintain? (invariants)

Through the language support, we can model:

  • Acceptable and unacceptable input values
  • Return values
  • Error conditions
  • Preconditions which subclasses may weaken (not strengthen)
  • Postconditions which subclasses may strengthen (not weaken)
  • Invariants which subclasses may strengthen (not weaken)

As it is a dialect of C#, we can model our preconditions such as requiring a dividend not being equal to zero:

public double Divide(int divisor, int dividend)
    requires dividend != 0;
{
    return divisor / dividend;
}

By using the requires keyword, we can easily specify inline with the method signature what our preconditions are.  Just as well, we can also model our postconditions, also known as what we guarantee, such as when we add an integer to our list, we increment the count by 1:

public int Count { ... }

public void Add(int number)
    ensures Count == old(Count) + 1;
{ ... }

By using the ensures keyword, we can create postconditions.  In this case, I also used the old(…) function to denote that we will compare the old value of Count before this method was called.  We can also model our invariants, what must hold true for our members such as an age of a person must be greater than zero:

class Person {
    private int age;
    invariant age >= 0;
    
    ...
}

During any operation, this invariant must hold or an exception will be thrown.  We have the ability to expose these sections where our state changes to the prover which then asserts that our invariants hold.

One more interesting facet of Spec# is the introduction of the non-null type system.  This allows us to specify either by default through a property window that all reference types must be non-null, or we can explicitly mark them as such using the ! or bang notation:

public int Count { ... }

public void Add(object! item)
    ensures Count == old(Count) + 1;
{ ... }

This non-null reference then becomes statically checked to ensure that we are not handing this Add method a null reference.  There are many other advanced topics that are covered in the Spec# documentation.

You can hear Mike and Rustan talk about Spec# and their experiences on some podcasts:

The Code Contracts being released as part of .NET 4.0 is based upon this approach, but instead of being a language approach, the idea is to allow all languages to use them as a library feature.  This allows me to use this in my F# code as well as any C#, VB.NET and so on

What Kind of a Name is Boogie Anyways?

So, we’ve talked about Spec#, but what about the other release, Boogie?  Well, Boogie, the name is applied actually to two different pieces.  First, Boogie is an immediate verification language which is intended to build program verifiers for other languages.  This allowed for targeting not only Spec#, but also C, Chalice among others.  Boogie, however, is also a tool that accepts the Boogie language as input and generates verification conditions that are passed to an SMT solver.  In the case of Spec#, that has been the Z3 theorem prover.  You can read more about Boogie, the language here as well as the architecture here.

Conclusion

These have been interesting times with the release of Trident and Dryad/DryadLINQ last month to the release of Boogie and Spec#.  It is quite encouraging to see these tools come into the public domain where not only other researchers can learn, but the average developer as well.  Although Code Contracts for .NET is the way to go going forward with .NET, it’s still encouraging to see Spec# being put out there for public consumption.

This entry was posted in Spec#. Bookmark the permalink. Follow any comments here with the RSS feed for this post.
  • http://codebetter.com/blogs/matthew.podwysocki/ Matthew Podwysocki

    @jdn,

    Agreed that it is less than optimal as it would have been great to expose it as you would Boogie. Although, I must admit that it is better than not having it at all, especially as a good learning experience.

    Matt

  • http://www.blogcoward.com jdn

    “which restricts Spec# usage to non-commercial uses only.”

    That’s disappointing.

  • http://codebetter.com/members/rob.reynolds/default.aspx Rob

    Awesome!