Блог

Главная - Вопросы по программированию - Тайм-аут при проверке WP с использованием Alt-ergo на Frama C

Тайм-аут при проверке WP с использованием Alt-ergo на Frama C

#frama-c #preconditions #alt-ergo

#frama-c #предварительные условия #alt-ergo

Вопрос:

Я пытался проверить правильность приведенной ниже программы с помощью 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 amp;amp; sal <= INT_MAX/2;
   ensures result > sal amp;amp; 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)

Комментарии:

1. незначительный момент: вы, вероятно, захотите отредактировать свой код, чтобы удалить ложную [enter image description here][1] информацию в конце первого ensures .

Ответ №1:

Автоматические проверяющие теоремы обычно ведут себя довольно плохо, когда сталкиваются с вычислениями с плавающей запятой (см., Например, Этот отчет ). Если они вам действительно, действительно нужны, вы можете установить Gappa, который специализируется на этом, или надеяться, что использование CVC4, Z3 и Alt-Ergo (в отличие от просто Alt-Ergo) позволит вам иметь хотя бы одного проверяющего, способного выполнить каждое обязательство по проверке. Но я бы посоветовал придерживаться целочисленной арифметики, например, используя центы в качестве единицы измерения, чтобы манипулировать целыми числами только при вычислении процентов (РЕДАКТИРОВАТЬ: поскольку вы умножаете проценты, это будет означать работу с 1/10000 единиц, но это все равно не должно быть проблемой). На самом деле, если вы настаиваете на удвоении, требования иметь значения меньше INT_MAX , чем не имеет особого смысла.

В том же духе, если вы используете целочисленный тип, это, вероятно, проще сделать unsigned , что автоматически выполнит требование о неотрицательной зарплате.

Наконец, ваша спецификация неоднозначна: для любой зарплаты меньше 10000 у вас есть две разные формулы для вычисления результата. assumes предложение о поведении sal2 , вероятно, должно гласить: assumes 10000 < sal <= 20000;