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

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

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;
}