了解如何正确使用post-condition和loop-invariant与Frama-c

Question

我试图在此示例中证明返回值将为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); 
@*/ 

和循环不变，因为邮资-C是基于霍尔逻辑：

/*@ 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; 
    @*/ 

我相当肯定，我错过了一些线路上，我试图使用所有 和存在。 我花了数小时试图理解，如何正确检查，如果任何值分配给数组或不，但我觉得我卡在这里。 我真的很感谢你的帮助:)

Answer 1

你的代码有几个问题。首先，你似乎混合了size和length。我冒昧地在各处使用size，否则这个代码甚至不会被C编译器接受，更不用说Frama-C。其次，\forall integer i; 0<= i < size && array[i] != 8（和相应的循环不变量）不正确。从字面上看，这意味着任何整数i验证既即i是0和和array[i]之间size不是8。以101为i给出了这个命题的一个微不足道的例子。你想表达的是什么，对于任何整数i，如果i是0和size之间，然后array[i]不8，其表示为\forall integer i; 0<= i < size ==> array[i] != 8。另一方面，当在\exists下使用时，&&连接器是正确的：这次我们确实想要找到i，使得i在该数组的范围内，并且为array[i]==8。然而，在你上确保了第二&&是不正确的：你想说那是什么如果有这样的i，然后\result == 1，因此你必须在这里的含义：(\exists integer i; 0<= i < size && array[i] == 8) ==> (fi8 == 1)

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

​​

所有证明义务已解除。