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

Question

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

/*@ 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;
}

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