2010/06/03

回文数式作成プログラム

プログラム検証ツールを使って回文数式を作る。
例えば

42+46=64+24


// 回文数式作成
void main()
{
  int a1, a2, b1, b2, A1, A2, B1, B2;
  __CPROVER_assume(a1 > 0 && a1 <10 && a2 > 0 && a2 < 10 && b1 > 0 && b1 < 10 && b2 > 0 && b2 < 10);
  A1 = 10*a1 + a2;
  A2 = 10*a2 + a1;
  B1 = 10*b1 + b2;
  B2 = 10*b2 + b1;

  assert((A1+B1) != (A2+B2));
}

このプログラムをCBMCに掛ければ検証に失敗して

State 7 file anagram.c line 9 function main thread 0
----------------------------------------------------
  anagram::main::1::A1=42 (00000000000000000000000000101010)

State 8 file anagram.c line 10 function main thread 0
----------------------------------------------------
  anagram::main::1::A2=24 (00000000000000000000000000011000)

State 9 file anagram.c line 11 function main thread 0
----------------------------------------------------
  anagram::main::1::B1=46 (00000000000000000000000000101110)

State 10 file anagram.c line 12 function main thread 0
----------------------------------------------------
  anagram::main::1::B2=64 (00000000000000000000000001000000)

State 11 file anagram.c line 14 function main thread 0
----------------------------------------------------
  c::main::$tmp::tmp$1=FALSE

Violated property:
  file anagram.c line 14 function main
  assertion (A1+B1) != (A2+B2)
  FALSE

VERIFICATION FAILED

を得ることができる。

7/1 追加
魔方陣の解き方
CBMCで魔方陣を作成するプログラムが公開されています。

2010/05/30

単体テストできない関数

ヨーロッパの鉄道の安全規格[1]で一番厳しいSIL4ではブランチテストの100%カバレッジが求められるらしい。if文がネストしている複雑な関数の場合、そこにたどり着く入力データを作り出すのはなかなか難しい。CBMCを使って簡単にテストデータを生成する方法としてassert(0)を埋め込む方法がある。到達したい場所にassert(0)を仕込んで置いてCBMCで検証をすればCBMCが向きになってそこまで行って転けてくれるのでたどり着く方法が明確になる。必要があればprintf文も仕込んでおく、さらにテキストファイルに書き出すようにすれば、テストツールに掛けられる形でテストケースを得ることができる。


しかし、この方法も構造化されたプログラムでないとうまく行かない。構造化されたプログラムというのは、逐次、分岐、繰り返し構造だけでできているプログラムで、前方に跳ぶgoto文とか入れ子にならない繰り返しを持っていないプログラムである。今時、この様なプログラムはアセンブラで書かれたOSのディスパッチャぐらいだろう。ところが、並列性がある場合は任意のgoto文が動的に入るのと同じだからうまく行かない。要するに単体テストできないのと同じである。
グローバル変数を使っていても並列性が無ければ単体テストはできるが、それがvolatileなものだとそうはいかない。いちいちvolatile宣言しないとテスト以前にコンパイルがチャンとできているか心配になる。



並列性がある場合には、節操なくグローバル数を使うことは控えなければならない。空海がどのように並列に文章を書くのか、文章だけはできていて出力だけが並列なのか、文章も考えながらつじつまの合うものを書き出すのか、これはアーキテクチャがぶれていては実現できない。
グローバル変数を多用して、並列性のあるシステムを作っていて、単体テストもチャンとやってますとか言う組織は多いけれどどんな単体テストをやっているのだろうか。

[1] European Committee forElectrotechnical Standardization. Railway Applications -
Communication, signalling and processing systems - Software forrailway control
and protection systems, http://www.cenelec.eu