Frama-c Aluminum-20160501是否提供「\ NearestEven」？

Question

ACSL implementation（Aluminum-20160501版本1.11實施）列出了\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舍入工作（但我不得不承認，浮法算法模型中段落WP's manual有點簡潔）。如果你想使用另一個四捨五入模式，我認爲只有Jes​​sie插件，如果在某個地方有與鋁兼容的版本，那麼這當然是行不通的。

請注意，要處理此類證明，您需要求助於Gappa和/或Coq。 WP中默認使用的證明者（Alt-Ergo）不太可能履行與浮點計算相關的許多證明義務。