Есть в наличии «\ NearestEven» в рамка-c Алюминий-20160501?

Question

ACSL implementation (Версия 1.11 Выполнение в Алюминии-20160501) перечисляет \NearestEven как режим округления (стр. 23). Однако, похоже, он пока недоступен во время выполнения. Когда я побежал следующий код:

/*@ requires 0x1p-967 <= C <= 0x1p970; 
    @ ensures \result == \round_double(\NearestEven, (x+y)/2) ; 
    @ */ 

double average(double C, double x, double y) { 
    if (C <= abs(x)) 
    return x/2+y/2; 
    else 
    return (x+y)/2; 
} 

с помощью следующей команды: frama-c -wp -wp-rte -wp-prover coq avg.c, я получаю: [wp] user error: Builtin \NearestEven not defined. Ни один из других режимов округления не был доступен.

Любые предложения?

Answer 1

В руководстве вы указываете, что поддерживается ядром Frama-C. Это не означает, что все плагины (или даже любой плагин) знают, как справиться с такой конструкцией. В вашем конкретном случае WP действительно не поддерживает \NearestEven.

С -wp-model +float, вы можете быть в состоянии работать на цели, такие как \result == (double)((x+y)/2), который будет очень вероятно, использовать ближайший даже для закругления, участвующих броском в double (но я должен признать, что пункт на Float арифметической модели в WP's manual немного кратким). Конечно, это не сработает, если вы хотите использовать другой режим округления, для которого, я думаю, что-то может сделать только плагин Jessie, если есть версия, совместимая с Aluminium.

Обратите внимание, что для обработки таких доказательств вам необходимо обратиться к Gappa и/или Coq. Повествователь, используемый в WP по умолчанию (Alt-Ergo), вряд ли выполнит много доказательных обязательств, связанных с вычислениями с плавающей запятой.