你好我想证明对于一维数组中包含的所有值的平均值的计算，以下是我的程序：
#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;
我做错了什么吗？ 我不知道我的问题是否来自浮点数的精度。 我尝试了很多断言，但仍然不起作用。 在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;
}
}
我保留了assert，但我确定其中很多都是无用的。
fabs(average(...) - average) < epsilon- Eugene Sh.float？ - Guillaume Petitjeantypedef unsigned int size_t;类型size_t在头文件stdio.h中定义，并被定义为：long unsigned int你为什么要尝试重新定义它？ - user3629249