问题描述
我正在尝试使用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