无法证明frama-C中的功能

Question

我在 frama C 中的函数证明方面遇到问题。我用于证明的代码如下所示：

#include <limits.h>
/*@ 
    requires len>=0 && \valid(arr + (0 .. len-1));
    ensures 0<= \result < len;
    ensures \forall integer j; 0 <= j < len ==> arr[j] < \result;
    assigns \nothing;
*/

int find_min(int* arr, int len)
{
   int min;
   min=arr[0];
    /*@ 
        loop invariant \forall integer j; 0 <= j < i ==> arr[j] < min;
        loop invariant 0 <= min < i <= len;
        loop assigns min , i;
        loop variant len -i;
    */
    for (int i = 0; i < len; i++)
    {
        if (arr[i] < min)
        {
            min = arr[i];
        }
    }
    return min;
}

void main (void)
{
    int a[] = {3, 5, 18, 12, 12};
    int r = find_min(a, 5);
    //@ assert r == 3;
}

这是一个尝试寻找最小数组值的程序。程序的结果将用于证明变量是否满足 frama-C 中使用的条件。

我目前陷入了这种不变性：

在得出这个结论之前我已经做了各种方法，包括改变“确保..”，但每当我这样做时，证明的目标就会从13/14减少到12/14，因此我目前不确定要改变什么来增加证明目标到 14/14。我真的需要这方面的帮助，因为我对 frama C 非常陌生。非常感谢有关此问题的任何回复。

Answer 1

您的规范中确实存在几个问题。首先，主要的

ensures

子句与您的描述不一致：

尝试查找最小的数组值

暗示您想要类似

\result < arr[j]

的东西。此外，由于这应该是最小的，所以应该有一个满足等式的索引，即您应该使用

<=

而不是

<

。总而言之，我们应该有

ensures small_value: \forall integer j; 0 <= j < len ==> \result <= arr[j]

（注意：为您的子句命名（此处

small_value

）总是一件好事，这样可以更轻松地在日志中识别它们）

此外，您返回的是最小值，而不是其索引，因此您的第一个

ensures

子句是不正确的。

最后对于合约，

requires

条款中也有一个小问题，只有当您使用

-wp-rte

来确保除了验证合约本身之外不存在运行时错误时，这个问题才会变得明显：因为您总是查看在

arr[0]

，你不能有一个空数组，即你必须有

len > 0

。

现在，让我们看一下不变量：必须更新第一个不变量以反映

ensures

中的变化。正如评论中提到的，第二个应该只讨论

i

的间隔，

min

没有理由在这些范围内。而

i

可以是

0

（其实进入循环的时候就是

0

）。

有了这一切，你就可以证明

f

履行了它的合同。然而，这不足以证明

main

中的断言。也就是说，

min_value

仅确保您返回较小的值，而不是最小的。为此，我们需要另一个保证，即

ensures min_so_far: \exists integer i; 0<= i < len && \result == arr[i];

当然还有相应的不变量

loop invariant min_so_far_2: \exists integer j; 0<= j < i && min == arr[j] || min == arr[0];

（请注意，

min_so_far_2

需要特殊情况来考虑我们以

min == arr[0]

开始循环的事实）

总结一下，有以下文件

#include <limits.h>
/*@ 
    requires valid_arr: len>0 && \valid(arr + (0 .. len-1));
    ensures small_value: \forall integer j; 0 <= j < len ==> \result <= arr[j];
    ensures min_value: \exists integer i; 0<= i < len && \result == arr[i];
    assigns \nothing;
*/

int find_min(int* arr, int len)
{
   int min;
   min=arr[0];
    /*@ 
        loop invariant small_so_far: \forall integer j; 0 <= j < i ==> min<=arr[j];
        loop invariant min_so_far: \exists integer j; 0<= j < i && min == arr[j] || min == arr[0];
        loop invariant loop_index: 0 <= i <= len;
        loop assigns min , i;
        loop variant len -i;
    */
    for (int i = 0; i < len; i++)
    {
        if (arr[i] < min)
        {
            min = arr[i];
        }
    }
    return min;
}

void main (void)
{
    int a[] = {3, 5, 18, 12, 12};
    int r = find_min(a, 5);
    //@ assert r == 3;
}

和 Frama-C 28.0 + Why3 1.6.0 + Alt-Ergo 2.5.2

frama-c -wp -wp-rte example.c

证明了所有验证条件。