Code Contracts（契約）の使いどころ

「Code ContractsとPex - Jamzzの日々」に引き続いてCode Contracts（契約）の使いどころについて書きたいと思います。
Code Contractsで興味深いと思う点は契約の継承、特にインターフェイスやabstractのクラス（abstractのメソッド）に対する契約を記述できる点です。
契約による設計（契約プログラミング）における議論として、どの範囲にどれぐらいの厳密さで契約を記述するべきかということがあると思います。
この議論に対してはっきりと言えることはライブラリ、モジュール、コンポーネントのインターフェイス、特にフレームワークにおける拡張点にあたる部分については相当な厳密さで契約を記述することは確実に効果が期待できるということです。
フレームワークの拡張点に契約を記述しようとした場合にインターフェイスやabstractのクラス（abstractのメソッド）に対する契約を記述できることは非常に重要だと思います。
このようなことが一般に商用で使われる開発、実行環境でサポートされるという点がとても魅力的です。（Java等の他の一般に商用で使われる言語で同様のことができるものがあれば興味がありますので情報を求めたいと思います）
あとCode Contracts（契約）の使いどころと言えばユニットテストの対象となるメソッドだと思います。
これはどの範囲にどれぐらいの厳密さでユニットテストを記述するべきかという議論に転嫁していてこの悩みの解消にならないのですが、どうせユニットテストで表明（Assertion）を書くつもりであればその分を契約として記述した方が結合デバッグの際に活用することができますし、ユニットテストコードをメンテするよりも対象のコードに契約として記述する方が情報が対象のメソッドの記述に集まるのでメンテしやすいと思います。
それからCode Contractsで記述した契約はSandcastleで自動生成するリファレンスに事前条件、事後条件を表示するように出来るようです。（参考：「Daryl Zuniga and Mike Barnett - Xml Documentation from Code Contracts for .Net」）
従来メソッドのコメントに記述していたような引数や戻り値の範囲の記述を契約として記述すれば自動的にリファレンスにも反映されるということです。
この様な事がより積極的に契約を書こうとする動機になると思います。

あと、興味がある方に参考までにCode Contractsが継承にどのように働くかを紹介しておきます。
例えば、

    class TestSuperClass
    {
        public virtual int TestMethod(int p)
        {
            Contract.Requires(p > 0); // 事前条件
            return 1;
        }
    }
    class TestClass : TestSuperClass
    {
        public override int TestMethod(int p)
        {
            Contract.Ensures(Contract.Result<int>() > 0); // 事後条件
            return p;
        }
    }
    class TestSubClass : TestClass
    {
        public override int TestMethod(int p)
        {
            return 0;
        }
    }

    class Program
    {
        static void Main(string[] args)
        {
            int ret = new TestSuperClass().TestMethod(1);
            ret = new TestClass().TestMethod(ret);
            ret = new TestSubClass().TestMethod(ret);
            Console.WriteLine(ret.ToString());
        }
    }

このようなソースでCode Contractsの静的検証を行うと以下の様な結果が出ます。

警告1 CodeContracts: ensures is false: Contract.Result() > 0
警告2 + location related to previous warning
警告3 CodeContracts: requires unproven: p > 0
警告4 + location related to previous warning
警告5 CodeContracts: requires unproven: p > 0
警告6 + location related to previous warning
メッセージ7 CodeContracts: Checked 5 assertions: 2 correct 2 unknown 1 false

これらの警告は以下の場所に出ます。

    class TestSuperClass
    {
        public virtual int TestMethod(int p)
        {
            Contract.Requires(p > 0); // 事前条件 <= 警告4 警告6
            return 1;
        }
    }
    class TestClass : TestSuperClass
    {
        public override int TestMethod(int p)
        {
            Contract.Ensures(Contract.Result<int>() > 0); // 事後条件 <= 警告2
            return p;
        }
    }
    class TestSubClass : TestClass
    {
        public override int TestMethod(int p)
        {
            return 0; // <= 警告1
        }
    }

    class Program
    {
        static void Main(string[] args)
        {
            int ret = new TestSuperClass().TestMethod(1);
            ret = new TestClass().TestMethod(ret); // <= 警告3
            ret = new TestSubClass().TestMethod(ret); // <= 警告5
            Console.WriteLine(ret.ToString());
        }
    }

この状態からTestClassクラスのTestMethodメソッドにある事後条件をTestSuperClassクラスのTestMethodメソッドに移動するとTestSuperClassクラスのTestMethodメソッドの戻りが0より大きいことが保証されるのでCode Contractsの静的検証の結果が以下のように変わります。

警告1 CodeContracts: ensures is false: Contract.Result() > 0
警告2 + location related to previous warning
メッセージ3 CodeContracts: Checked 6 assertions: 5 correct 1 false

    class TestSuperClass
    {
        public virtual int TestMethod(int p)
        {
            Contract.Requires(p > 0); // 事前条件
            Contract.Ensures(Contract.Result<int>() > 0); // 事後条件 <= 警告2
            return 1;
        }
    }
    class TestClass : TestSuperClass
    {
        public override int TestMethod(int p)
        {
            return p;
        }
    }
    class TestSubClass : TestClass
    {
        public override int TestMethod(int p)
        {
            return 0; // <= 警告1
        }
    }

    class Program
    {
        static void Main(string[] args)
        {
            int ret = new TestSuperClass().TestMethod(1);
            ret = new TestClass().TestMethod(ret);
            ret = new TestSubClass().TestMethod(ret);
            Console.WriteLine(ret.ToString());
        }
    }

これらは静的検証なので実行しなくてコンパイルだけでチェックできます。
上記の例ではオブジェクトの不変条件 (invariant)の記述がありませんが、オブジェクトの不変条件 (invariant)も継承されます。
継承したクラスでも不変条件 (invariant)を記述できて親をさかのぼったすべての条件が組み合わされることになりますが、子供の不変条件 (invariant)は親の条件より限定することは許されますが条件を緩和することはできません。
ただリスコフの置換原則にあるように継承関係の階層によって契約条件が異なることは注意が必要だと思います。

インターフェイスやabstractのクラス（abstractのメソッド）に対する契約の記述方法については「とある契約の備忘目録。契約による設計(Design by Contract)で信頼性の高いソフトウェアを構築しよう。 - Bug Catharsis」やCode ContractsのUser Manualを参照してみてください。