c - 证明数组的平均值

Question

你好，我想证明一维数组中包含的所有值的平均值的计算，

到目前为止我有以下程序:

#include <stdbool.h>

typedef unsigned int size_t;
typedef struct Average avg;
struct Average
{
    bool success;
    float average;
};
/*@
axiomatic Float_Div{
    logic real f_div(real a,real b) = a/b ;

    axiom div:
        \forall real q,a,b;  0 != b ==>
        (a == b*q <==> q == f_div(a, b));

    axiom split :
        \forall real q,a,b,c;  0 != b ==>
        f_div(a + c , b) == f_div(a,b) + f_div(c,b);

}

axiomatic Average {
    logic real average(int * t, integer start, integer stop, integer size);

    axiom average_0:
        \forall int *t, integer start , integer stop, size;
        start >= stop ==> average(t,start, stop, size) == 0;

    axiom average_n:
        \forall int *t, integer start , integer stop, integer size;
        start < stop && size >0  ==>
        average(t,start, stop, size) ==
        f_div((real)stop-1 ,(real) size) +( average(t,start, stop-1, size) );

    axiom average_split :
        \forall int *t, integer start ,integer middle, integer stop, integer size;
        start < middle < stop && size >0  ==>
        average(t,start, stop, size) ==  average(t,start, middle, size) + average(t,middle, stop, size);

    axiom average_unit :
        \forall int *t, integer start , integer stop, integer size;
        start == stop-1 && size >0  ==>
        average(t,start, stop, size) == f_div((real)stop-1 ,(real) size);

}

*/


/*@
requires \valid(array + (0..size-1));
ensures (!\result.success) ==> size == 0 ;
ensures (\result.success) ==> \result.average == average(array, 0, size, size);
assigns \nothing;
*/
avg average(int * array, size_t size){
    avg ret;
    ret.success = true ;
    ret.average = 0 ;
    if (size == 0){
        ret.success = false;
        return ret;
    }
    float average = 0;
    /*@
    loop assigns i, average;
    loop invariant 0 <= i <= size;
    loop invariant  average(array , 0, i , size) == average;
    */
    for (size_t i = 0 ; i < size ; i ++){
        float value = ((float)array[i] / size);
        average += value;
    }
    ret.average = average ;
    return ret;
}

frama-c 未能成功证明此循环不变式:

loop invariant  average(array , 0, i , size) == average;

我做错了什么吗？我不知道我的问题是否来自 float 的精度。我尝试了很多断言，但它也不起作用它可以在 Frama-c 中完成吗？

编辑:

我终于证明了我的功能，我在加和之前先做除法，因为每次我尝试先求和都会溢出。

问题是我需要证明我的总和没有溢出。所以我导入了 limits.h并添加一个新的循环不变量:INT_MIN * i <= sum <= INT_MAX * i;所以我的代码现在看起来像这样:

#include <stdbool.h>
#include <limits.h>

typedef unsigned int size_t;
typedef struct Average avg;
struct Average
{
    bool success;
    long long average;
};
/*@
axiomatic Sum{
    logic integer sum(int * t , integer start, integer end);

    axiom sum_false :
        \forall int *t, integer start , integer stop;
        start >= stop ==> sum(t,start,stop) == 0;

    axiom sum_true_start :
        \forall int *t, integer start , integer stop;
        0 <= start < stop ==>
        sum(t,start,stop) == sum(t,start,start+1) + sum(t,start+1,stop);

    axiom sum_true_end :
        \forall int *t, integer start , integer stop;
        0 <= start < stop ==>
        sum(t,start,stop) == sum(t,start,stop-1) + sum(t,stop-1,stop);

    axiom sum_split :
        \forall int *t, integer start , integer stop, integer middle;
        0 <= start<=  middle < stop ==>
        sum(t,start,stop) == sum(t,start,middle) + sum(t,middle,stop);


    axiom sum_alone :
        \forall int *t, integer start;
        (0<=start)
        ==>
        sum(t,start,start+1) == t[start] ;
}

*/
/*@
requires \valid(array + (0..size-1));
ensures (!\result.success) ==> size == 0 ;
ensures (\result.success) ==> (\result.average == sum(array,0,size)/size) ;
assigns \nothing;
*/
avg average(int * array, size_t size){
    //we use a structure to be sure that the function finish without error
    avg ret;
    ret.success = true ;
    ret.average = 0 ;
    if (size == 0){
        //if the size == 0 the function will fail
        ret.success = false;
        return ret;
    }
    else{
        /*
        the average is the sum of all the element of the array divided by the size
        An int is between - 2^15-1 and 2^15-1 that imply that the sum of
        all the element of an array is between
        -2^15 * size and 2^15 * size as size is between 0 and 2^16
        the sum is between -2^31 and 2^31
        a long long is between -2^63 and 2^63

        the sum of all the element can be inside a long long.
        */
        long long sum = 0;

        /*@
        loop assigns i, sum ;
        loop invariant 0 <= i <= size;
        loop invariant sum == sum(array,0,i);
        loop invariant INT_MIN * i <= sum <= INT_MAX * i;
        */
        for (size_t i = 0 ; i < size ; i ++){
            //@assert INT_MIN * i <= sum <= INT_MAX * i;

            sum += array[i];
            //@assert  i+1 <= size;

            //@assert INT_MIN * (i+1) <= sum <= INT_MAX * (i+1);
            //@assert ((LLONG_MIN < INT_MIN * size ) && (LLONG_MAX > INT_MAX* size));
            //@assert LLONG_MIN <= sum <= LLONG_MAX;

            //@assert sum == sum(array,0,i) + array[i];

        }
        ret.average = sum/size ;
        return ret;
    }
}

我让断言，但我确信其中很多都是无用的。

Answer 1

I want to prove the computation of the average of all the values contained in a 1d array

对于精确的数学，避免 float 。

因为 array[] 是 int，坚持使用整数数学。

建议重写代码。
用于测试“一维数组中包含的所有值的平均值”的伪代码

// Compute sum of all elements of the array
wide_integer_type sum = 0
for (i=0; i<n; i++) 
  sum += array[i]

for (i=0; i<n; i++) 
  // below incurs no rounding like `array[i] == (double)sum/n` might
  if ((cast to wide_integer_type)array[i] * n == sum) 
    print "average found!" sum/n