Spec Sharp

Spec#とは、C#にEiffel風の仕様記述言語的要素を追加したプログラミング言語である。Spec#ではオブジェクト不変条件・事前条件・事後条件などの契約を記述するための構文を持つ。ESC/Javaのように、定理証明機を用いた静的検証ツールを持っており、不変条件の多くを静的に検証できる。
.NET Framework 4.0におけるコードコントラクトAPIはSpec#とともに発展してきた。
Spec#はSing#の基礎にもなっている。

 特徴 
C#と比べ、Spec#には以下の要素を持つ。

 null非許容参照型
 事前条件・事後条件を書くための構文
 Java風の検査例外
 簡易構文

 例 
事前条件・事後条件・null非許容参照型を用いた例を以下に示す。(ブラウザ上でSpec#を試す)
static int Main(string![] args)
    requires args.Length > 0;
    ensures return == 0;
{
    foreach(string arg in args)
    {
        Console.WriteLine(arg);
    }
    return 0;
}

  はnull非許容参照型である。argsはnullであってはいけない。
  は事前条件である。この例ではargsの数が0以下であることは許されない。
  事後条件である。Main関数は0を返さなければならない。

 Sing# 
Sing#はMicrosoft ResearchがSingularity(OS)を開発するためにSpec#を拡張した言語である。Sing#では低水準プログラミング言語におけるチャネルと契約を扱える。

 脚注 

 出典 

 Barnett, M., K. R. M. Leino, W. Schulte, "The Spec# Programming System: An Overview." Proceedings of Construction and Analysis of Safe, Secure and Interoperable Smart Devices (CASSIS), Marseilles. Springer-Verlag, 2004.

 関連項目 
 Eiffel
 Singularity
 C#

 外部リンク 
 Spec# from Microsoft Research
 Spec# at Codeplex
 Online Spec# at RiSE4fun

Category:C Sharp
Category:形式手法ツール
Category:.NET
Category:マイクロソフトのプログラミング言語
Category:形式仕様記述言語