Salut à tous,
je viens en demande d'aide ^^

J'ai un souçi pour la preuve du programme suivant avec frama-c et jessie.

Code : Sélectionner tout - Visualiser dans une fenêtre à part
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
int min2_array(int * a, int n) {

  int imin1 = 0; 
  int imin2 = -1;

  /*@
    loop invariant (i <= n) && 
(\forall integer k; 
   (1 <= k < i) ==>
        ((a[k] >= a[imin1])
     && ((imin2 == -1) || (a[k] == a[imin1]) || (a[k] >= a[imin2]))
     && ((imin2 == -1) || (a[imin2] >= a[imin1])) ));
    loop variant n-i-1;
  */

  int i;
  for(i = 1; i < n; i++) 
  {
    if (a[i] < a[imin1]) 
    {
      imin2 = imin1;
      imin1 = i;
    }
    else if ((a[imin1] < a[i]) && ((imin2 == -1) || (a[i] < a[imin2])))
      imin2 = i;
  }

  return imin2;
}
La spécification est simple : le programme renvoie la position du second minimum du tableau (par valeurs strictes entre le premier et le second).
Il renvoie "-1" si le minimum strict du tableau est à la première case (indice 0 donc).

Néanmoins: d'une part, l'invariant de boucle que j'ai mis fait des erreurs, et d'autre part je n'arrive pas à trouver de préconditions...

Donc voilà, j'espère que vous pourrez m'aider.

Merci à tous!