Проверка функции, которая суммирует массив int и массив float, используя FramaC / WP

Question

Я пытаюсь указать и проверить эту простую функцию, которая суммирует массив.Эта спецификация для массива целых чисел принята WP:

/*@ axiomatic Sum_Int {
      logic int sum_int(int *values, integer begin, integer end)
          reads values[begin .. (end - 1)];

      axiom empty_int:
        \forall int *p, integer begin, end; begin >= end
            ==> sum_int(p, begin, end) == 0;

      axiom range_int:
        \forall int *p, integer begin, end; begin < end
            ==> sum_int(p, begin, end) == sum_int(p, begin, end - 1) + p[end - 1];
}
*/

/*@ requires \valid_read(values + (0 .. size - 1));

    assigns \nothing;

    ensures \result == sum_int(values, 0, size);
*/
int sum_int_array(const int *values, size_t size) {
    int sum = 0;
    /*@ loop invariant 0 <= index <= size;
        loop invariant sum == sum_int(values, 0, index);
        loop assigns sum, index;
        loop variant size - index;
    */
    for (size_t index = 0; index < size; index++) {
        sum += values[index];
    }
    return sum;
}

Но та же спецификация для массива с плавающей точкой не может быть доказана WP:

/*@ axiomatic Sum_Real {
      logic float sum_real(float *values, integer begin, integer end)
          reads values[begin .. (end - 1)];

      axiom empty_real:
        \forall float *p, integer begin, end; begin >= end
            ==> sum_real(p, begin, end) == 0;

      axiom range_real:
        \forall float *p, integer begin, end; begin < end
            ==> sum_real(p, begin, end) == sum_real(p, begin, end - 1) + p[end - 1];
}
*/

/*@ requires \valid_read(values + (0 .. size - 1));

    requires \forall integer i; 0 <= i < size ==> \is_finite(values[i]);
    assigns \nothing;

    ensures \result == sum_real(values, 0, size);
*/
float sum_float_array(const float *values, size_t size) {
    float sum = 0;
    /*@ loop invariant 0 <= index <= size;
        loop invariant sum == sum_real(values, 0, index);
        loop assigns sum, index;
        loop variant size - index;
    */
    for (size_t index = 0; index < size; index++) {
        sum += values[index];
    }
    return sum;
}

Аксиоматическое определението же самое (и я думаю, что это должно быть то же самое, если это правильно).Единственное отличие заключается в добавленном предварительном условии для массива с плавающей точкой:

requires \forall integer i; 0 <= i < size ==> \is_finite(values[i]);

Что я не уверен, если это необходимо.Какая информация здесь отсутствует, чтобы WP мог проверить версию с плавающей точкой?