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 成立，但存在不成立。只有当我在它之前添加断言“p [1] == 3”时，存在才成立。证明这种存在数组属性缺少什么？我需要这个来表达数组条目上搜索循环的循环不变量。

谢谢，哈拉尔

4

1 回答 1

3

错误的简化将“要求”转换为错误。它将在下一个版本中更正。感谢您发现错误。

修复后，Alt-ergo 仍然无法证明最后一个断言，因为它无法使用其通常的启发式方法找到 i 的见证。当您添加断言“p [1] == 3”时，您会给出证人，这就是为什么它更容易证明的原因。其他一些证明者（Z3、CVC4）将能够直接证明这个特定的断言。请继续关注下一个版本。

于 2013-01-09T17:04:44.283 回答