如何在Frama-C中使用真实公理证明代码 [英] How do I prove code with a real axiomatic in Frama-C
问题描述
我已从ACSL-by-Example的内部产品"代码中将int
类型更改为float
(具有int
类型的代码对我有用),现在我无法证明循环不变式inner
.我为inf和NaN添加了一些检查,但没有成功.
I have changed the int
type to float
in the "Inner Product" code from the ACSL-by-Example book (the code with int
type worked for me) and now I am not able to prove the loop invariant inner
. I have added some checks for inf and NaN without any success.
#include "limits.h"
/*@
predicate Unchanged{K,L}(float* a, integer first, integer last) =
\forall integer i; first <= i < last ==>
\at(a[i],K) == \at(a[i],L);
predicate Unchanged{K,L}(float* a, integer n) =
Unchanged{K,L}(a, 0, n);
lemma UnchangedStep{K,L}:
\forall float *a, integer n;
0 <= n ==>
Unchanged{K,L}(a, n) ==>
\at(a[n],K) == \at(a[n],L) ==>
Unchanged{K,L}(a, n+1);
lemma UnchangedSection{K,L}:
\forall float *a, integer m, n;
0 <= m <= n ==>
Unchanged{K,L}(a, n) ==>
Unchanged{K,L}(a, m);
*/
/*@ axiomatic InnerProductAxiomatic
{
logic real InnerProduct{L}(float* a, float* b, integer n, float init)
reads a[0..n-1], b[0..n-1];
axiom InnerProductEmpty:
\forall float *a, *b, init, integer n;
n <= 0 ==> InnerProduct(a, b, n, init) == init;
axiom InnerProductNext:
\forall float *a, *b, init, integer n;
n >= 0 ==>
InnerProduct(a, b, n + 1, init) ==
InnerProduct(a, b, n, init) + a[n] * b[n];
axiom InnerProductRead{L1,L2}:
\forall float *a, *b, init, integer n;
Unchanged{L1,L2}(a, n) && Unchanged{L1,L2}(b, n) ==>
InnerProduct{L1}(a, b, n, init) ==
InnerProduct{L2}(a, b, n, init);
}*/
/*@
predicate ProductBounds(float* a, float* b, integer n) =
\forall integer i; 0 <= i < n ==>
(INT_MIN <= a[i] * b[i] <= INT_MAX) ;
predicate InnerProductBounds(float* a, float* b, integer n, float init) =
\forall integer i; 0 <= i <= n ==>
INT_MIN <= InnerProduct(a, b, i, init) <= INT_MAX;
*/
/*@
requires valid_a: \valid_read(a + (0..n-1));
requires valid_b: \valid_read(b + (0..n-1));
requires \is_finite(init);
requires !\is_NaN(init);
requires bounds: ProductBounds(a, b, n);
requires bounds: InnerProductBounds(a, b, n, init);
requires (n < 100) && (n>=0);
requires \forall integer i; 0 <= i < n ==> \is_finite(a[i]);
requires \forall integer i; 0 <= i < n ==> \is_finite(b[i]);
requires \forall integer i; 0 <= i < n ==> !\is_NaN(b[i]);
requires \forall integer i; 0 <= i < n ==> !\is_NaN(a[i]);
assigns \nothing;
ensures result: \result == InnerProduct(a, b, n, init);
ensures unchanged: Unchanged{Here,Pre}(a, n);
ensures unchanged: Unchanged{Here,Pre}(b, n);
*/
float inner_product(const float* a, const float* b, int n, float init)
{
int i = 0;
/*@
loop invariant index: 0 <= i <= n;
loop invariant inner: init == InnerProduct(a, b, i, \at(init,Pre));
loop assigns i, init;
loop variant n-i;
*/
while (i < n) {
init = init + a[i] * b[i];
i++;
}
return init;
}
我如何通过?哪里有真实计算证明的好案例?
How can I pass? Where to get the good cases with proves of real computations?
坦白地说,我想证明Sine的循环不变.我为此创建了一个引理(有界Sine Taylor级数)并将其作为函数进行了测试.而且我不知道如何开始证明它.
And frankly speaking I would like then to prove my loop invariant for Sine. I created a lemma for it (bounded Sine Taylor series) and tested it as a function. And I don't know a way how to start proving it.
/*@
axiomatic SinNAxiomatic
{
logic real Sinnn {l} (real x, real sum, real current, integer i, integer i_max);
axiom SinnnEmpty: \forall real x, real sum, real current, integer i, integer i_max; (\abs(current) < 0.00001) || (i == i_max) ==> Sinnn(x, sum, current, i, i_max)
== sum + current;
axiom SinnnNext: \forall real x, real sum, real current, integer i, integer i_max; \abs(current) > 0.00001 ==> Sinnn(x, sum, current, i, i_max) ==
Sinnn(x, sum + current, current * (-1.0 * x * x / ((2 * i) * (2 * i + 1))), i + 1, i_max);
lemma SinnnMemCmp{L1,L2}: \forall real x, real sum, real current, integer i, integer i_max;
\at(x, L1)==\at(x, L2) && \at(sum, L1)==\at(sum, L2) && \at(current, L1)==\at(current, L2) && \at(i, L1)==\at(i, L2) && \at(i_max, L1)==\at(i_max, L2)
==> Sinnn{L1}(x, sum, current, i, i_max) == Sinnn{L2}(x, sum, current, i, i_max);
}
*/
float SinTailor(float x) {
float n = x;
float sum = 0.0;
int i = 1;
/*@
loop invariant over: \abs(sum - Sinnn(x, 0, x, 1, i - 1)) <= 0.001;
loop assigns sum, n, i;
*/
do
{
sum += n;
n *= -1.0 * x * x / ((2 * i) * (2 * i + 1));
i++;
//printf("sum my=%f recursion=%f\n", sum, TestSinnn(x, 0, x, 1, i - 1)); //prints the same values
}
while (fabs(n)> 0.00001);
return sum;
}
我注意到对于内部\sin
,存在一些-1<=\sin(x)<=1, \cos^2(x)+\sin^2(x)==1
等引理,但是对于sin(x)
返回函数,我们无法证明\result==\sin(x)
.还是我在这里错了?
I noticed that for internal \sin
there are a few lemmas like -1<=\sin(x)<=1, \cos^2(x)+\sin^2(x)==1
, etc., but we cannot prove \result==\sin(x)
for a sin(x)
returning function. Or am I wrong here?
推荐答案
我将回答您问题的第一部分.问题出在公理InnerProductNext
,更确切地说是InnerProduct(a, b, n + 1, init) == InnerProduct(a, b, n, init) + a[n] * b[n]
. ACSL规范使用实数运算,而您的函数使用32位浮点计算.由于在C函数中发生舍入,因此无法获得证明.修复非常简单:在引理中适当舍入所有操作.
I'm going to answer the first part of your question. The problem lies in the axiom InnerProductNext
, more precisely here InnerProduct(a, b, n + 1, init) == InnerProduct(a, b, n, init) + a[n] * b[n]
. ACSL specification use real arithmetics, while your function use 32 bits floating point computation. Due to the rounding that occurs in the C function, the proof cannot be achieved. The fix is simple enough: round all operations appropriately in your lemma.
axiom InnerProductNext:
\forall float *a, *b, init, integer n;
n >= 0 ==>
InnerProduct(a, b, n + 1, init) ==
(float)(InnerProduct(a, b, n, init) + (float)(a[n] * b[n]));
这足以证明成功.
这篇关于如何在Frama-C中使用真实公理证明代码的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!