Conception Formelle |
Récupérer l’archive suivante et décompressez-la.
Le prédicat \valid(a) indique que la zone mémoire est correctement allouée, et \valid_read(a) que l’on peut y lire, mais pas nécessairement y écrire. La distinction permet de désigner des pointeurs const, qui sont typiquement \valid_read, mais pas \valid.
À chaque fois qu’on manipule des pointeurs, RTE vous demandera de prouver que ceux-ci sont bien alloués si l’on souhaite y lire ou écrire. En pratique, on les utilisera toujours comme précondition, la fonction malloc n’étant pas commode à manipuler et spécifier avec Frama-C.
Dans un contrat de fonction, si on veut faire référence explicitement à une valeur avant de l’appel de la fonction, on doit la mettre dans la fonction \old(...). Par défaut, c’est ce qui est fait sur les arguments passés par valeurs (puisqu’ils ne peuvent pas être modifiés par la fonction), mais pour les valeurs pointées, ce n’est pas le cas, puisqu’elles peuvent subir des effets de bord. Par défaut, leur valeur est évaluée après l’appel dans une post-condition.
Exemple: /*@ ensures \old(a[0]) == a[0];*/
Vous noterez d’ailleurs que Frama-C place des \old autour des arguments de la fonction dans ce qu’il vous affiche : comme c’est la seule interprétation possible pour eux, les \old sont implicites.
Le mot clé \separated permet d’assurer que deux pointeurs ne pointent pas vers la même zone mémoire (ce qui est a priori possible). Il est également possible d’assurer que plusieurs adresses sont disjointes deux à deux grâce au même mot clé.
Exemple: /*@ \separated(a,b+(0 .. n));*/.
La clause assigns permet d’indiquer quelles valeurs la fonction peut être amenée à modifier lors de son exécution. Si elle ne modifie rien, on peut écrire assigns \nothing. Attention, WP réussira à prouver tout sur-ensemble des valeurs que la fonction modifie vraiment. Ainsi, une fonction ne modifiant que la valeur *a aura les clauses assigns *a,*b; et assigns *a; prouvées par WP, mais pas la clause assigns *b;.
Si besoin, pour augmenter la lisibilité de vos spécification, utilisez des comportements et des prédicats.
This document was translated from LATEX by HEVEA.