любой способ указать предварительные условия внутри цикла во frama C?

Я пытаюсь доказать приведенную ниже функцию, где элементы массива добавляются к целочисленному значению c. это в frama c, но я не могу доказать некоторые части. Может ли кто-нибудь помочь с этим?

#include <limits.h>

/*@requires n>0;
   requires \forall integer i;0<=i<n ==> INT_MIN<=a[i]+c<=INT_MAX;
   requires \valid(a+(0..n-1));
   ensures \forall integer i;0<=i<n ==> a[i] == \old(a[i]) +c;
   assigns a[0..n-1];
*/


  void array(int *a,int n,int c){

  /*@loop invariant 0<=p<=n;
     loop invariant \forall integer i;0<=i<p ==> a[i] == \at(a[i],LoopEntry) +c;
     loop assigns p,a[0..n-1];
     loop variant n-p;
   */
   for(int p=0;p<n;p++){
      a[p]=a[p]+c;
   }
}

Ниже приведены недоказанные цели: Я выделил недоказанные цели.

[kernel] Parsing q2.c (with preprocessing)
[wp] Running WP plugin...
[rte] annotating function array
[wp] 15 goals scheduled
[wp] [Qed] Goal typed_array_loop_invariant_established : Valid (8ms)
[wp] [Qed] Goal typed_array_loop_invariant_2_established : Valid (5ms)
---->[wp] [Alt-Ergo 2.3.3] Goal typed_array_loop_invariant_2_preserved : Timeout (Qed:43ms) (10s) (cached)<----
[wp] [Alt-Ergo 2.3.3] Goal typed_array_loop_invariant_preserved : Valid (Qed:40ms) (32ms) (12) (cached)
[wp] [Alt-Ergo 2.3.3] Goal typed_array_ensures : Valid (Qed:35ms) (50ms) (52) (cached)
---->[wp] [Alt-Ergo 2.3.3] Goal typed_array_assert_rte_signed_overflow_2 : Timeout (Qed:16ms) (10s) (cached)<-----
------>[wp] [Alt-Ergo 2.3.3] Goal typed_array_assert_rte_signed_overflow : Timeout (Qed:17ms) (10s) (cached)<-----
[wp] [Alt-Ergo 2.3.3] Goal typed_array_assert_rte_mem_access_2 : Valid (Qed:18ms) (45ms) (112) (cached)
[wp] [Alt-Ergo 2.3.3] Goal typed_array_assert_rte_mem_access : Valid (Qed:71ms) (44ms) (109) (cached)
[wp] [Qed] Goal typed_array_assigns : Valid (4ms)
[wp] [Qed] Goal typed_array_loop_assigns_part1 : Valid
[wp] [Qed] Goal typed_array_loop_variant_positive : Valid (13ms)
[wp] [Qed] Goal typed_array_loop_variant_decrease : Valid (15ms)
[wp] [Alt-Ergo 2.3.3] Goal typed_array_loop_assigns_part2 : Valid (Qed:27ms) (59ms) (139) (cached)
[wp] [Alt-Ergo 2.3.3] Goal typed_array_assert_rte_signed_overflow_3 : Valid (Qed:93ms) (37ms) (62) (cached)
[wp] [Cache] found:9
[wp] Proved goals:   12 / 15
  Qed:               6  (4ms-30ms-93ms)
   Alt-Ergo 2.3.3:    6  (32ms-59ms) (139) (interrupted: 3) (cached: 9)

loops loop-invariant frama-c
person Niresh    schedule 10.11.2020    source источник

Ответы (1)


arrow_upward
3
arrow_downward

Ты почти там. На самом деле ваши инварианты цикла не полны: вы указываете, что происходит с началом массива, но не то, что конец остается неизменным. Вообще говоря, любое место, упомянутое в loop assigns, должно появиться в loop invariant, иначе о нем ничего не известно после первого шага цикла (т.е. для доказательства сохранения или какой-либо аннотации к состоянию после цикла). Здесь местоположения a[p..n-1] имеют совершенно неизвестные значения, за исключением LoopEntry.

Добавление loop invariant \forall integer i; p<= i < n ==> a[i] == \at(a[i],LoopEntry); должно решить проблему.

NB: у вас может возникнуть соблазн более сильного loop assigns с использованием a[0..p-1], но опыт показывает, что WP не очень удобно присваивать циклы массивам, границы которых сами назначаются. Я бы предложил явно добавить инвариант, что конец массива неизменен.

person Virgile    schedule 10.11.2020