06

15

有界モデル検査技術 CBMC その2

2010.06.15(20:55)

CBMCを使って、まほうじんを解いてみましょう。

#define NUM 3

int solve(void) {
// マス目の数
int masu[NUM*NUM];
// マス目の数の合計 縦 NUM個、横 NUM個、斜め 2個
int sum[NUM*2+2];
int ans[NUM*NUM];
int check;
int i, j;
int sum_index;

// すべてのマスの値は、0より大きく、マス目の数より小さい
for(i = 0; i < NUM*NUM; i++){
__CPROVER_assume(masu[i] > 0 && masu[i] < NUM*NUM+1);
}

// すべてのマスの値は異なる
for(i = 0; i < NUM*NUM; i++){
for(j = i+1; j < NUM*NUM; j++){
__CPROVER_assume(masu[i] != masu[j]);
}
}

// 縦横の合計
for(i = 0; i < NUM; i++){
sum[i] = 0;
sum[NUM + i] = 0;
for(j = 0; j < NUM; j++){
sum[i] += masu[i*NUM+j];
sum[NUM + i] += masu[i+NUM*j];
}
}

// 斜めの合計
sum[NUM*2 + 0] = 0:
sum[NUM*2 + 1] = 0;
for(j = 0; j < NUM; j++){
sum[NUM*2 + 0] += masu[0 +(NUM+1)*j];
sum[NUM*2 + 1] += masu[(NUM-1)+(NUM-1)*j];
}

// 合計がすべて一致すると assertで落とす
check = 1;
for(i = 0; i < NUM*2+2-1; i++){
check &= (sum[i] == sum[i+1]);
}
if(check){
ans = masu; // 代入文
assert(0);
}
}


assert(0)が実行されたとき、まほうじんが解けています。
これをCBMCにかけると、 assert(0)が失敗するような、数字の組み合わせを見つけてくれます。

D:\CBMC>cbmc mahoujin.c --function solve

... 中略 ...

State 354 file mahoujin.c line 49 function solve thread 0
----------------------------------------------------
mahoujin::solve::1::ans={ 6, 1, 8, 7, 5, 3, 2, 9, 4 }

Violated property:
file mahoujin.c line 50 function solve
assertion
FALSE

VERIFICATION FAILED


6 1 8
7 5 3
2 9 4

確かに3x3のまほうじんが解けています。プログラムを修正し、先頭のほうに、
__CPROVER_assume(masu[4] != 5);
を追加します。つまりちょうど真ん中が 5ではないと条件を追加してみます。


... 中略 ...
Runtime decision procedure: 0.312s
VERIFICATION SUCCESSFUL

反例を見つけることができませんでした。3x3のまほうじんでは、真ん中は必ず 5 になることがわかりました。

先頭で定義されているNUMを4にすると4x4のまほうじんが、5にすると5x5のまほうじんが解けます。

4の場合
...
Runtime decision procedure: 3.5s
...
State 808 file mahoujin.c line 49 function solve thread 0
----------------------------------------------------
mahoujin::solve::1::ans={ 4, 7, 10, 13, 14, 16, 1, 3, 5, 9, 8, 12, 11, 2, 15, 6}

5の場合
...
Runtime decision procedure: 141.032s
...
State 1674 file mahoujin.c line 49 function solve thread 0
----------------------------------------------------
mahoujin::solve::1::ans={ 6, 22, 10, 19, 8, 3, 18, 12, 23, 9, 24, 13, 16, 5, 7 , 15, 1, 25, 4, 20, 17, 11, 2, 14, 21 }

3と4は一瞬で解けますが、5はかなり時間がかかります。PCの性能によりますが私のPCの場合、141秒ぐらいかかりました。画面が何も変わらないのでじっと待ちます。

このようにして、プログラムがそこを通過するときに、失敗するようなassertをいれておけば、プログラムがそこを通過する条件がないか総当たりで調べてくれます。

たとえば、ある関数を、引き数がNULLでは絶対に呼んでほしくないときに、NULLで呼び出してくる場所を総当たりで調べてくれる、という使い方ができます。

CBMCは、モデル検査に使うツールなのですが、このように、C言語で使え、モデル全部ができあがっていなくても、1関数だけでも使い道があるところがすばらしいです。

続く。

コメントの投稿

非公開コメント

プロフィール

島敏博

Shima Toshihiro 島敏博
信州アルプスハイランド在住。HaskellとElixirが好き。組み込みソフトウェアアーキテクト、C++プログラマ、山歩き、美術館巡り、和食食べ歩き、日本赤十字社救急法指導員、インデックス投資、クラシック音楽、SESSAME会員、状態マシン設計、モデル駆動開発、ソフトウェアプロダクトライン、Rubyist、実践ビジネス英語

■ ツイッター
http://twitter.com/saltheads
■ Facebook
http://www.facebook.com/saltheads
■ Qiita
http://qiita.com/saltheads

印刷する場合は、ブラウザの印刷メニューではなく、このページの上から3cmくらいの青いところにある、「印刷」を押してみてください。少しうまく印刷できます。まだ完全ではないのですが、これで勘弁してください。


カテゴリ
最新記事
月別アーカイブ
最新コメント
検索フォーム
リンク
sessame
RSSリンクの表示