0

我试图在这个例子中证明返回值将是 0（如果 8 不在数组中）或 1（如果 8 在数组中）。

int fi8(int *array, int size) {
  int fi8 = 0;
  int i = 0;
  for(i = 0; i < length; ++i)
  {
     if(array[i] == 8)
     fi8 = 1;
  }
  return fi8;
}

我创建了前置和后置条件：

/*@ requires 0 <= size <= 100;
@  requires  \valid(array+(0..size-1));
@  assigns \nothing;
@  ensures (\forall integer i; 0<= i < size && array[i] != 8)  ==> (\result == 0);
@  ensures (\exists integer i; (0<= i < size && array[i] == 8)) && (\result == 1);
@*/

和循环不变量，因为 Frama-C 基于 Hoare Logic：

/*@ loop invariant 0 <= i <= length;
  @  loop invariant  fi8 == 0 || fi8 == 1;
  @  loop invariant (\forall integer i; 0<= i < size && array[i] != 8)
      ==> (fi8 == 0);
  @  loop invariant (\exists integer i; (0<= i < size && array[i] == 8)) 
      && (fi8 == 1);
  @  loop assigns i, fi8;
  @*/

我很确定我在尝试使用 forall 并存在的地方遗漏了一些东西。我花了几个小时试图理解，如何正确检查，是否在数组上分配了任何值，但我觉得我被困在这里。我真的很感谢你的帮助:)

4

1 回答 1

3

您的代码存在一些问题。首先，您似乎混合了size和length。我冒昧地size在任何地方使用，否则这个代码甚至不会被 C 编译器接受，更不用说 Frama-C 了。其次，\forall integer i; 0<= i < size && array[i] != 8（以及相应的循环不变量）不正确。从字面上看，这意味着任何整数都i验证介于和和不是之间。Take for为这个命题提供了一个微不足道的反例。你要表达的是，对于任何整数，如果在and之间，则不是，表示为i0 sizearray[i]8101ii i0size array[i]8\forall integer i; 0<= i < size ==> array[i] != 8. 另一方面，&&连接器在 : 下使用时是正确的\exists：这一次我们确实想要找到一个在数组范围内的i这样，并且对于它。但是，您最后一个确保中的第二个是不正确的：您想说的是，如果存在这样的, 那么，因此您必须在这里暗示：iarray[i]==8&&i\result == 1(\exists integer i; 0<= i < size && array[i] == 8) ==> (fi8 == 1)

最后一个问题是你的循环不变量。当它已经是 C 变量时，您将其重新用作量化变量，这通常不是一个好主意。事实上，这是一个真正的问题，因为您要表达的属性是，只要我们没有看到8之间的0和i，fi8==0（以及双重的，如果看到了8，fi8==1），i就是 C 变量。如果您j在量化中使用，如

 loop invariant (\forall integer j; 0<= j < i ==> array[j] != 8) ==> (fi8 == 0);
 loop invariant (\exists integer j; 0<= j < i && array[j] == 8) ==> (fi8 == 1);

所有证明义务均已履行。

于 2014-11-23T17:10:55.697 回答