Scott Hanselman's ComputerZen.com

My one-hundred-and-tenth podcast is up. This episode was recorded at the ALT.NET Open Spaces Conference in Seattle a few weeks back. I got to sit down with two gentlemen from Microsoft Research, Mike and Rustan, and talk about Spec# after their presentation at the conference.

What's Spec#? Currently it's a new language that is essentially extensions to C# 2.0. For example:

class ArrayList { public virtual void Insert(int index , object value)
requires 0 <= index && index <= Count;
requires !IsReadOnly && !IsFixedSize;
{ . . . }

See all that new stuff BEFORE the first curly brace? That's where you specify preconditions that you want enforced. You can also specify postconditions:

ensures Count == old(Count) + 1;
ensures value == this[index ];
ensures Forall{int i in 0 : index ; old(this[i]) == this[i]};
ensures Forall{int i in index : old(Count); old(this[i]) == this[i + 1]};

There's LOTS more, including a pretty extraordinary static analysis that runs in the background, kind of like the grammar checker in Word. Word has the spelling checker that turns errors red with squiggly underlines, and the grammar checker that turns grammatical errors green with squiggly underlines. Spec# will turn static errors into squiggles while you type.

They've even added specifications for the Base Class Library (BCL) that have previously only existed in documentation.

BTW, if you want to see horribly shaky cellphone video of their presentation, you can see it at Greg Young's blog. He's posted recently about Spec# as well. If you don't like videos or podcasts, you can also read the Spec# Research Paper (PDF).

How can you get involved? We need to convince that folks on the C# team that Spec# is a valuable thing and that we'd like it sooner than later. Go over to Charlie Calvert's blog and email him that you want Spec# and why!

• Spec# from Microsoft Research
• Mike Barnett
• Rustan M. Leino
• Install Spec# for VS 2005
• Install Spec# for VS 2008

Subscribe:

• Download: MP3 Full Show
• Torrent: Download via µtorrent
• ACTION: Please vote for us on Podcast Alley! Digg us at Digg Podcasts!

If you have trouble downloading, or your download is slow, do try the torrent with µtorrent or another BitTorrent Downloader.

Do also remember the complete archives are always up and they have PDF Transcripts, a little known feature that show up a few weeks after each show.

Telerik is our sponsor for this show.

Check out their UI Suite of controls for ASP.NET. It's very hardcore stuff. One of the things I appreciate about Telerik is their commitment to completeness. For example, they have a page about their Right-to-Left support while some vendors have zero support, or don't bother testing. They also are committed to XHTML compliance and publish their roadmap. It's nice when your controls vendor is very transparent.

As I've said before this show comes to you with the audio expertise and stewardship of Carl Franklin. The name comes from Travis Illig, but the goal of the show is simple. Avoid wasting the listener's time. (and make the commute less boring)

Enjoy. Who knows what'll happen in the next show?