本来の表記は「Spec#」です。この記事に付けられたページ名は技術的な制限または記事名の制約により不正確なものとなっています。

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

Spec#
パラダイム マルチパラダイム: 構造化, 命令型, オブジェクト指向, イベント駆動, 関数型, 契約
登場時期 2004年 (18年前) (2004)
設計者 Microsoft Research
開発者 Microsoft Research
最新リリース SpecSharp 2011-10-03/ 2011年10月7日 (10年前) (2011-10-07)
型付け 静的型付け, 強い型付け, 安全, 公称的派生型
影響を受けた言語 C#, Eiffel
影響を与えた言語 Sing#
ウェブサイト research.microsoft.com/specsharp/
テンプレートを表示

.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であってはいけない。
  • requires は事前条件である。この例ではargsの数が0以下であることは許されない。
  • ensures 事後条件である。Main関数は0を返さなければならない。

Sing#編集

Sing#はMicrosoft ResearchSingularity(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.

関連項目編集

外部リンク編集