2

配列の定量化されたアサーションを証明しようとしていますが、いくつかの問題が発生しました。次の小さなプログラムを検討してください。

int a[4] = {1,2,3,4};

/*@ requires p == a;
    assigns \nothing;
*/
void test(int *p)
{
  p++;
  //@ assert \forall int i; 0 <= i < 3 ==> p[i] < 10;
  //@ assert \exists int i; p[i] == 3;
}

「型付き」メモリモデルを使用しています：

frama-c-gui -wp -wp-qed -wp-byreference -wp-model 'Typed' -main test Test.c

何らかの理由で「要求」が成り立たないため、1==2 であってもすべての主張を証明できます。これを克服するために、関数本体でグローバル変数を直接割り当てます。

int a[4] = {1,2,3,4};

/*@  assigns \nothing;
*/
void test(int *p)
{
  p = a;

  p++;
  //@ assert \forall int i; 0 <= i < 3 ==> p[i] < 10;
  //@ assert \exists int i; p[i] == 3;
}

ここで forall は成立しますが、exists は成立しません。存在は、アサーション「p[1] == 3」をその前に追加した場合にのみ保持されます。そのような存在する配列プロパティを証明するには何が欠けていますか? これは、配列エントリに対する検索ループのループ不変条件を表現するために必要です。

ありがとう、ハラルド

4

1 に答える 1

3

「requires」は、誤った単純化によって false に変換されます。次のリリースで修正される予定です。エラーを見つけていただきありがとうございます。

この修正により、Alt-ergo は通常のヒューリスティックを使用して i の証人を見つけることができないため、最後のアサーションはまだ証明されていません。アサーション「p[1] == 3」を追加すると、証人を与えるので、証明が簡単になります。他のいくつかの証明者 (Z3、CVC4) は、この特定の主張を直接証明できます。次回のリリースにご期待ください。

于 2013-01-09T17:04:44.283 に答える