Discussion :

[boozook]

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!

[gangsoleil]

Bonjour,

Je ne connais pas frama-c ni jessie, or je pense que ton probleme est plus lie a ca qu'au langage C.

Neanmoins, quelques remarques :
En C, les indices de tableau commencent a 0, pas a un, d'ou un soucis dans ta boucle for.
Tu ne verifies pas que a n'est pas NULL. Or c'est la premiere chose a faire.

Dans le commentaire-specifique, tu as des choses etranges :

/*@
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;
*/

Tu dis que i doit etre inferieur ou egal a n. OK
Tu dis que k doit etre compris entre 1 et i-1 (k<i). Donc pour tout k compris entre 1 et n-1. Si c'est bien ce que tu veux, c'est mal ecrit : pour gagner en lisibilite, tu devrais essayer de toujours avoir des inferieurs strict ou des inferieur ou egal, mais pas les deux
Ensuite, tu enonces des conditions : A && B && C
A : rien de special
B : composee de X || Y || Z : si ton verificateur ne fait pas d'evaluation paresseuse, c'est a dire qu'il ne s'arrete pas des que la premiere condition est verifiee, alors tu as un soucis dans le cas ou imin2 vaut -1 :
imin2 == -1 : VRAI
a[k] == a[imin1] : on s'en fout
a[k] >= a[imin2] : tu accedes a a[-1], ce qui est clairement une erreur.
D'ailleurs, si imin2 vaut 0, tu as aussi un probleme : tu manipules a pour des indices allant de 1 a N-1 (ce qui est probablement une erreur vu que les tableaux en C vont de 0 a N-1), et tu as une condition sur a[0]

Bref, pas mal de legers problemes, mais a confirmer car je ne connais pas frama-c ou jessie.

[boozook]

Salut, merci de ta réponse.

Par rapport à ta première remarque concernant le code, en fait le code est donné et on ne doit pas le modifier, nous ce qu'on doit faire c'est mettre en commentaire les annotations ACSL uniquement. Et la boucle for commence à 1 parce que imin1 est déjà initialisé à 0 (en fait on force le premier tour de boucle en disant que le minimum du tableau c'est la première case au premier tour).

Après pour l'évaulation paresseuse, c'est pour ça que j'ai mis le imin2 == -1 en premier mais ça ne change rien au final donc bon ...

[boozook]

Peut-être que ce sujet aurait sa place dans une autre section ?

[ManusDei]

Il n'y a pas vraiment de forum pour la preuve de programme (enfin pas que je sache).

Comme précondition, n > 2 ?
Tu peux aussi vérifier en précondition que a est différent de NULL, comme le propose gangsoleil (donc sans modifier le code).

A ce que je pense en comprendre, l'erreur est peut-être plutôt dans la syntaxe.
Tu as essayé de noter ton invariant sur papier pour voir ? Tu peux séparer ton invariant en plusieurs cas, pour détecter plus facilement d'où vient le problème ?

Si non, met juste

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
\forall integer k; 
 (1 <= k < i) ==>
 (a[k] >= a[imin1])

en invariant, si ça plante pas rajoute le bout suivant, etc....

[Taurre]

Salut,

Tu ne verifies pas que a n'est pas NULL. Or c'est la premiere chose a faire.

Sans vouloir dire, cela me semble plutôt inutile. Recevoir un pointeur nul n'est qu'un cas parmis une multitude de valeurs invalides possible. Je pourrais tout aussi bien provoquer une erreur avec l'appel suivant : min2_array((int *)1, 10). C'est à l'utilisateur de la fonction de faire attention à la validité des valeurs qu'il envoie à cette dernière, pas l'inverse.

[gangsoleil]

Sans vouloir dire, cela me semble plutôt inutile [de tester un pointeur a NULL]. Recevoir un pointeur nul n'est qu'un cas parmis une multitude de valeurs invalides possible. Je pourrais tout aussi bien provoquer une erreur avec l'appel suivant : min2_array((int *)1, 10). C'est à l'utilisateur de la fonction de faire attention à la validité des valeurs qu'il envoie à cette dernière, pas l'inverse.

Tu peux faire confiance a l'utilisateur. Mais tu verras vite que la programmation defensive passe avant tout par la protection des valeurs que tu peux tester : Oui, NULL n'est qu'une valeur invalide parmi tant d'autres. Mais c'est celle que tu peux tester, alors pourquoi ne pas en profiter ?

Acceder a a[i], si a est NULL, va planter.Et comme le code est le suivant :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
9
10
int min2_array(int * a, int n) {
 
  int imin1 = 0; 
  int imin2 = -1;
 
  int i;
  for(i = 1; i < n; i++) 
  {
    if (a[i] < a[imin1]) 
...

le simpe fait de tester a a NULL te permet d'eviter l'erreur.

[Taurre]

Oui, NULL n'est qu'une valeur invalide parmi tant d'autres. Mais c'est celle que tu peux tester, alors pourquoi ne pas en profiter ?

Parce que, à mon sens, cela n'a pas beaucoup d'intérêt. À supposer que l'utilisateur manipule un pointeur nul, il finira tôt ou tard par effectuer une indirection et à provoquer l'arrêt du programme. Alors oui, cela aura lieu dans une autre fonction, mais cela se produira tout de même.

Au final, le test ne servira qu'avant une interruption et constituera donc plus une perte de temps qu'autre chose. Maintenant, chacun son opinion, mais personnellement je trouve la vérification superflue.

[gangsoleil]

À supposer que l'utilisateur manipule un pointeur nul, il finira tôt ou tard par effectuer une indirection et à provoquer l'arrêt du programme.

Sans verification, le programme plante lamentablement.
Avec verification, la fonction produit une erreur, et le programme ne plante pas.

Je prefere clairement la seconde.

[Taurre]

Sans verification, le programme plante lamentablement.

Nous sommes bien d'accord sur ce point.
Nous divergeons juste d'opinion sur qui doit effectuer cette vérification. Pour moi, cette dernière incombe à l'utilisateur de la fonction et non à la fonction elle-même.

[gangsoleil]

Nous sommes bien d'accord sur ce point.
Nous divergeons juste d'opinion sur qui doit effectuer cette vérification. Pour moi, cette dernière incombe à l'utilisateur de la fonction et non à la fonction elle-même.

L'habitude de la programmation defensive : je teste tout, partout, tout le temps.

La meilleure defense, c'est l'attaque.