Функция заказа Frama-C

Question

Я пытаюсь доказать правильность своей функции сортировки 'order' с Frama-C на языке ACSL. У меня есть дополнительная функция 'swap' для перестановки двух значений моего массива 't'.

РЕДАКТИРОВАТЬ: Я обновил свой код.

/*@ 
    requires \valid (t+ (0..(l-1)));
    requires l > 0;
    requires i<l && j<l && i>=0 && j>=0;
    assigns t[i], t[j];
    ensures t[j] == \old(t[i]);
    ensures t[i] == \old(t[j]);
*/
void swap(int *t, int l, int i,int j){
  int tmp;
  tmp = t[i];
  t[i] = t[j];
  t[j] = tmp;
  return;
}

/*@ 
    requires \valid (t+ (0..(l-1)));
    requires l > 0;
    ensures \forall integer k; (0 <= k < l-1) ==> t[k] <= t[k+1]; 
*/
void order(int *t, int l) {
  int i;
  int j;
/*@
    loop assigns i, t[0 .. l-1];
    loop invariant 0<=i<l && i>=0;
    loop invariant \forall integer k; (0 <= k<=i) ==> t[k] <= t[k+1]; 
    loop variant l-i;


*/
  for (i=0;i<l;i++) {

/*@
    loop assigns j, t[0 .. l-1];
    loop invariant i<=j<l && i>=0 && j>=0;
    loop invariant  \forall  integer k; (0 <= k <= j)  ==> (t[k] <=  t[k+1]);
    loop variant l-j;

*/
    for (j=i; j<l; j++) {

      if (t[i] > t[j]){
    /*@ assert t[i] > t[j] && i<l && j<l && i>=0 && j>=0 ; */
    swap(t, l, i, j);
    /*@ assert t[i] < t[j] && i<l && j<l && i>=0 && j>=0 ; */
      }
    }
  }
}

Спасибо за вашу помощь!

Answer 1

Как всегда при использовании WP, важно, чтобы все функции, вызываемые проверяемой функцией, были снабжены контрактом с предложениями assigns. Кроме того, все циклы указанной функции при проверке должны иметь предложение loop assigns. Если это не так, WP придет к выводу, что любая часть состояния памяти может быть изменена вызовом (или, соответственно, циклом), так что он не сможет сказать что-либо значимое после соответствующей инструкции.

Таким образом, как минимум, вы должны добавить / заменить существующее предложение на:

• в договоре swap, пункт assigns t[i], t[j];
• в аннотации цикла внешнего цикла, пункт loop assigns i, t[0 .. l-1];
• в аннотации цикла внутреннего цикла, пункт loop assigns j, t[i .. l-1];

Как примечание относительно loop assigns:

• они должны описывать все потенциальные модификации от первого входа в цикл до текущего шага (следовательно, t[i], t[j] недостаточно, поскольку, возможно, произошли другие перестановки до текущего j).
• индекс цикла (здесь i и j) должен быть частью присваивания цикла, хотя его очень легко пропустить и удивляться, почему WP не устраивает.

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