Введение спецификаций математических функций с ACSL/Frama-C

Question

Можно ли реализовать спецификации в ACSL для функций, обычно вызываемых при компиляции с -lm, как sqrt? Я использую его для плагина Frama-C WP.

Вот небольшой пример, чтобы проиллюстрировать, что я хотел бы сделать.

/*@ requires sqrt_spec: \forall float x; 
             \model(sqrt(x)) * \model(sqrt(x)) == \model(x);  
    ensures [...] */  

void f (...) {
double y = sqrt x;
[...]
}

Очевидно, что если я это сделаю, WP плачет, потому что sqrt не существует, когда я использую его в аннотациях.

Ошибка пользователя [kernel]: несвязанная функция sqrt в аннотации

Поэтому я хотел бы определить абстрактный sqrt, но ни один из моих тестов не сработал:

#define sqrt(x) (...)

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

/*@  axiomatic SqrtSpec {
logic real sqrt (real x);
} */

И этот не решает мою проблему:

Ни код, ни спецификация для функции sqrt, генерирующей назначения по умолчанию из прототипа.

Answer 1

Frama-C имеет встроенную логическую функцию \sqrt который работает над real число (обратите внимание, что встроенные функции и предикаты обычно начинаются с обратной косой черты \ чтобы избежать любого столкновения с существующими идентификаторами Си). Тем не менее, не так уж сложно дать аксиоматическое определение sqrt:

axiomatic Sqrt {
  logic real sqrt(real);
  axiom real_def: \forall real x; x >= 0 ==> x == sqrt(x) * sqrt(x);
}

Кроме того, обратите внимание, что Gappa ( http://gappa.gforge.inria.fr/) является единственным автоматическим средством проверки, который знает о числах с плавающей запятой (в отличие от действительных чисел), но даже если вы его установили, выполнение обязательств по проверке Работа с вычислениями с плавающей запятой может быть очень сложной.

Обновить

Если вы хотите аксиоматизировать double sqrt(double) (И / или float sqrt(float)) идея состояла бы в том, чтобы охарактеризовать ошибку относительно результата \sqrt оперируя реалами, то есть чем-то сродни

axiomatic Sqrt {
  logic float sqrt(float sqrt);
  axiom sqrt_def: \forall float x; \is_finite(x) && x>= 0.0 ==> sqrt(x) ==  (float)\sqrt(x);
}

Конечно, эта характеристика может быть немного ограничительной. Вы можете захотеть что-то вроде \abs(sqrt(x) - \sqrt(x)) <= err_bound * \sqrt(x), но я должен признать, что я не достаточно беглый в вычислениях с плавающей точкой, чтобы дать соответствующее значение err_bound от макушки моей головы.

Обновление 2

Предполагая, что у вас есть логика sqrt который имеет свойства, которые вы хотите, говоря, что C sqrt имеет такое же поведение, это просто вопрос заключения контракта с ним:

/*@ requires \is_finite(x); //unless you want to play with NaN or infinities 
    assigns \nothing;
    ensures \result == sqrt(x);
 */
extern float sqrt(float x);

Спецификации функции объединяются на этапе соединения, поэтому не имеет значения, написан ли этот контракт в math.h (Примечание: в стандартном заголовке sqrt берет (и возвращает) double, это sqrtf который работает на float) или в вашем собственном файле.