Frama-C/WP教程示例“失配算法”

Question

我正在尝试使用Frama (Neon-20140301)和Alt的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;
}

Answer 1

您的函数应该返回一个bool，即0或1。任何整数值x都可以转换为_Bool：如果x==0和1不同，则布尔值为0 (参见C99和C11第6.3.1.2节)。如果您看一下由Frama规范的代码，这正是return i和return n所做的工作。因此，\result不应该等于n或两个数组不同的索引。如果将函数改为返回int，则所有内容都由Alt执行。