在Frama C上使用Alt-ergo验证WP时超时

Question

我正在尝试使用frama-C验证以下程序的正确性。我是frama-C的新用户。

问题：

录入员工的基本工资，并按如下方式计算员工的毛薪：

基本工资<= 10000 : HRA = 20%，DA = 80%

基本工资<= 20000 : HRA = 25%，DA = 90%

基本工资> 20000 : HRA = 30%，DA = 95%

#include <limits.h>

 /*@requires sal >= 0 && sal <= INT_MAX/2;
   ensures \result > sal && \result <= INT_MAX[enter image description here][1];

   behavior sal1:
   assumes sal <= 10000;
   ensures \result == sal+(sal*0.2*0.8);
   behavior sal2:
   assumes sal <= 20000;
   ensures \result == sal+(sal*0.25*0.9);
   behavior sal3:
   assumes sal >20000;
   ensures \result == sal+(sal*0.3*0.95);
   complete behaviors sal1,sal2,sal3;
  */


double salary(double sal){
    if(sal<=10000){return (sal+(sal*0.2*0.8));}
    else if(sal<=20000){return (sal+(sal*0.25*0.9));}
    else{return (sal+(sal*0.3*0.95));}
}

我在这里犯了什么错误？前提条件应该更精确些。

控制台消息：

[wp] [Alt-Ergo 2.3.3] Goal typed_salary_ensures : Timeout (Qed:57ms) (10s) 
(cached)
[wp] [Alt-Ergo 2.3.3] Goal typed_salary_assert_rte_is_nan_or_infinite_3 : 
Timeout (Qed:20ms) (10s) (cached)
[wp] [Alt-Ergo 2.3.3] Goal typed_salary_assert_rte_is_nan_or_infinite_6 : 
Timeout (Qed:2ms) (10s) (cached)
[wp] [Alt-Ergo 2.3.3] Goal typed_salary_assert_rte_is_nan_or_infinite_5 : 
Timeout (Qed:2ms) (10s) (cached)
[wp] [Alt-Ergo 2.3.3] Goal typed_salary_assert_rte_is_nan_or_infinite_4 : 
Timeout (Qed:17ms) (10s) (cached)
[wp] [Alt-Ergo 2.3.3] Goal typed_salary_assert_rte_is_nan_or_infinite_7 : 
Timeout (Qed:15ms) (10s) (cached)
[wp] [Alt-Ergo 2.3.3] Goal typed_salary_sal1_ensures : Timeout (Qed:33ms) 
(10s) (cached)
 [wp] [Alt-Ergo 2.3.3] Goal typed_salary_assert_rte_is_nan_or_infinite_9 : 
 Timeout (Qed:2ms) (10s) (cached)
 [wp] [Alt-Ergo 2.3.3] Goal typed_salary_assert_rte_is_nan_or_infinite_8 : 
 Timeout (Qed:4ms) (10s) (cached)
 [wp] [Alt-Ergo 2.3.3] Goal typed_salary_sal2_ensures : Timeout (Qed:42ms) 
 (10s) (cached)
 [wp] [Alt-Ergo 2.3.3] Goal typed_salary_sal3_ensures : Timeout (Qed:35ms) 
 (10s) (cached)

Answer 1

当面对浮点计算时，自动定理证明器通常表现得很差(例如，参见this report)。如果你真的真的需要它们，你可能想安装Gappa，它是专门为此而设计的，或者希望使用CVC4，Z3和Alt-Ergo (而不仅仅是Alt-Ergo)将允许你至少有一个证明者能够履行每个证明义务。但我建议坚持整数运算，例如，使用美分作为单位，以便在计算百分比时只处理整数(编辑:由于您的乘积百分比，这将意味着使用1/10000单位，但这仍然不是问题)。事实上，如果您坚持使用双精度，则要求值小于INT_MAX没有多大意义。

同样，如果您使用整数类型，可能更容易使用unsigned，它将自动满足拥有非负工资的要求。

最后，您的规范是模棱两可的:对于任何低于10000的薪水，您有两个不同的公式来计算结果。behavior sal2的assumes子句可能应该是：assumes 10000 < sal <= 20000;