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

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

0 голосов
/ 10 ноября 2018

Я пытаюсь доказать правильность своей функции сортировки '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 ; */
      }
    }
  }
}

enter image description here Спасибо за вашу помощь!

1 Ответ

0 голосов
/ 12 ноября 2018

Как всегда при использовании 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, вероятно, является единственной наиболее важной вещью, которую нужно иметь, прежде чем пытаться доказать более глубокие функциональные свойства.

Добро пожаловать на сайт PullRequest, где вы можете задавать вопросы и получать ответы от других членов сообщества.
...