回文数式作成プログラム

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

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で魔方陣を作成するプログラムが公開されています。