Как мне доказать код с реальным аксиоматическим во Frama-C

Question

Я изменил тип int на float в коде "Внутренний продукт" из книги ACSL-by-Example (код с типом int работал для меня), и теперь я не могу доказатьинвариант цикла inner.Я добавил некоторые проверки для инф и NaN без какого-либо успеха.

#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;
}

Как пройти?Где взять хорошие случаи с доказательствами реальных вычислений?

И, честно говоря, я бы хотел доказать, что мой цикл инвариантен для синуса.Я создал для него лемму (ограниченную серию Синус Тейлор) и проверил ее как функцию.И я не знаю, как начать доказывать это.

/*@
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 и т. Д., Но мы не можем доказать \result==\sin(x) для sin(x) возвращающей функции.Или я здесь не прав?

Answer 1

Относительно второй части вашего вопроса, кажется, есть некоторое глубокое недопонимание относительно семантики аксиоматики ACSL.В частности:

• Ваша SinnnEmpty аксиома в основном говорит о том, что для любых x и sum у нас есть Sinnn(x,sum,0,0,0) == sum (в основном, я только что создал current, i и i_max с 0, что делает левую часть импликации истинной).Маловероятно, что вы хотели сказать это
• SinnnMemCmp - тавтология.Фактически, внутри глобальных аннотаций конструктивные и логические метки \at() предназначены для того, чтобы говорить о C переменных и местах памяти.Здесь у вас есть только чисто логические переменные, связанные универсальной квантификацией: они неизменны и не привязаны к состоянию памяти C, то есть их значение не зависит от логической метки.

Наконец, один развы разобрались со своим определением того, что Sinnn должен делать с точки зрения ACSL (т. е. играя с математическими реалами, которые успешно игнорируют проблемы округления), вы столкнетесь с проблемой проверки того, что результаты, применимые на этом математическом уровне,все еще верно при вычислениях с числами с плавающей запятой конечной точности.Обычно это трудная задача, и не все автоматизированные средства проверки имеют хорошую поддержку для вычислений с плавающей точкой (см., Например, этот документ для получения дополнительной информации).

Answer 2

Я собираюсь ответить на первую часть вашего вопроса.Проблема заключается в аксиоме InnerProductNext, точнее здесь InnerProduct(a, b, n + 1, init) == InnerProduct(a, b, n, init) + a[n] * b[n].Спецификация ACSL использует реальную арифметику, а ваша функция использует 32-битные вычисления с плавающей запятой.Из-за округления, которое происходит в функции C, доказательство не может быть достигнуто.Исправление достаточно простое: округлите все операции в вашей лемме соответствующим образом.

  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]));

Этого достаточно для успеха доказательства.