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

如何解决在Frama C上使用Alt-ergo证明WP时超时

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

问题：

输入员工的基本工资并根据以下内容计算其总工资：

基本工资

基本工资> 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)

解决方法

当遇到浮点计算时，自动定理证明者通常表现得很差（请参见this report）。如果您确实非常需要它们，则可以安装专门为此目的的Gappa，或者希望使用CVC4，Z3和Alt-Ergo（而不是仅使用Alt-Ergo）可以使您拥有至少一名能够履行每项举证责任的证明人。但是我建议坚持整数运算，例如通过使用分作为单位，以便仅在计算百分比时操作整数（编辑：由于您要乘以百分比，这意味着使用1/10000单位，但这仍然不是问题）。实际上，如果您坚持要加倍，则要求值小于INT_MAX并没有多大意义。

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

最后，您的说明不明确：对于少于10000的薪水，您有两个不同的公式来计算结果。行为assumes的{{1}}子句可能应显示为：sal2