Validation formelle d'une fonction informatique

Bonjour,

À la lecture de ce long article et en particulier le chapitre Les boucles - Exemples, une question m’est venue : Comment prouvez que le résultat de la fonction search renvoie, si elle contient plusieurs fois l’élément recherché, le pointeur vers la première case trouvée ?

J’ai tenté différentes approches mais je ne suis malheureusement pas tout à fait à l’aise avec ces outils que j’espère sincèrement maitriser au plus vite

Merci d’avance pour le temps que vous accorderez à la lecture de ce message !

En théorie, il suffit d’exprimer dans la valeur retourné (ie le pointeur) est le plus petit parmi tous ceux dont le déférencement donne element.

Dans le comportement in, quelque chose comme ca

pour tout autre pointeur i2 compris arr et arr+length tel que *i2 == element, tu as \result <= i2

N’ayant pas fait de Frama-C depuis un bail, pas garanti que ca marche (même si ca devrait, la syntaxe exacte est à chercher). Il faudra peut être adapter l’invariant de boucle pour prouver ceci.

PS: le C garantit que l’adresse d’un élément est plus petite que celle d’un élément dont l’index est plus grand, j’espère que Frama-C le modélise (sinon voir réponse après, bien plus efficace).

Lu’!

Une version facile est aussi de dire que tous les éléments qui précèdent le résultat sont différents, donc c’est le premier.

Oui et c’est nécessaire pour exprimer la propriété en question avec le programme que j’ai donné dans le tutoriel. Par contre, il faut se montrer un peu fourbe pour lui faciliter le travail.

En rajoutant quelque chose du genre :

1

/*@ ensures \forall size_t off ; 0 <= off < \result => array[off] != element; */

Est-ce suffisant ?

Alors, ça a priori c’est correct (modulo la faute de frappe sur l’implication => –> ==>) si ton résultat est l’indice de l’élément dans le tableau. D’ailleurs, on peut constater qu’avec une telle version, cette post-condition est bien prouvée :

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30

/*@
  requires 0 < length;
  requires \valid_read(array + (0 .. length-1));

  assigns  \nothing;

  behavior in:
    assumes \exists size_t off ; 0 <= off < length && array[off] == element;
    ensures 0 <= \result < length && array[\result] == element;
    ensures \forall size_t off ; 0 <= off < \result ==> array[off] != element;

  behavior notin:
    assumes \forall size_t off ; 0 <= off < length ==> array[off] != element;
    ensures \result == length;

  disjoint behaviors;
  complete behaviors;
*/
size_t search_idx(int* array, size_t length, int element){
  /*@
    loop invariant 0 <= i <= length;
    loop invariant \forall size_t j; 0 <= j < i ==> array[j] != element;
    loop assigns i;
    loop variant length-i;
  */ 
  for(size_t i = 0; i < length; i++)
    if(array[i] == element)
      return i;
  return length;
}

Sauf que dans l’exemple du tutoriel, on renvoie un pointeur vers l’élément, donc il faut modifier un peu cette formule pour que ça marche. Cela dit, pour faciliter la vie de WP, c’est pas plus mal de rester sur une forme proche de ça. La question est alors : vu que je ne peux pas mettre \result pour ma borne supérieure, comment je peux calculer une bonne supérieure correcte pour off à partir de \result et de mes variables d’entrée ?