[C#] Spec# が CodePlex に登場

Microsoft Research にあった Spec# が CodePlex に登場してました。
http://specsharp.codeplex.com/
と言っても、チュートリアル は 「もうすぐ」 と書いてあるだけですし、ドキュメントは Microsoft Research の方を見てくれ、とかそんな感じなんですが。

Spec# というのは C# に契約指向？ （contract oriented） な機能を追加したものです。
Eiffel に 「表明」 と呼ばれる機能がありますが、あんなやつです。
Generics みたいに Microsoft Research で生まれて、その後本家 .NET Framework に取り込まれたものもありますが、Spec# が今後どうなっていくのかはわかりません。
F# も Microsoft Research 生まれですね。

以下、Spec# のわかりやすいところを紹介してみます。

■ NonNull

public Method(object! o)
{
...
}

こんな風に引数の型名に ! を付けると 「null であってはならない」 ことを表明できます。

■ PreConditions

public void Method(int a)
requires a > 0;
{
...
}

こんな風に requires でメソッド開始前の必要条件を指定できます。
「requires ValidString(s)」 みたいにチェック用メソッドを自分で定義してチェックさせることもできるようです。
で、条件を満たさない場合は RequiresException が発生する、のかな？（PPT にそう書いてありました）

■ PostConditions

public int Method(int x, int y)
ensures result == x + y;
{
return x + y;
}

こんな風に ensures でメソッド完了後の必要条件を指定できます。
上記の例では result キーワードを使って戻り値をチェックしてますが、他にもプロパティの値をチェックしたりといったことも書けるようです。
というか、requires と ensures には boolean を返す式をなんでも書けるんじゃないかと思います。

■ その他
Program Verification Using the Spec# Programming System [PPT] なんかを見ると他にもいろんな機能があるようです。
上記の例はいずれもメソッド単位のチェックですが、もっと細かくループ単位でのチェックだとか、反対にクラスのインスタンス単位でのチェックなんかもできるみたいです。