1

我正在尝试使用 Frama-C (Neon-20140301) 和 Alt-Ergo 的 WP 教程示例。我陷入了“不匹配算法”示例，而其他类似示例（例如“相等”和“查找”）没有问题。代码如下所示。后置条件 P0、P2 未放电。谁能告诉我这里有什么问题？

#include<stdbool.h>

/*@
  @ predicate IsEqual {A,B} (float* a, integer n, float* b) =
  @   \forall integer i; 0 <= i < n ==> \at(a[i], A) == \at(b[i], B);
*/a

/*@ requires n >= 0;
  @ requires \valid(a+(0..n-1));
  @ requires \valid(b+(0..n-1));
  @ 
  @ assigns \nothing;
  @ 
  @ behavior all_equal:
  @   assumes IsEqual{Here,Here}(a, n, b);
  @   ensures P0: \result == n;
  @   
  @ behavior some_not_equal:
  @   assumes !IsEqual{Here,Here}(a, n, b);
  @   ensures P1: 0 <= \result < n;
  @   ensures P2: a[\result] != b[\result];
  @   ensures P3: IsEqual{Here,Here}(a, \result, b);
  @   
  @ complete behaviors;
  @ disjoint behaviors;
*/

bool mismatch (float* a, int n, float* b)
{
  /*@ loop invariant 0 <= i <= n;
    @ loop invariant IsEqual{Here,Here}(a, i, b);
    @ loop assigns i;
    @ loop variant n-i;
   */
  for (int i=0; i<n; i++) {
    if (a[i] != b[i])
      return i;
  }
  return n;
}
4

1 回答 1

1

您的函数应该返回一个bool，即 要么0要么1。任何整数值x都可以转换为_Bool：布尔值是0ifx==0和1else（参见 C99 和 C11 第 6.3.1.2 节）。如果您查看 Frama-C 规范化的代码，这正是为return iand所做的return n。因此，没有理由\result应该等于n或两个数组不同的索引。如果你让你的函数返回一个int而不是，一切都由 Alt-ergo 释放。

于 2014-07-19T17:00:12.737 回答