Conception Formelle
2021-2022
TP5: Fonctions logiques et prédicats : formalisation plus poussée.

Vincent Penelle

Points abordés



Récupérer l’archive suivante et décompressez-la.

Exercice 1: Fonctions logiques : mise en jambes
Point Technique:

Il est possible de définir en ACSL des fonctions mathématiques. On peut le faire soit par une expression directe, soit via un ensemble d’axiomes permettant de la définir récursivement. Cette dernière version sera faite via un bloc dit "axiomatic" (on verra cela dans un exercice ultérieur).

Voir code exemple de l’exercice courant.

Le premier intérêt de faire cela est, comme pour les prédicats, de n’écrire qu’une seule fois la définition de la fonction et d’utiliser ensuite le nom de la fonction (rendant ainsi la spécification plus lisible).

Le fichier exo1.c contient des codes dont les contrats de fonctions vous sont fournis. Il vous «reste» à compléter les invariants (et variants) de boucle et les définitions des fonctions utilisées. Un des deux ensures de doublePointer est volontairement fausse (cf. deuxième point technique), donc il est normal qu’il ne soit pas prouvé, et il ne vous est pas demandé de le corriger.

  1. Observez la définitions de nextInt, et observez que la fonction correspondante est prouvée.
  2. Écrivez des définitions pour les fonctions sumOfInt et sumFirstLast, et prouvez les contrats des fonctions sumInt et sumFL. N’oubliez pas d’enlever l’espace devant le @ des spécifications des fonctions que vous voulez prouver après avoir écrit vos fonctions logiques (je les ai mis pour que frama-c accepte d’ouvrir le fichier, puisque les fonctions logiques ne sont pas définies).
  3. La spécification de sumFLBis n’est pas prouvée. C’est normal, puisque le tableau a été modifié après qu’on ait calculé la valeur. On ne demande pas de corriger le code, mais la spécification : il suffit de dire que la fonction sumFirstLast est évaluée au début du programme avec \old.
    Point Technique:

    Il est possible de demander l’évaluation d’une fonction en un point particulier du programme, en lui fournissant un label L. La fonction sera alors calculée en considérant que les valeurs pointées sont évaluées au label L. Les règles s’appliquant aux labels possibles sont les même que pour \at (i.e., pas de labels à l’intérieur de blocs, pas de labels après l’appel).

    Exemple: \result == sumFirstLast{Pre}(t,n); évaluera sumFirstLast en regardant les valeurs pointées par t avant l’appel de la fonction C, mais en évaluant n après l’appel de la fonction C (la fonction C où cette spécification est mise).

    Cette syntaxe n’est pas équivalente à \result == \old(sumFirstLast(t,n);) : le label ne concerne en effet que les valeurs pointées dans le corps du prédicat, pas dans ses arguments, contrairement au \old qui affectera tous les arguments. En l’espèce, si on remplace maintenant n par une valeur pointée *i, avec un old, *i serait évaluée avant l’appel de la fonction, alors qu’avec {Pre}, il le serait à la fin. Voir la spécification de doublePointer pour avoir un aperçu du phénomène (il est normal que seule l’une des deux post-condition soit vraie).

    \old(sumFirstLast(t,n)) est équivalent à sumFirstLast{Pre}(\old(t),\old(n)).

  4. Remplacez le \old par la syntaxe décrite ci-dessus, puisqu’en réalité c’est le comportement souhaité (certes, pour ce cas précis, puisque n est un argument de la fonction, ça ne change rien). Vous remarquerez que doublePointerBis est une meilleure spécification (mais le but de ces mauvais exemples est de vous faire jouer avec).


Exercice 2: Labels multiples et prédicats
Point Technique:

Tout comme pour les fonctions, il est possible d’appeler un prédicat sur un label du programme. On peut même définir les prédicats (et les fonctions aussi) pour qu’ils lisent des valeurs à différents labels, mais il faut pour cela l’indiquer dans la définition du prédicat.

