Блог

Главная - Вопросы по программированию - Почему это простое свойство арифметики с плавающей запятой не может быть проверено с помощью WP?

Почему это простое свойство арифметики с плавающей запятой не может быть проверено с помощью WP?

#frama-c

#frama-c

Вопрос:

Я пытаюсь проверить этот простой пример кода, но не могу найти, что не так. Я сократил его до минимального случая здесь:

 /*@ requires (float)0 <= (float)number < (float)1.0;
    ensures (float)result == (float)((float)1.0 - (float)number);
    ensures (float)((float)result   (float)number) == (float)1.0;
    ensures (float)0 < (float)result <= (float)1.0;
    ensures (float)result > (float)0;
*/
float complement(float number) {
    return (float)1 - number;
}

Я был бы очень благодарен за вашу помощь.
Кроме того, поскольку я обнаружил, что документация по проверке с плавающей запятой несколько скудна, есть ли что-нибудь, что я здесь упускаю из виду?

Комментарии:

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

2. Для этого я использовал alt-ergo. Я знаю о Gappa, но не смог установить его в своей системе.

3. Спасибо за информацию. Однако, покопавшись немного дальше, я боюсь, что поддержка WP с плавающей запятой в настоящее время слишком рудиментарна, чтобы ее можно было действительно использовать.

4. В любом случае спасибо за вашу помощь. Тем не менее, я смог доказать, что некоторые другие алгоритмы с плавающей запятой работают нормально.

5. @Virgile, могу я спросить, где вы «копнули немного дальше», чтобы найти эту информацию? Мне было бы интересно увидеть текущее состояние.