Spec_Sharpとは? わかりやすく解説

Weblio 辞書 > 辞書・百科事典 > 百科事典 > Spec_Sharpの意味・解説 

Spec Sharp

出典: フリー百科事典『ウィキペディア(Wikipedia)』 (2024/02/16 13:49 UTC 版)

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

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であってはいけない。
  • 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.

関連項目

外部リンク




英和和英テキスト翻訳>> Weblio翻訳
英語⇒日本語日本語⇒英語
  

辞書ショートカット

すべての辞書の索引

「Spec_Sharp」の関連用語

Spec_Sharpのお隣キーワード
検索ランキング

   

英語⇒日本語
日本語⇒英語
   



Spec_Sharpのページの著作権
Weblio 辞書 情報提供元は 参加元一覧 にて確認できます。

   
ウィキペディアウィキペディア
All text is available under the terms of the GNU Free Documentation License.
この記事は、ウィキペディアのSpec Sharp (改訂履歴)の記事を複製、再配布したものにあたり、GNU Free Documentation Licenseというライセンスの下で提供されています。 Weblio辞書に掲載されているウィキペディアの記事も、全てGNU Free Documentation Licenseの元に提供されております。

©2025 GRAS Group, Inc.RSS