Scott Hanselman

Hanselminutes Podcast 110 - Microsoft Research: Spec#

May 8, '08 Comments [3] Posted in Podcast | Programming
Sponsored By

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.

UseMscorlibContracts - Microsoft Visual Studio

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!

Subscribe: Subscribe to Hanselminutes Subscribe to my Podcast in iTunes

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?

About Scott

Scott Hanselman is a former professor, former Chief Architect in finance, now speaker, consultant, father, diabetic, and Microsoft employee. He is a failed stand-up comic, a cornrower, and a book author.

facebook twitter subscribe
About   Newsletter
Sponsored By
Hosting By
Dedicated Windows Server Hosting by ORCS Web
Friday, 09 May 2008 08:54:18 UTC
Great podcast (my first one !) .. it got me very interested in Spec# .. definately something to be included in the next version of C#.. just one problem .. does anyone know how i set requirements for strings ie. requires name.Contains("Cat"); - Im getting errors but I cant seem to find in-date documentation on how to fix, what im sure is very trivial (and me just being a bit thick) :)
Bob Sampson
Friday, 23 May 2008 17:30:31 UTC
Thanks to everyone who wrote me about Spec#. Your comments were passed on to the team. The folks here at Microsoft are impressed with how much interest there is in Spec#, and we appreaciate your taking the time to comment on this subject.
Thursday, 19 June 2008 07:55:17 UTC
I really enjoyed this podcast and hope that these kinds of features make it into the next version of the C# language. I'm a keen user of the ReSharper plugin for Visual Studio. This plugin allows value analysis of fields, properties, method parameters and method return values via attribute annotations that indicate whether null is permissable or not. At design time, R# warns about possibly null reference exceptions.

Spec# guards against many more situations, but the R# product demonstrates today that this kind of analysis is useful in real world development using C#.

I'd particularly like to see Spec# include features that enforce immutability of types. I'm thinking that a type can only be marked as immutable (perhaps "public readonly class ...") if all of its fields are readonly, and the types of those fields are also known to be readonly. In such cases, the entire object graph can be thought of as being frozen, which allows for simpler reasoning about the usages of such objects in multithreaded applications. As parallel and functional programming ideas circulate in the C# space, immutability is being revisited as a powerful concept.
Comments are closed.

Disclaimer: The opinions expressed herein are my own personal opinions and do not represent my employer's view in any way.