WindowsFormとCodeContractsについて

Question

Visual Studio 2010 Pro、C＃に関連する質問です。

Code Contractsを使用して、以下のようなコードを作成しました。

フォーム上にチェックボックスとボタンを配置し、チェックボックスがONの場合に限りボタンがクリック可能であるというアプリケーションです。

 

---- コードここから----

    public partial class Form1 : Form
    {
        public Form1()
        {
            InitializeComponent();
            ToggleButton();
        }

        private void button1_Click(object sender, EventArgs e)
        {
            System.Diagnostics.Contracts.Contract.Requires(checkBox1.Checked);
            System.Windows.Forms.MessageBox.Show("test");
        }

        private void checkBox1_CheckedChanged(object sender, EventArgs e)
        {
            ToggleButton();
        }

        private void ToggleButton()
        {
            button1.Enabled = checkBox1.Checked;
        }
    }

---- コードここまで----

 

Code Contractsにて、上記の

System.Diagnostics.Contracts.Contract.Requires(checkBox1.Checked);

を記述し、自動的にチェックが働くことを期待しているのですが、期待通りに動きません。

WindowsフォームでCode Contractsを使用したい場合、どのようにすればよいのでしょうか？

 

宜しくお願いします。

 

【環境】

Visual Studio 2010 Professional

.NET Framework 4.0

Answer 1

Code Contractsについて誤解されています。Debug.Assert() はご存知でしょうか？ Code Contractsはその延長の概念で、ソースコードが意図通り正しく書かれているかどうかをチェックするための機構です。画面動作を制御する用途には使えません。

Answer 2

つまり、以下のような書き間違いをしている場合は、検出してもらえないということでしょうか。

逆に言うと、このような書き間違いを自動的に検出する目的で使えるツールなどはあるのでしょうか？

 

---- コードここから----

    public partial class Form1 : Form
    {
        public Form1()
        {
            InitializeComponent();
            //ToggleButton();を書き忘れた場合。
        }

        private void button1_Click(object sender, EventArgs e)
        {
            System.Diagnostics.Contracts.Contract.Requires(checkBox1.Checked);
            System.Windows.Forms.MessageBox.Show("test");
        }

        private void checkBox1_CheckedChanged(object sender, EventArgs e)
        {
            ToggleButton();
        }

        private void ToggleButton()
        {
            button1.Enabled = checkBox1.Checked;
        }
    }

---- コードここまで----

Answer 3

画面動作の制御ではなく、ボタン押下時の契約の前提条件の話と解釈しました。

上記の場合、画面実行後すぐに（チェックボックスの状態を変更せずに）ボタンを押せば、

Contractの例外が発生しませんか？

なお、プロジェクトのプロパティの「Code Constracts」の「Perform Runtime Constract Checking」に

チェックは入ってますか？

Answer 4

> 画面動作を制御する用途ではなく、ボタン押下時の契約の前提条件チェックの話ですよね？

はい。

そして、コンパイル時にチェックしてくれることを望んでおります。

CodeContractsを使用した場合、コンパイラが警告を出してくれるようですが、

今回はその警告が望んだとおりに出てくれなくて困っているという状態です。

 

> 上記の場合、画面実行後すぐに（チェックボックスの状態を変更せずに）ボタンを押せば、Contractの例外が発生しませんか？

はい。

コンパイルして実行すれば、例外が出力されます。

 

> なお、プロジェクトのプロパティの「Code Constracts」の「Perform Runtime Constract Checking」にチェックは入ってますか？

もちろん入れています。

しかし、今回の目的はランタイムチェックではなく、コンパイル時のチェックです。

Answer 5

補足すると、SPINのモデル検査のような動作を期待しています。

コンパイルやビルド、もしくはそれ以外の静的検査によってCode Contractsにて指示した内容に違反があるならば、その反例を検出してくれるような動作を期待しておりました。

Answer 6

＞今回の目的はランタイムチェックではなく、コンパイル時のチェックです。

＞補足すると、SPINのモデル検査のような動作を期待しています。

 

たしかテストパターンチェックは、Pexを使えば出来たと思います。

http://research.microsoft.com/en-us/projects/pex/default.aspx

Answer 7

イベントハンドラがどんな時に呼び出されるか、それに応じてチェックをしてくれるツールなのでしょうか？ あったら怖いなぁ…。

Answer 8

Code Contractsは静的チェックを行うツールなので、このような期待をすることはある意味正しいですが、元の質問文からは質問内容が読み取れませんでした。特に「期待通りに動きません」の辺りなど。

以下、回答ではありませんが、WPFを使うとbindingで簡単に記述できます。

<CheckBox Name="checkBox1" Content="CheckBox" IsChecked="True" />
<Button Name="button1" Content="Button" IsEnabled="{Binding  ElementName=checkBox1, Path=IsChecked}" />

こう書くとbutton1.IsEnabledプロパティはcheckBox1.IsCheckedプロパティに連動します。ToggleButton()のようなメソッドを書く必要はありません。

ま、参考までにと。

Answer 9

なるほどPEXでテストケースを自動生成してしまおうと……

近いと言えば近いですが、モデル検査のような動作ではないですよね……

 

しかし、よくよく調べるとCodeContractsはモデルチェック機能を持ってないらしく

さらに、そもそもオブジェクト指向でのモデルチェッカはあまりないみたいですね……

技術的に不可能なのかな？

 

しかし、PEXは近いと思いますので、実際に使ってみようと思います。

Answer 10

ありがとうございます。

確かに、このような手段もありますね。

 

とりあえず、C#での開発時にはモデル検査ツールとPEXなどを併用して行っていきたいと思います。

皆さん回答ありがとうございました。