时间戳

首页 > 解决方案 > 在 Frama C 上使用 Alt-ergo 证明 WP 时超时

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

问题描述

我试图使用 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)

标签： frama-cpreconditionsalt-ergo

解决方案

当面对浮点计算时，自动定理证明器的表现通常很差（例如，参见本报告）。如果您真的非常需要它们，您可能需要安装专门用于此目的的Gappa，或者希望使用 CVC4、Z3 和 Alt-Ergo（而不仅仅是 Alt-Ergo）可以让您至少拥有一个证明者能够履行每一项证明义务。但我建议坚持整数算术，例如使用美分作为单位，以便在计算百分比时只操作整数（编辑：因为你乘以百分比，这意味着使用 1/10000 单位，但它仍然不应该是个问题）。实际上，如果您坚持使用双精度数，那么要求具有小于的值INT_MAX并没有多大意义。

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

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

推荐阅读