Code Contractsを使用した仕様記述の例（鶴亀算）

引き続きCode Contractsを使用した仕様記述と検証についてです。
試しに鶴亀算について仕様記述と検証を行ってみました。
はじめは簡単に考えていたのですが実際にやってみるとなかなか奥が深く思っていたほど簡単ではないことが分かりました。
そしてこの難しさが実行時にエラーが起こらないように仕様を記述することの難しさであることを実感しました。
それと同時に、仕様記述にCode Contractsを使いPexも合わせて検証を行う手法の効果について理解することができました。
実際に私が行った手順を紹介してみます。

まずはじめに直感的に鶴亀算の仕様記述を行って以下の様なものを書きました。

    public class TsuruKameCalculator
    {
        public int NumberOfTsuru { get; private set; }
        public int NumberOfKame { get; private set; }
        public void Calculate(int heads, int legs)
        {
            // 事前条件
            Contract.Requires(heads > 0);
            Contract.Requires(legs > 0);

            // 事後条件
            Contract.Ensures((this.NumberOfTsuru + this.NumberOfKame) == Contract.OldValue<int>(heads));
            Contract.Ensures((2 * this.NumberOfTsuru + 4 * this.NumberOfKame) == Contract.OldValue<int>(legs));

            // 実装
            this.NumberOfTsuru = (4 * heads - legs) / 2;
            this.NumberOfKame = (legs - 2 * heads) / 2;
        }
    }

これでCode Contractsの静的チェックでの警告はありません。
直感的にはこんな感じになったのですが、Calculate()メソッドでPexを使ってコードカバレッジが100%となるユニットテストを自動実行すると、この記述では鶴亀算への入力チェックが不十分であるというだけでなく、不適切な入力に対して鶴や亀の数が負の数になるという不適切な結果になるというバグがあることがわかりました。
そこでまずは不適切な結果になることが無いように以下の様な事後条件を追加しました。

            Contract.Ensures(this.NumberOfTsuru >= 0);
            Contract.Ensures(this.NumberOfKame >= 0);

この状態でコンパイルするとCode Contractsの静的チェックにより、現在の事前条件ではこの追加した事後条件が保障されないという警告が出ました。（賢い！）
このままでは入力によって実行エラーが発生する可能性があるということです。
それで仕様の定義を追加しなければならないのですが、この様な鶴亀算に対する不正な入力に対して呼び出し元にエラー（Exceptionなど）を通知するという仕様か、呼び出し側がこのような不正な入力を行わない様にする責任を負うという仕様が考えられます。
ここでは呼び出し側がこのような不正な入力を行わない様にするという責任を負うという仕様として、その仕様を事前条件としてCalculate()メソッドに以下のように追加しました。

            Contract.Requires(((4 * heads - legs) / 2) >= 0);
            Contract.Requires(((legs - 2 * heads) / 2) >= 0);

これでCode Contractsの静的チェックの警告が無くなりました。
これで完了かと思ったのですが改めてCalculate()メソッドでPexを実行するとまだ実行時エラーが発生するケースが見つかりました。
どうやらパラメータlegsに奇数が指定された場合に実行時エラーになる可能性がある様です。
よく考えればlegsは偶数でなければならないことに気がつきました。
それで事前条件にlegsが偶数であることを条件として追加しました。

            Contract.Requires((legs % 2) == 0);

これでCode Contractsの静的チェックもPexによるユニットテストの結果も問題ありません。
ここまでの内容を反映したものは以下の様になります。

    public class TsuruKameCalculator
    {
        public int NumberOfTsuru { get; private set; }
        public int NumberOfKame { get; private set; }
        public void Calculate(int heads, int legs)
        {
            // 事前条件
            Contract.Requires(heads > 0);
            Contract.Requires(legs > 0);
            Contract.Requires((legs % 2) == 0);
            Contract.Requires(((4 * heads - legs) / 2) >= 0);
            Contract.Requires(((legs - 2 * heads) / 2) >= 0);

            // 事後条件
            Contract.Ensures(this.NumberOfTsuru >= 0);
            Contract.Ensures(this.NumberOfKame >= 0);
            Contract.Ensures((this.NumberOfTsuru + this.NumberOfKame) == Contract.OldValue<int>(heads));
            Contract.Ensures((2 * this.NumberOfTsuru + 4 * this.NumberOfKame) == Contract.OldValue<int>(legs));

            // 実装
            this.NumberOfTsuru = (4 * heads - legs) / 2;
            this.NumberOfKame = (legs - 2 * heads) / 2;
        }
    }

この鶴亀算の仕様に対して呼び出し側を記述してみました。

    class Program
    {
        static void Main(string[] args)
        {
            TsuruKameCalculator calculator = new TsuruKameCalculator();
            //calculator.Calculate(1, 1); <= 警告
            calculator.Calculate(1, 2);
            calculator.Calculate(1, 4);
            //calculator.Calculate(2, 2); <= 警告
            calculator.Calculate(2, 6);
            //calculator.Calculate(2, 10); <= 警告
            calculator.Calculate(306783378, 613566760);
        }
    }

ここでコメントアウトしている様に呼び出し側で不正な入力を与えるような記述を行うとコンパイルの際にCode Contractsの静的チェックにより警告してくれます。
このように呼び出し側でCode Contractsの静的チェックによる警告とPexを利用するなどしてカバレッジ100%のテストを実行すれば実行時エラー発生の可能性を排除することができると思います。
具体的には実際にCode ContractsとPexを使って上記のソースなどを修正して動作を実感してもらえればよいと思います。

ここで紹介したのはちょっとした例でしかありません。
実際のシステム開発で活用しようとするとかなりのボリュームになることが予想されますのでやはり負担と効果の経済合理性が課題になると思われます。
ここまで調査した印象としては仕様の機能的な検証を目的とする場合にはCode ContractsとPexを組み合わせることで他の手法に比べて非常に高い生産性を期待できると思っています。
そして実現手段としてソフトウェアの設計に利用する場合ももちろんです。
今後も調査を継続し、動向にも注意したいと思っています。