Exemple: predicate toto{L,M}(int *i) = \at(*i,L) == \at(*i,M) sera vrai si et seulement si i pointe vers la même valeur aux labels L et M.

Attention, si vous définissez plusieurs labels dans un prédicat (ou fonction), toutes les valeurs pointées devront être dans un \at (sinon c’est ambigu), les arguments entiers étant déterminés à l’appel de la fonction, ce n’est pas la peine de les mettre dans des \at.

  1. Après avoir regardé les exemples de prédicats, définissez les deux prédicats unchangedTab et tabNextIntFixed et ajoutez les bons invariants de boucles pour prouver la spécification de la fonction addOneTab.


Exercice 3: Définitions axiomatiques
Point Technique:

Certaines fonctions ou prédicats ne sont pas aisément définissables par une expression logique ou arithmétique, mais sont plus faciles à définir de manière récursive. Par exemple, la somme des éléments d’un tableau ne peut pas être écrite via une seule expression, puisque cela dépend du nombre d’élements dans le tableau, mais est assez facile à définir si on définit la somme des éléments d’un tableau vide (0) et la somme des éléments d’un tableau de taille n est la somme des éléments du tableau de taille n-1 qui ne contient pas la dernière case, plus cette dernière case.

En Frama-C, on peut définir des fonctions et prédicats de cette manière grâce à des axiomatiques (et même autrement que récursivement) qui se définissent globalement avec les éléments suivants :

Il faut faire très attention avec les axiomatiques : comme Frama-C considère que ce qui y est écrit est vrai, il faut veiller à ne pas écrire d’axiomes contradictoires, et bien veiller à ce qu’ils ne permettent que de définir ce que vous cherchez à définir. En effet, si des axiomes sont contradictoires, alors Frama-C réussira à prouver des trucs faux, et donc n’importe quoi !

On donne des exemples dans le code de cet exercice.

Note, dans cet exercice, ne vous préoccupez pas des gardes RTE, elles ne sont pas évidentes à prouver, et ce n’est pas ce qui est important ici.

  1. Regardez et comprenez les définitions axiomatiques Fibo et FiboTab.
  2. Définissez les axiomatiques SumTab et CountTab (des indications vous sont données pour les axiomes), et déterminez et prouvez les bons invariants pour les fonctions faisant intervenir ces fonctions.
  3. Définissez un prédicat swapInArray. Je vous donne des indications, et vous encourage à le découper en sous prédicats. Ce prédicat peut être défini sans axiomatique. Vous pourriez avoir besoin du prédicat unchangedTab défini à l’exercice 1. Utilisez-le pour prouver la spécification de la fonction swapInArray.
  4. Définissez maintenant l’axiomatique Permutation (encore une fois, vous avez des indications). Observez que vous arrivez à prouver la spécification de threeSwap. Vous pourrez voir que vous n’arrivez pas à prouver ensures permutation{Pre,Post} (t,t,i,n) dans la fonction swapInArray. C’est parce que les prédicats définis de ce genre ne sont pas aisé à démontrer si on n’a pas des axiomes sur mesure, et en particulier dans une fonction qui modifie un tableau à plusieurs endroit du code, il est difficile de prouver un tel prédicat. Aussi, pour les preuves, il sera plus aisé de découper le code et d’utiliser swapInArray à chaque fois que c’est possible pour faciliter les preuves. D’une manière générale, il est plus facile de prouver de petites fonctions.


Exercice 4: Axiomatiques : de l’art de choisir la bonne

Attention : Pour cet exercice, Alt-ergo n’arrive pas à démontrer les propriétés demandées pour l’axiomatique BetterCountTab. Par contre Z3 y arrive, lui.

Pour définir une fonction, on a souvent plusieurs choix possible pour les définir, et toutes ces définitions ne permettent pas de démontrer toutes les propriétés qu’on voudrait. Cela n’est pas dû forcément à une mauvaise définition, mais plutôt à la difficulté de démontrer automatiquement des propriétés, notamment avec des axiomes un peu trop spécifiques. Le but de cet exercice est de remarquer ce fait.



This document was translated from LATEX by HEVEA.