Conception Formelle |
Récupérer l’archive suivante et décompressez-la.
WP ne peut pas dérouler des boucles tout seul. Pour être capable de prouver des propriétés vérifiées par les boucles, on a besoin de la notion d’invariant de boucle. Un invariant de boucle est une propriété préservée par une application de la boucle, c’est-à-dire que si la propriété est vraie au début de la boucle, elle sera vraie à la sortie de la boucle. Il est possible de mettre plusieurs invariants de boucle (qui seront alors considérés comme devant tous être vrais (cf cours). La différence est que les preuves seront faites séparément et cela peut donc simplifier la tâche aux solveurs).
Exemple: /*@ loop invariant 0 <= i <n;*/
De même que pour les fonctions, Frama-C suppose qu’une boucle peut faire n’importe quel effet de bord sur la mémoire. Tout comme les fonctions, il est donc possible de déclarer (et prouver) des clauses assigns pour les boucles.
Exemple: /*@ loop assigns i,n,max;*/
Lorsque les fonctions où se trouvent une boucles disposent d’un contrat avec des comportements, il est possible d’utiliser ces comportements dans les contrats de boucles pour en simplifier l’expression. De même que pour les contrats de fonctions, il est toujours possibles de les exprimer sans comportement. Il faut toujours écrire les clauses globales avant celles concernant des comportements.
Exemple: /*@ for id: loop invariant i <= n; loop invariant j <= i; */, où id est le nom d’un comportement.
Note : il est tout à fait possible d’obtenir un contrat de boucle valide en utilisant uniquement des implications. C’est d’ailleurs peut-être mieux : dans certaines fonctions, les solveurs n’arrivent pas à démontrer les versions avec behavior dans les boucles, mais y arrivent avec des implications. Ça doit venir de l’implémentation de tout ça, mais je ne suis pas certain du problème exact.
Dans certains contrats de fonction ou de boucles, on peut avoir besoin de parler d’un grand nombre de valeurs, ou de l’existence d’une valeur qu’on ne connaît pas exactement (par exemple, pour des propriétés parlant de tableaux, mais pas seulement). En ACSL, cela peut être exprimé à l’aide des constructions \forall and \exists. La syntaxe est \forall type name; expr;, où type est un type C ou mathématique (integer ou real, par exemple), name le nom de la variable que l’on quantifie et expr une expression ACSL (faisant intervenir name, sinon ce n’est pas très utile).
Exemple: \forall int i; (0 <= i < n ==> \exists int j; 0 <= j < i && tab[j] < tab[i]);
Attention, vous pourriez être tenté d’écrire un loop assigns de la forme loop assigns tab[i]. Cela n’est pas possible. En effet, le loop assigns dit que «pour toute valeur en mémoire non listée, elle est égale à la valeur qu’elle avait avant l’entrée dans la boucle avant et après le tour courant» (dit autrement, c’est un invariant de boucle un peu particulier). Or, si au tour i, on considère tab[i], tous les tab[j] pour j<i ont été modifiés et ne sont plus égaux à la valeur qu’ils avaient avant le premier tour de boucle. Une autre manière de le voir est que ce contrat doit être utilisable par WP en abstrayant le contenu de la boucle (en regardant juste son contrat). Et la seule information pertinente dans ce cas seront quelles valeurs ont été modifiées à un tour de boucles quelconque, pas à quel tour de boucle elles l’ont été.
Pour la deuxième fonction vous pourriez (pour ne pas dire allez) avoir besoin de parler de la valeur d’une case mémoire lors du contexte d’appel de la fonction. Pour cela, vous ne pouvez pas utiliser \old(x), mais vous pouvez utiliser \at(x,Pre) qui a le même effet.
Puisqu’on manipule des tableaux, on pourrait vouloir considérer que la taille d’un tableau est un entier non-signé.
En C, sur les entiers non-signés, le comportement d’un overflow est bien défini (contrairement à l’overflow sur les entiers signés). Aussi, par défaut, RTE ne prévient pas des possibles overflow. WP en tient cependant compte, comme vous avez pu le constater.
Il est possible de forcer RTE à générer des assertions pour les overflows d’entiers non-signés avec l’option -warn-unsigned-overflow.
Le but de cet exercice est d’utiliser tout ce que nous avons vus jusqu’ici pour concevoir une spécification formelle de la fonction memcpy, puis un code sûr l’implémentant.
This document was translated from LATEX by HEVEA.