作为作业，我决定尝试使用带有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,rightmost); // Recursively sort the right side of pivot
}
作为旁注，我知道wp不支持递归，因此在运行decreases时忽略了Frama-c -wp -wp-rte语句。
这是gui中的结果：
您可以看到，即使对我来说有意义，我的循环不变式也没有得到验证。
Frama-c在不支持递归的情况下能够在假设下验证第二个递归调用。据我了解，该呼叫quickSort(t,counter-2)未得到验证，因为它可能违反先决条件requires 0 <= rightmost。不过，我不太确定那种情况下的Frama-c行为以及如何解决它。
我想要一些有关正在发生的事情的信息。我认为不验证不变量与递归无关，即使通过删除递归调用也不会对其进行验证。最后，您能否向我解释在递归调用的情况下Frama-c的行为是什么？是将它们视为其他任何函数调用，还是我不了解的行为？
谢谢