Design by Contract in C#といったもののようだ。
「達人プログラマー」を読んだ人やJavaでiContractのようなツールを使って契約ベースのプログラミングをしたことある人ならば、コードに対する事前条件・事後条件の価値がすぐわかるでしょうというようなことが参照元に記述されている。達人プログラマーの「第4章 契約による設計」(p.110-)に概要が載っているので興味ある人は読んでみては。
VC++とかにも欲しいところなんだけど、似たようなものは既にあるのかな？
The Spec# programming system is a new attempt at a more cost effective way to develop and maintain high-quality software. The system consists of:
* A programming methodology, which includes a sound treatment of object invariants in object-oriented programs.
* The Spec# programming language, which is a superset of C# and adds things like non-null types, checked exceptions, method contracts (like pre- and postconditions), and object invariants.
* The Spec# compiler, which is integrated into the Microsoft Visual Studio development environment, statically enforces non-null types, emits run-time checks for method contracts and invariants, and records the specifications in metadata for consumption by the program verifier.
* The Spec# static program verifier, which translates programs into logical verification conditions, which are passed to an automatic theorem prover.
* An interface to the SpecExplorer tool for test generation and model-based testing.
[Spec# Overviewより引用]