[作为作业,我决定尝试使用带有wp和rte插件的frama-c来验证quicksort的实现(取自here)。请注意,第一个最左端为0,最右端等于size-1。这是我的证明。
/*@
requires \valid(a);
requires \valid(b);
ensures *a == \old(*b);
ensures *b == \old(*a);
assigns *a,*b;
*/
void swap(int *a, int *b)
{
int temp = *a;
*a = *b;
*b = temp;
}
/*@
requires \valid(t +(leftmost..rightmost));
requires 0 <= leftmost;
requires 0 <= rightmost;
decreases (rightmost - leftmost);
assigns *(t+(leftmost..rightmost));
*/
void quickSort(int * t, int leftmost, int rightmost)
{
// Base case: No need to sort arrays of length <= 1
if (leftmost >= rightmost)
{
return;
} // Index indicating the "split" between elements smaller than pivot and
// elements greater than pivot
int pivot = t[rightmost];
int counter = leftmost;
/*@
loop assigns i, counter, *(t+(leftmost..rightmost));
loop invariant 0 <= leftmost <= i <= rightmost + 1 <= INT_MAX ;
loop invariant 0 <= leftmost <= counter <= rightmost;
loop invariant \forall int i; leftmost <= i < counter ==> t[i] <= pivot;
loop variant rightmost - i;
*/
for (int i = leftmost; i <= rightmost; i++)
{
if (t[i] <= pivot)
{
/*@assert \valid(&t[counter]);*/
/*@assert \valid(&t[i]);*/
swap(&t[counter], &t[i]);
counter++;
}
}
// NOTE: counter is currently at one plus the pivot's index
// (Hence, the counter-2 when recursively sorting the left side of pivot)
quickSort(t, leftmost, counter-2); // Recursively sort the left side of pivot
quickSort(t, counter, rightmost); // Recursively sort the right side of pivot
}
作为旁注,我知道wp不支持递归,因此在运行decreases
时忽略了Frama-c -wp -wp-rte
语句。
您可以看到我的循环不变量即使对我来说也没有经过验证。
Frama-c在不支持递归的情况下,可以在假设下验证第二个递归调用。据我了解,呼叫quickSort(t, leftmost, counter-2)
未得到验证,因为它可能违反前提条件requires 0 <= rightmost
。我不太确定那种情况下的Frama-c行为以及如何解决。
我想了解发生了什么。我认为不验证不变量与递归无关,即使通过删除递归调用也不会对其进行验证。最后,您能否向我解释在递归调用的情况下Frama-c的行为是什么?是否将它们视为其他任何函数调用,还是我不知道的行为?
谢谢
首先,与Eva不同,除了证明终止,WP没有递归函数的实际问题,它完全正交以证明后置条件成立每次函数返回(这意味着我们没有以证明不终止情况的任何内容):在文献中,当您还可以证明函数始终终止时,这称为部分正确性与总正确性。 decreases
子句仅用于证明终止,因此,如果您希望完全正确,则不支持该事实只是一个问题。对于部分正确性,一切都很好。
即,为了部分正确,递归调用与其他调用一样被对待:您获得了被调用方的合同,证明前提在此刻保持不变,并尝试证明调用方的后置条件,前提是通话后,被呼叫者的后置条件成立。递归调用实际上对开发人员来说更容易:由于调用者和被调用者是相同的,因此您只需编写一份合同即可。]
现在关于失败的证明义务:当循环不变式的“已建立”部分失败时,开始进行调查通常是一个好主意。与保留相比,这通常是一个更简单的证明义务:对于已建立的部分,您想证明注释是在您第一次遇到循环时保持的(即,这是基本情况),而对于保留,您必须证明如果在任意循环步骤的开始时假设不变为真,则在所述步骤的结尾保持不变(即,归纳情况)。特别是,您不能从前提条件推断出right_most+1 <= INT_MAX
。即,如果您有rightmost == INT_MAX
,则会遇到问题,尤其是最终的i++
会溢出。为了避免这种算术上的微妙,将size_t
用作leftmost
并考虑rightmost
是要考虑的最大偏移量之后的方法可能更简单。但是,如果您要求leftmost
和rightmost
都严格小于INT_MAX
,则可以继续进行。
但是,还不是全部。首先,您的边界计数器不变性太弱。您想要的是counter<=i
,而不仅仅是counter<=rightmost
。最后,有必要保护递归调用,以免违反leftmost
或rightmost
的前提条件,以防万一枢轴被错误选择并且您的原始索引接近极限(即counter
最终成为0
或1
因为枢轴太小,或者INT_MAX
因为枢轴太大。在任何情况下,只有当相应的边为空时,才会发生这种情况。
最后,以下代码由WP(Frama-C 20.0钙,使用-wp -wp-rte
完全证明:]
#include <limits.h>
/*@
requires \valid(a);
requires \valid(b);
ensures *a == \old(*b);
ensures *b == \old(*a);
assigns *a,*b;
*/
void swap(int *a, int *b)
{
int temp = *a;
*a = *b;
*b = temp;
}
/*@
requires \valid(t +(leftmost..rightmost));
requires 0 <= leftmost < INT_MAX;
requires 0 <= rightmost < INT_MAX;
decreases (rightmost - leftmost);
assigns *(t+(leftmost..rightmost));
*/
void quickSort(int * t, int leftmost, int rightmost)
{
// Base case: No need to sort arrays of length <= 1
if (leftmost >= rightmost)
{
return;
} // Index indicating the "split" between elements smaller than pivot and
// elements greater than pivot
int pivot = t[rightmost];
int counter = leftmost;
/*@
loop assigns i, counter, *(t+(leftmost..rightmost));
loop invariant 0 <= leftmost <= i <= rightmost + 1;
loop invariant 0 <= leftmost <= counter <= i;
loop invariant \forall int i; leftmost <= i < counter ==> t[i] <= pivot;
loop variant rightmost - i;
*/
for (int i = leftmost; i <= rightmost; i++)
{
if (t[i] <= pivot)
{
/*@assert \valid(&t[counter]);*/
/*@assert \valid(&t[i]);*/
swap(&t[counter], &t[i]);
counter++;
}
}
// NOTE: counter is currently at one plus the pivot's index
// (Hence, the counter-2 when recursively sorting the left side of pivot)
if (counter >= 2)
quickSort(t, leftmost, counter-2); // Recursively sort the left side of pivot
if (counter < INT_MAX)
quickSort(t, counter, rightmost); // Recursively sort the right side of pivot
}