仕様記述言語としてのCode Contractsの利用

「Code Contracts（契約）の使いどころ - Jamzzの日々」に引き続きCode Contractsについて書きたいと思います。
ここまでの内容はソフトウェア本来の目的である仕様の実現という視点で品質と生産性を向上させるためにCode Contractsを契約による設計（DbC:Design By Contract）として利用しする趣旨で書きました。
これはこれで十分な収穫があったのですが、しかし私が調べていたことは実現手段を考える以前の仕様自体の検証を行うために形式手法を具体的にどのように活用できるかということでした。
私が形式手法を知ったのは情報処理学会ソフトウェア工学研究会「ウィンターワークショップ 2010・イン・倉敷」に参加したのがきっかけでした。
まずは試しにということでVDMToolsを使ってみて、次に他にも使えそうで面白そうなものが無いかを探していたときにSpec#を見つけて、これであれば別にわざわざ専用の言語じゃなくてもC#で属性を利用すれば同じ事が出来るのではないかと思ってさらに調べたいたところCode Contractsにたどりつきました。
私の不勉強のために正直に言っていまだに何が形式手法で何がそうでないかについて理解できていないですし実践でバリバリと使ってみたわけではないので保証はないのですが、今のところの私の中ではVisual Studio環境でCode ContractsとPexを使って仕様記述言語として意図的に活用すればVDMなどのモデル規範型の記述手法を利用することと同じ効果か、場合によってはそれ以上の効果が期待できるのではないかという結論になっています。
これは以下の様な手順で仕様の機能面の検証を行うことができるということです。

1. 仕様をオブジェクト指向のクラスでモデル化する（クラス図にモデリング）
2. プログラミング言語とDbC（Design By Contract）を使って仕様記述を行う
3. 仕様記述に対してカバレッジが100%となるテスト環境を作成して検証を行う

私の今までの実務的な経験に照らし合わせて考えると、この様な手順で仕様検証を行えばVDMToolsを使って仕様検証を行うのと同等の効果は期待できるだろうと思います。
ここでDbCにCode Contractsを使えばその静的検証（これは形式的な検証と言えるのか、私には理解できていません）の機能を利用して精度を高めることができますし、Pexによりテスト精度とテスト環境構築の生産性を向上させることができると思います。
一般的な形式手法による方法に対してこの方法の利点としては以下の様なものがあると思います。

• オブジェクト指向のクラスによるモデリングの知識と経験、情報が活用できる
• プログラミング言語の知識と経験、情報が活用できる
• ソフトウェア設計の上流として利用する場合仕様記述の成果物が設計へのインプットとしてうまくつながる可能性が高い

一方で欠点としては

• 仕様の記述か実現手段の記述かの境界があいまいになりやすい

ということがあると思います。
これは普段設計者は主に仕様の実現という課題をプログラミング言語で表現するということを行っていて仕様記述を行う場合にこのスキルは非常に役に立つのですが、一方で仕様検証を行うはずが実現手段の設計を行っていたり実現手段の検証作業になってしまったりなり安いと思われます。
これは他の形式手法を用いても同様のことは課題になると思いますがプログラミング言語とは違う別の言語を使うことで設計行為との意識や発想の切り替えを行いやすいかもしれません。
これはいずれにしても運用上の注意点となると思います。
あと本質的な話からはそれますがCode ContractsやPexのすべての機能を商用で利用しようとするとVisual StudioのTeamエディションかそれ以上の構成が要求されるのですがこれは私（そして多くの人）にとって重要で悩ましい問題です。