Проблема проверки с использованием плагина Jessie и Frama-C

Question

Я новичок в Frama-C и хочу правильно изучить синтаксис ACSL. У меня есть этот фиктивный пример, и плагин Jessie не может проверить строки № 9 и 12. Я что-то упустил? Проверяемая (равная) функция проверит, имеют ли два массива (a и b) одинаковые значения или нет для каждого индекса:

/*@
     requires \valid_range(a,0,n-1);
     requires \valid_range(b,0,n-1);
     requires n >= 0;
     requires i >= 0 && i <= n;
     assigns i;
     behavior all_equal:
         assumes i == n;
         ensures \result == 1;
     behavior some_not_equal:
        assumes i != n;
        ensures \result == 0;
*/
int equal(int a[], int n, int b[], int i) {
  /*@ 
    loop invariant 0 <= i <= n;
    loop assigns i;
    loop variant n-i;
  */  
  for (i = 0; i < n; i++) {
    if (a[i] != b[i])
      return 0;
  }
  return 1;
}

Answer 1

Здесь есть пара неправильных вещей:

behavior all_equal:
     assumes i == n;
     ensures \result == 1;
 behavior some_not_equal:
    assumes i != n;
    ensures \result == 0;

в assumes предложение, все переменные оцениваются в предварительном состоянии функции. Это означает, что если у вас есть два одинаковых массива размера nи предполагая i является 0 (чего не могло быть, см. следующее объяснение), i == n всегда будет терпеть неудачу за исключением случаев, когда массив имеет размер 0

Другое дело: вы, кажется, используете i в качестве переменной для управления циклом, устанавливая его в 0 в начале цикла, однако в ваших аннотациях вы говорите, что iв предварительном состоянии программы, между 0 а также n, Это в сочетании с тем, что я сказал ранее, является одной из причин, почему Джесси не может доказать это.

Наконец, основная причина, по которой вы не можете доказать это, заключается в том, что вы пропустили существенный инвариант цикла, который гарантирует, что оба массива для всех индексов массива, предшествующих текущей итерации, равны:

loop invariant loop invariant \forall integer k; 0 <= k < i ==> a[k] == b[k];

С этим инвариантом вы можете теперь лучше определять свое поведение. Правильное решение вашей проблемы:

/*@
     requires \valid_range(a,0,n-1);
     requires \valid_range(b,0,n-1);
     requires n >= 0;
     behavior all_equal:
         assumes \forall integer k; 0 <= k < n ==> a[k] == b[k];
         ensures \result == 1;
     behavior some_not_equal:
        assumes \exists integer k; 0 <= k < n  && a[k] != b[k];
        ensures \result == 0;
*/
int equal(int a[], int n, int b[]) {
  int i = 0;
  /*@ 
    loop invariant 0 <= i <= n;
    loop invariant \forall integer k; 0 <= k < i ==> a[k] == b[k];
    loop assigns i;
    loop variant n-i;
  */  
  for (i = 0; i < n; i++) {
    if (a[i] != b[i])
      return 0;
  }
  return 1;
}