Spec Sharp

Spec#は、マイクロソフトリサーチによって開発されたプログラミング言語で、C#に契約による設計（Design by Contract）の概念を取り入れた拡張版と言えます。この言語の大きな特徴は、プログラムの正確性や信頼性を高めるために、コード中にオブジェクトの不変条件、メソッドの事前条件、事後条件といった契約を記述できる点にあります。

Spec#の主な特徴

null非許容参照型: C#の参照型はデフォルトでnullを許容しますが、Spec#では`!`記号を使ってnullを許容しない参照型を宣言できます。これにより、NullPointerExceptionなどのエラーをコンパイル時に検出することが可能になります。
契約の記述: `requires`キーワードで事前条件を、`ensures`キーワードで事後条件を記述できます。これにより、メソッドが呼び出される前と後に満たすべき条件を明示的に示すことができます。これらの契約は、プログラムの振る舞いをより正確に定義し、バグの早期発見に役立ちます。
検査例外: Javaのように検査例外を扱うことができます。これにより、メソッドがスローする可能性のある例外を明示的に指定し、呼び出し元での適切な処理を強制することができます。
簡易構文: Spec#はC#の構文をベースにしつつも、契約記述を容易にするための簡易構文が導入されています。これにより、契約をより簡潔に記述することが可能になります。

静的検証ツール

Spec#は、ESC/Javaのような定理証明機を用いた静的検証ツールを備えています。これにより、記述された不変条件の多くを静的に検証することができます。つまり、プログラムを実行する前に、論理的な矛盾や潜在的なエラーを検出できるため、プログラムの信頼性を高めることができます。

コード例

以下はSpec#のコード例です。`args`はnullであってはいけない、また引数の数が0以下でないことを事前条件として指定しています。また、`Main`関数は0を返さなければならないという事後条件を指定しています。

specsharp
class MainClass {
public static int Main(string![]! args)
requires args.Length > 0
ensures result == 0 {
return 0;
}
}

Sing#との関係

Spec#は、マイクロソフトリサーチが開発したオペレーティングシステムSingularityを開発するためのプログラミング言語Sing#の基礎となっています。Sing#では、低水準プログラミングにおけるチャネルと契約を扱うことができます。これは、Spec#の契約記述の能力をさらに拡張し、より複雑なシステムにおける信頼性を確保するためのものです。

.NET Frameworkとの関係

.NET Framework 4.0で導入されたコードコントラクトAPIは、Spec#の発展とともに進化してきました。Spec#で培われた契約プログラミングの概念が、.NET Frameworkの標準機能として取り込まれた形と言えるでしょう。

まとめ

Spec#は、C#をベースに契約プログラミングの概念を導入した言語であり、null非許容参照型、事前条件、事後条件、検査例外などの機能を提供します。静的検証ツールにより、プログラムの信頼性を高めることができ、Sing#や.NET FrameworkのコードコントラクトAPIにも影響を与えた重要なプログラミング言語です。より堅牢なソフトウェア開発を目指す上で、Spec#の考え方は非常に有用であると言えるでしょう。

参考資料

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

もう一度検索