Spec Sharp
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2024/02/16 13:49 UTC 版)
 | この記事は検証可能な参考文献や出典が全く示されていないか、不十分です。（2024年2月） |
| パラダイム | マルチパラダイム: 構造化, 命令型, オブジェクト指向, イベント駆動, 関数型, 契約 |
|---|---|
| 登場時期 | 2004年 |
| 設計者 | Microsoft Research |
| 開発者 | Microsoft Research |
| 最新リリース | SpecSharp 2011-10-03/ 2011年10月7日 |
| 型付け | 静的型付け, 強い型付け, 安全, 公称的派生型 |
| 影響を受けた言語 | C#, Eiffel |
| 影響を与えた言語 | Sing# |
| ウェブサイト |
research |
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 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.
関連項目
外部リンク
| アーキテクチャ | |
|---|---|
| 共通言語基盤 | |
| 言語 |
|
| 関連技術 |
|
| その他のCLI実装 |
|
| 組織 | |
| 開発環境 |
|
 カテゴリ | |
- Spec Sharpのページへのリンク
