lemma-functions.tex

Les assertions nous permettent de donner des indices au générateur
d'obligation de preuves pour les solveurs SMT obtiennent assez d'information
pour produire la preuve dont nous avons besoin. Cependant, il est parfois
difficile d'écrire une assertion qui créera exactement la propriété dont le
solveur SMT a besoin pour déclencher le bon lemme (par exemple, puisque le
générateur effectue des optimisations sur les obligations de preuve, ils peuvent
légèrement la modifier, ainsi que le contexte de preuve). De plus, nous
reposons sur des lemmes qui ont souvent besoin d'être prouvés en Coq, et pour
cela nous avons besoin d'apprendre Coq.


Dans cette section, nous verrons quelques techniques qui peuvent être
utilisées pour rendre tout cela plus prédictible et nous éviter d'utiliser
l'assistant de preuve Coq. Tandis que ces techniques ne peuvent pas toujours
être utilisées (et nous expliquerons quand cela n'est pas applicable), elles
sont généralement efficaces pour obtenir de la preuve presque complètement
automatiques. Cela repose sur l'usage de code fantôme.


\levelThreeTitle{Preuve par induction}


Précédemment, nous avons mentionné que les solveurs SMT sont mauvais pour
effectuer des preuves par induction (la plupart du temps), et c'est la raison
pour laquelle nous avons souvent besoin d'exprimer des lemmes que nous prouvons
avec l'assistant de preuve Coq qui nous permet de faire notre preuve par
induction. Cependant, dans la section~\ref{l2:statements-loops} à propos des
boucles, nous trouvons une sous-section~\ref{l3:statements-loops-invariant}
nommée « Induction et invariant », où nous expliquons que pour prouver un
invariant de boucle, nous procédons ... par induction. L'auteur de ce tutoriel
aurait-il honteusement menti au lecteur pendant tout ce temps ?


En fait non, et la raison est plutôt simple. Lorsque nous prouvons un
invariant de boucle par induction en utilisant des solveurs SMT, ils n'ont pas
besoin d'effectuer le raisonnement par induction eux-mêmes. Le travail qui
consiste à séparer la preuve en deux sous-preuves, la première pour
l'établissement de l'invariant (le cas de base de la preuve), et la seconde pour
la préservation (le cas d'induction) est effectué par le générateur
d'obligations de preuve. Par conséquent, quand les obligations de preuves sont
transmises aux solveurs SMT, ce travail n'est plus nécessaire.


Comment pouvons-nous exploiter cette idée ? Nous avons expliqué précédemment
que le code fantôme peut être utilisé pour fournir plus d'information que ce qui
est explicitement fourni par le code source. Pour cela, nous ajoutons du code
fantôme (et possiblement des annotations à propos de ce code) qui nous permet
de déduire plus de propriétés. Illustrons cela avec un exemple simple. Dans
un exercice précédent (\ref{l4:acsl-properties-lemmas-lsorted-gsorted}), nous
voulions prouver l'appel de fonction suivant (nous avons exclus la
postcondition pour raccourcir l'exemple) :


\CodeBlockInput{c}{ghost-code-usage-1.c}


Pour cela, la solution que nous avions demandée dans l'exercice était de fournir
un lemme qui énonce qui si la plage est « triée localement », au sens où chaque
élément est supérieur ou égal à l'élément qui le précède, alors nous pouvons
dire qu'elle est « globalement triée », c'est-à-dire que pour chaque paire
d'indices $i$ et $j$, si $i \leq j$ alors le $j^{ième}$ élément du tableau est
supérieur ou égal au $i^{ième}$ élément. Donc, la précondition de la fonction
pouvait être prouvée par les solveurs SMT, mais pas le lemme lui-même qui
nécessite une preuve Coq. Est-ce que l'on ne pourrait pas faire quelque chose
de mieux à ce sujet ?


La réponse est oui. Avant d'appeler la fonction, nous pouvons construire une
preuve qui montre que puisque le tableau est trié localement, nous pouvons
déduire qu'il est trié globalement (ce qui est simplement la preuve du lemme
dont nous aurions besoin). Pour écrire cette preuve à la main, nous procéderions
par induction sur la taille de la plage. Nous avons deux cas. D'abord si la
plage est vide, la propriété est trivialement vraie. Ensuite, supposons qu'une
plage donnée de taille $i$ avec $i < length$ ($length$ étant la taille de la
plage complète) est globalement triée et montrons que si c'est le cas, alors la
plage de taille $i+1$ est triée. C'est facile parce que, d'après notre
précondition, nous savons que le $i^{ième}$ élément est supérieur ou égal au
$(i-1)^{ième}$ élément, qui est lui même plus grand que tous les éléments qui
précède.


Comment pouvons-nous traduire cela en code fantôme ? Nous écrivons une boucle qui
vas de $0$ (notre cas de base), à la fin \CodeInline{len} et nous fournissons
un invariant montrant que le tableau est globalement trié depuis $0$ jusqu'à la
cellule actuellement visitée. Nous ajoutons également une assertion pour aider le
prouveur (qui nous dit que l'élément courant est plus grand que les éléments qui
précèdent) :



\CodeBlockInput[15][31]{c}{ghost-code-usage-2.c}



Nous pouvons voir que toutes les obligations de preuve sont facilement
vérifiées par les solveurs SMT, sans que cela ne nécessite d'écrire une preuve Coq
ou un lemme. Les obligations de preuve respectivement créées pour
l'établissement et la préservation de l'invariant correspondent aux deux cas que
nous avions besoin dans notre preuve par induction :


\image{ghost-code-base}


\image{ghost-code-ind}


Ce type de code est appelé un « \textit{proof carrying code} » : nous avons écrit
un code et les annotations qui amènent la preuve d'une propriété que nous voulons
vérifier.


Notons qu'ici, puisque nous devons écrire beaucoup de code fantôme, cela augmente
notre risque d'introduction d'une erreur qui changerait les propriétés du code
vérifié. Nous devons donc impérativement nous assurer que le code fantôme que
nous avons écrit termine et qu'il ne contient pas d'erreurs à l'exécution
(grâce au plugin RTE) pour avoir confiance dans notre vérification.


Dans cet exemple, nous avons directement écrit le code fantôme comme annotation du
programme, cela signifie que si nous avons un autre appel comme celui-ci quelque
part dans le code avec une précondition similaire, nous aurions à le faire à
nouveau. Rendons cela plus simple et modulaire avec des « fonctions lemmes »
(\textit{lemma functions}).



\levelThreeTitle{fonction lemme}


Le principe des « fonctions lemmes » est le même que celui des lemmes : à
partir de certaines prémisses, nous voulons arriver à une conclusion particulière.
Et une fois que c'est fait, nous voulons les utiliser à d'autres endroits pour
directement déduire la conclusion depuis les prémisses sans avoir à faire la
preuve à nouveau, en instanciant les valeurs nécessaires.


La manière de faire cela est d'utiliser une fonction, en utilisant les clauses
\CodeInline{requires} pour exprimer les prémisses du lemme, et les clauses
\CodeInline{ensures} pour exprimer la conclusion du lemme. Les variables
quantifiées universellement peuvent rester quantifiées ou correspondre à un
paramètre de la fonction. Plus précisément, si une variable est uniquement liée
aux prémisses ou uniquement aux conclusions, elle peut rester une variable
quantifiée, à supposer qu'il ne soit pas nécessaire de la lier à une variable
du code de preuve (puisque qu'une variable quantifiée n'est pas visible depuis
le code C). Si elle est liée aux prémisses et conclusions, elle doit être un
paramètre de la fonction (puisqu'ACSL ne nous permet pas de quantifier une
variable pour un contrat de fonction entier).


Considérons l'exemple suivant où nous n'utilisons pas (directement) de
variable universellement quantifiée dans le contrat, avec notre précédent
exemple à propos des valeurs triées. Depuis la propriété
\CodeInline{element\_level\_sorted(arr, len)}, nous voulons déduire
\CodeInline{sorted(arr, len)}. Le lemme correspondant pourrait être :


\begin{CodeBlock}{c}
/*@
  lemma element_level_sorted_is_sorted:
    \forall int* arr, integer len ;
       element_level_sorted(arr, len) ==> sorted(arr, len) ;
*/
\end{CodeBlock}


Écrivons donc une fonction qui prend deux paramètres, \CodeInline{arr} et
\CodeInline{len}, et requiert que le tableau soit trié localement et assure
qu'il est trié globalement :


\CodeBlockInput[15][22]{c}{lemma-function-1-1.c}


Notons que cette fonction doit affecter \CodeInline{\textbackslash{}nothing}.
En effet, nous l'utilisons pour déduire des propriétés à propos du programme, dans
du code fantôme, et donc elle ne devrait pas modifier le contenu du tableau, sinon
le code fantôme modifierait le comportement du programme. Maintenant, produisons un
corps pour cette fonction, le code qui nous amène la preuve que la conclusion est
bien vérifiée en supposant que la précondition est vérifiée. Cela correspond au
code que nous avons écrit précédemment pour prouver la précondition de l'appel de
la fonction \CodeInline{bsearch} :



\CodeBlockInput[15][32]{c}{lemma-function-1-2.c}


Avec cette boucle spécifiée, nous obtenons une preuve par induction que le lemme
est vrai. Maintenant, nous pouvons utiliser cette fonction lemme en
l'appelant tout simplement à l'endroit où nous avons besoin de faire cette
déduction :


\CodeBlockInput[34][40]{c}{lemma-function-1-2.c}


Ce qui nous demande d'établir la preuve que les prémisses sont établies grâce
à la précondition de la fonction lemme (et qui est trivialement vraie,
puisque nous l'obtenons de la précondition de \CodeInline{bsearch\_callee}), et
qui nous donne en retour la conclusion gratuitement puisque c'est la postcondition
de la fonction lemme (et nous pouvons utiliser cette propriété comme
précondition de l'appel à la fonction \CodeInline{bsearch}).


Comme nous l'avons expliqué, quand des variables universellement quantifiées
sont liés à la fois aux prémisses et aux conclusions, elles doivent être des
paramètres, c'est par exemple le cas ici pour les variables \CodeInline{arr}
et \CodeInline{len}, tandis que pour les variables quantifiées dans les
prédicats :



\CodeBlockInput[4][8]{c}{lemma-function-1-2.c}


puisqu'elles ne sont respectivement liées qu'aux prémisses et aux conclusions
restent universellement quantifiées (même si elles sont cachées dans les
prédicats). Nous pourrions avoir écris le contrat comme ceci :



\CodeBlockInput[15][32]{c}{lemma-function-1-3.c}


où nous voyons parfaitement que les variables sont toujours universellement
quantifiées. Cependant, nous ne sommes pas obligés de les maintenir quantifiées
universellement, et nous pourrions parfaitement les transformer en paramètres
(en supposant que la conclusion que nous obtenir des prémisses a toujours du
sens). Faisons par exemple cela pour les variables \CodeInline{i} et
\CodeInline{j} de la conclusion :


\CodeBlockInput[34][43]{c}{lemma-function-1-3.c}


Ce qui est tout à fait bon et nous pourrions par exemple utiliser cette fonction
pour déduire des propriétés à propos du contenu du tableau. Notons qu'ici, nous
utilisons un appel à la précédente fonction lemme pour rendre la preuve
plus facile. Nous pouvons même aller plus loin en transférant la « prémisse de
notre conclusion » en tant que prémisse d'un nouveau lemme :



\CodeBlockInput[45][55]{c}{lemma-function-1-3.c}


Tous ces lemmes énoncent la même relation globale, la différence est liée à la
quantité d'information requises pour les instancier (et par conséquent la
précision de la propriété que nous obtenons en retour).


Finalement, présentons un dernier usage des fonctions lemmes. Dans tous les
exemples précédent, nous avons considéré des variables universellement quantifiées.
En fait, ce que nous avons dit précédemment est aussi applicable aux variables
existentiellement quantifiées : si elles sont liées aux prémisses et aux
conclusions, elles doivent être des paramètres, sinon elles peuvent donner lieu
à des paramètres ou rester quantifiées. Cependant, à propos des variables
existentiellement quantifiées, nous pouvons parfois aller plus loin en construisant
une fonction qui nous fournit directement une valeur qui satisfait la propriété
à propos de la variable existentiellement quantifiée.



Par exemple, considérons la définition axiomatique du comptage d'occurrences et
imaginons qu'à un certain point de notre programme, nous voulons prouver
l'assertion suivante à partir de la précondition :


\CodeBlockInput[24][32]{c}{lemma-function-2-1.c}


Bien sûr, il existe un indice \CodeInline{n} tel que \CodeInline{in[n]} est
\CodeInline{v}, sinon le nombre d'occurrences de cette valeur serait $0$.
Mais au lieu de prouver que cet index existe, montrons que nous pouvons trouver
un index qui respecte les contraintes à propos de \CodeInline{n} en utilisant
une fonction lemme qui le retourne :


\CodeBlockInput[24][44]{c}{lemma-function-2-2.c}


Si nous regardons seulement le corps de la fonction, il a deux comportements :
soit il existe une cellule du tableau qui contient \CodeInline{v} et la fonction
retourne son indice, ou ce n'est pas le cas, et dans ce cas la fonction retourne
-1. Le premier comportement est facile à montrer, le retour correspondant à cette
découverte n'est effectuée que dans une branche où l'on a trouvé une cellule qui
correspond à la valeur recherchée.


Nous prouvons que le second comportement respecte la postcondition en montrant
qu'il mène à une contradiction. S'il n'y a pas de cellule dont la valeur est
\CodeInline{v}, alors le nombre d'occurrences de \CodeInline{v} est 0. C'est
exprimé grâce au second invariant qui nous dit qu'aucun \CodeInline{v} n'a été
rencontré depuis le début de la boucle, et donc le nombre d'occurrences est 0.
Cependant, la précondition de la fonction nous énonce que le nombre d'occurrences
est supérieur à 0, ce qui mène à une contradiction que nous modélisons par une
assertion de faux (notons qu'elle n'est pas nécessaire, nous l'écrivons
explicitement pour notre explication) ce qui signifie que ce chemin est
infaisable.


Finalement, nous pouvons appeler cette fonction pour montrer qu'il existe un
indice qui nous permet de valider notre assertion :


\CodeBlockInput[46][55]{c}{lemma-function-2-2.c}


L'utilisation des fonctions lemmes nous permet de raisonner par
induction à propos de lemmes sans avoir besoin de preuve interactive. De plus,
le déclenchement des lemmes devient beaucoup plus prévisible puisque nous le
faisons à la main. Cependant, les lemmes nous permettent de travailler sur
plusieurs labels :



\begin{CodeBlock}{c}
/*@
  lemma my_lemma{L1, L2}:  P{L1} ==> P{L2} ;
*/
\end{CodeBlock}


Les fonctions lemmes ne nous fournissent pas de mécanisme équivalent
car elles sont simplement des fonctions C normales, qui ne peuvent pas prendre
de labels comme entrée. Regardons ce que nous pouvons faire à ce sujet.



\levelThreeTitle{Macro lemme}


Lorsque nous devons traiter de multiples labels, l'idée est « d'injecter »
directement le code de preuve à l'endroit où c'est nécessaire comme nous
l'avons fait au début de ce chapitre. En revanche, nous ne voulons pas écrire
ce code à la main chaque fois que nous en avons besoin, utilisons donc des
macros pour le faire.


Pour le moment, traduisons notre code précédent en une macro au lieu d'une
fonction. Comme nous utilisons la macro dans du code fantôme (donc en annotation),
nous devons faire attention à utiliser la syntaxe pour les annotations fantômes
lorsque nous écrivons l'invariant de notre boucle et les assertions :


\CodeBlockInput[16][33]{c}{lemma-macro-1.c}


Au lieu de fournir un pré et une postcondition, nous énonçons ces propriétés en
utilisant des assertions avant et après le code de preuve. Ce code de preuve est
simplement le même qu'avant, et est utilisé exactement comme il était utilisé dans
le cas de la fonction. Cependant, nous pouvons voir que cela fait une différence
importante une fois qu'il a été préprocessé par Frama-C, puisque le bloc de code
et les annotations sont directement injectées dans la fonction
\CodeInline{bsearch\_callee}.


\image{lemma-macro-1}


En fait, nous utilisons une macro pour générer le code que nous écrivions
précédemment. Dans le cas présent, ce n'est pas vraiment intéressant puisque
l'appel de fonction nous permettait d'avoir une preuve plus modulaire. Étudions
donc un exemple où nous n'avons pas d'autre choix qu'utiliser une macro.


Nous utiliserons le lemme suivant :


\CodeBlockInput[4][11]{c}{lemma-macro-2-1.c}


Avec pour objectif de prouver le programme suivante :


\CodeBlockInput[13][29]{c}{lemma-macro-2-1.c}


où le lemme \CodeInline{shift\_ptr} est nécessaire pour prouver que la
postcondition de \CodeInline{callee} depuis la postcondition de
\CodeInline{shift\_array}. Notre but est bien sûr de ne pas avoir besoin du
lemme en le remplaçant par une macro lemme.


Il n'y a pas de guide précis pour concevoir une macro utilisée pour injecter
un code de preuve. Cependant, la plupart des lemmes énoncés à propos de labels
multiples sont relativement similaires dans leur manière de lier les labels.
Illustrons donc avec cet exemple ; la plupart du temps concevoir une macro dans
une telle situation suivra plus ou moins ce schéma.


Pour construire la macro, nous avons besoin d'un contexte dans lequel travailler.
Nous construisons ce contexte en utilisant une fonction,
nommons-la \CodeInline{context\_to\_prove\_shift\_ptr}. L'idée est d'utiliser
cette fonction pour construire notre macro en isolation du reste du programme pour
rendre la vérification de la propriété plus facile. Cependant, tandis que les
fonctions lemmes sont ensuite appelées dans d'autres fonctions pour déduire
des propriétés, cette fonction ne sera jamais appelée, son rôle est juste de nous
permettre d'avoir un « endroit » où nous pouvons construire notre preuve. En
particulier, comme nous avons besoin de plusieurs labels mémoire, notre fonction
\textbf{a besoin} de modifier le contenu de la mémoire (sinon, nous aurions qu'un
seul état mémoire pour toute la fonction).


Illustrons cela avec notre problème actuel pour rendre tout cela plus clair.
Premièrement, nous créons la macro \CodeInline{shift\_array} qui contiendra notre
code de preuve, pour le moment indiquons juste que c'est une instruction vide.
Dans les paramètres de ce lemme, nous prenons les labels considérés. Notons que
les règles précédemment exprimées à propos des variables quantifiées s'appliquent
aussi pour les macros.


\begin{CodeBlock}{c}
#define shift_ptr(_L1, _L2, _arr, _fst, _last, _s1, _s2) ;
\end{CodeBlock}


Ensuite nous créons notre fonction de contexte :


\CodeBlockInput[22][41]{c}{lemma-macro-2-2.c}


Décomposons ce code, en commençant par la fonction de contexte. En entrée, nous
recevons les variables du lemme. Nous énonçons également quelques propriétés à
propos des bornes des entiers considérés, généralement cela devrait simplement
être les préconditions qui ne sont pas liées aux états mémoire, ou liées au
premier état mémoire. Ensuite, nous introduisons le label \CodeInline{L1} et nous
appelons la fonction \CodeInline{assign\_array} qui nous amène au label
\CodeInline{L2}. Le rôle de cet appel est de s'assurer que WP créera un nouvel
état mémoire (et qu'il ne considérera donc pas que la mémoire est la même), et
d'établir les prémisses. En effet, si nous regardons le contrat de
\CodeInline{assign\_array}, nous voyons qu'elle assigne le tableau (ce qui
garantit la création d'un nouvel état mémoire) et en postcondition, elle assure
que le contenu du tableau, entre la pré et la postcondition (donc, quand nous
l'appelons : \CodeInline{L1} et \CodeInline{L2}), respecte les prémisses de notre
lemme (que l'on répète en ligne 36, en ajoutant une assertion). Ensuite nous
utilisons notre macro \CodeInline{shift\_ptr} (qui contiendra par la suite notre
code de preuve), et nous voulons être capables de prouver la postcondition de
notre lemme (ligne 40).


En faisant cela, nous assurons que nous avons construit un contexte qui ne
contient que les informations nécessaires pour construire le code de preuve
permettant de déduire la conclusion (ligne 40) depuis les prémisses (ligne 36).
Maintenant écrivons la macro.


\CodeBlockInput[9][19]{c}{lemma-macro-2-2.c}


Nous ne détaillerons pas ce code, car il est très similaire à ce que nous avons
écrit au début de cette section. La seule petite subtilité est l'assertion qui
permet d'aider les solveurs SMT à relier les positions mémoire entre
\CodeInline{L1} et \CodeInline{L2} aux lignes 16--17. Avec cette macro, nous
pouvons voir que l'assertion à la fin de la fonction
\CodeInline{context\_to\_prove\_shift\_ptr} est correctement validée. Par
conséquent, nous pouvons espérer qu'elle sera capable d'aider les prouveurs à
obtenir une conclusion similaire dans un contexte similaire (c'est-à-dire un
contexte où nous savons que \CodeInline{shifted} est validée pour un certain
tableau entre labels).


Finalement, nous pouvons compléter la preuve de notre fonction \CodeInline{callee}
en utilisant notre macro lemme :


\CodeBlockInput[52][61]{c}{lemma-macro-2-2.c}


Nous pouvons constater que même si cette technique permet d'injecter le code de
preuve avec une seule ligne de code, elle peut injecter beaucoup de code à la
position où nous l'utilisons. De plus, lorsque nous injectons ce code à un endroit
où nous savons qu'il sera utile, le contexte correspondant peut déjà être plutôt
complexe. Il n'est donc pas rare d'avoir à modifier légèrement la macro pour
ajouter un peu d'information qui n'est pas nécessaires dans un contexte bien
propre comme celui que nous utilisons pour produire la macro.


Notons qu'en cela, à la différence de la fonction lemme qui a un comportement
très proche d'un lemme « classique », au sens où elle nous permet de faire une
déduction immédiate d'une conclusion à partir de certaines prémisses à un point
particulier de programme sans avoir à en refaire la preuve ; la macro lemme,
elle, s'éloigne beaucoup du comportement d'un lemme « classique », car elle
implique de refaire la preuve à chaque point où l'on a besoin de cette déduction.


Tout ceci peut rendre le contexte beaucoup plus gros, et plus difficile à utiliser
pour les solveurs SMT. Il y a d'autres limitations à cette technique et le lecteur
très attentif aura déjà pu les constater. Parlons-en.



\levelThreeTitle{Limitations}


La principale limitation des fonctions lemmes et macros lemmes
est le fait que nous sommes limités à des types C. Par exemple, si nous
comparons notre lemme \CodeInline{element\_level\_sorted\_is\_sorted} avec la
fonction lemme correspondante, le type original de la valeur
\CodeInline{len} est un type entier mathématique, tandis que dans la
fonction lemme, ce type est \CodeInline{size\_t}. Cela signifie que là
où notre lemme était vrai pour tout entier, et donc qu'il pouvait être utilisé
peu importe que la variable représentant la taille soit un \CodeInline{int},
ou un \CodeInline{unsigned} (ou n'importe quel autre type entier), à l'opposé,
notre fonction ne peut être utilisée que pour les types qui peuvent être
convertis de manière sure vers \CodeInline{size\_t}. Cependant, cette limitation
n'est généralement pas un problème : nous avons juste à exprimer notre
spécification dans le type le plus gros que nous avons à considérer dans notre
programme et la plupart du temps cela sera suffisant. Et si ce n'est pas le cas,
nous pouvons par exemple dupliquer le lemme pour les types qui nous intéressent.
La plupart du temps cette limitation est largement gérable puisque nous
travaillons avec les types utilisés dans le programme à prouver.


Dans certains cas, en revanche, cela contraint notre manière de modéliser des
propriétés, ce qui est principalement lié aux types logiques que nous pouvons
utiliser pour modéliser certaines structures de données concrètes. Par exemple,
pour modéliser une liste chaînée, nous pouvons utiliser le type logique ACSL
\CodeInline{\textbackslash{}list<Type>} et exprimer une propriété inductive ou
axiomatique pour définir comment une liste chaînée concrète peut être modélisée
par une liste logique. Nous pourrions donc avoir des lemmes à propos des listes
logiques, comme :

\begin{CodeBlock}{c}
/*@
  lemma in_list_in_sublist:
    \forall \list<int> l, l1, l2, int element ;
      l == (l1 ^ l2) ==>      // Here, ^ denotes lists concatenation
      (in_list(element, l) <==> (in_list(element, l1) || in_list(element, l2))) ;
*/
\end{CodeBlock}


Nous ne pouvons pas écrire une fonction lemme avec du code de preuve
pour cette propriété puisque nous n'avons pas de moyen d'utiliser ce type logique
dans du code C, et donc, aucun moyen d'écrire une boucle et un invariant qui nous
permettraient de prouver cette propriété.


L'autre limitation est liée aux macros lemmes et ce que nous avons déjà
mentionné dans le chapitre précédent à propos des assertions. En ajoutant trop
d'assertions, le contexte de preuve peut devenir trop gros et trop complexe, et
donc difficile à manipuler pour les solveurs SMT. Utiliser des
macros lemmes peut générer beaucoup de code et d'annotations et amener
à de plus gros contextes preuve. Elles devraient
donc être utilisées avec beaucoup de parcimonie.


Finalement, selon la propriété à prouver, il peut être difficile de trouver un
code de preuve. En effet, les assistants de preuve comme Coq sont conçus pour
être capables d'exprimer des preuves même pour des propriétés très complexes,
en se reposant sur une vue très haut niveau de nos problèmes, tandis que C a été
conçu pour écrire des programmes, et avec une vue très détaillée de la manière de
résoudre le problème. Il peut donc parfois être difficile d'écrire un programme
C permettant de prendre en compte certaines propriétés et plus encore de trouver
un invariant utilisable lié à nos boucles.


\levelThreeTitle{Encore un peu de tri par insertion}


Maintenant, revenons à notre preuve du tri par insertion et voyons comment nous
pouvons nous débarrasser de nos preuves interactives pour cette fonction. Notons
cependant que dans cette preuve, nous avons souvent besoin de macros puisqu'il
n'a pas été particulièrement écrit avec comme objectif de le vérifier plus tard
(pour cela, le lecteur peut se référer au livre {\em ACSL by Example} qui peut être
adapté avec une technique similaire et est beaucoup plus facile à prouver). Donc
dans cet exemple, nous poussons les solveurs SMT vers leurs limites à cause des
gros contextes de preuve. En fonction de la puissance de la machine sur laquelle
la preuve est lancée, la preuve pourrait approcher les 120 secondes (ce qui est
déjà long pour un solveur SMT). Dans cet exemple, nous illustrerons les trois
cas d'usage que nous avons vu du code fantôme jusqu'ici :


\begin{itemize}
    \item écris directement un code pour construire une preuve,
    \item écrire (et utiliser) des fonctions lemmes,
    \item écrire (et utiliser) des macros lemmes.
\end{itemize}


Nous utilisons également des assertions pour rendre le contexte de preuve plus
riche afin que les solveurs SMT puissent prouver les propriétés qui nous intéressent.
Certaines parties des annotations que nous avons écrites précédemment seront
équivalentes à ce que nous avons fait précédemment. Nous rappellerons leur
but dans chaque fonction. Ensuite, nous utilisons la même définition axiomatiques
pour le comptage d'occurrences. De plus, nous conservons ces définitions de
prédicats :


\CodeBlockInput[25][42]{c}{insert-sort-auto.c}


puisque nous en avons besoin, ainsi que le lemme à propos de la transitivité du
comptage d'occurrences, puisqu'il était prouvé automatiquement par les solveurs
SMT (nous pouvons donc le garder puisqu'il ne nécessite pas de preuve interactive
de notre part).


\CodeBlockInput[43][48]{c}{insert-sort-auto.c}


Commençons par la fonction \CodeInline{insertion\_sort}. Dans cette fonction,
nous avons écrit trois assertions :


\CodeBlockInput[87][108]{c}{insert-sort-auto.c}


La première nous assure que le début du tableau où nous avons inséré une valeur
est une permutation de la même plage de valeur avant l'appel à \CodeInline{insert}.
Comme c'est la postcondition de la fonction, elle n'est pas nécessaire, mais nous
la conservons la pour illustration. La dernière assertion est la propriété que
nous voulons prouver pour obtenir suffisamment de connaissance pour que le
lemme à propos de la transitivité de la permutation soit utilisé (et montre qu'à
la fin du bloc de la boucle, puisque le tableau est une permutation du tableau
au début, qui est lui-même une permutation du tableau original, alors le tableau
à la fin du corps est une permutation du tableau original).


La seconde assertion dit que la seconde partie du tableau reste inchangée, et nous
voulons utiliser cette connaissance pour montrer que le nombre d'occurrences des
valeurs n'a pas changé. Ici, nous pourrions utiliser une combinaison des
fonctions et macros lemmes pour prouver que la plage complète est une
permutation (comme nous le ferons pour l'autre fonction). Cependant ici, écrire
directement le code est un peu plus simple et requiert moins de preuves (comme
nous le verrons plus tard), écrivons donc directement le code qui permet de
prouver notre propriété.


Pour montrer que la plage complète est une permutation, nous devons montrer que le
nombre d'occurrences de chaque valeur n'a pas changé. Nous savons que la première
partie du tableau est une permutation de la même plage au début du corps de la
boucle. Donc, nous savons déjà que le nombre d'occurrences de chaque $v$ n'a pas
changé pour une partie de notre tableau. En utilisant une boucle avec
\CodeInline{j} allant de \CodeInline{i} à \CodeInline{end} et un invariant
\CodeInline{permutation{L,PI}(a, beg, j)}, nous pouvons continuer le comptage des
occurrences pour le reste de notre tableau, avec la connaissance que la fin n'a
pas changé (quand \CodeInline{i+1} est plus petit que \CodeInline{end} sinon
nous n'avons simplement plus rien à compter):


\CodeBlockInput[271][287]{c}{insert-sort-auto-proved.c}


ce qui est suffisant pour assurer que la fonction \CodeInline{insertion\_sort}
respecte sa spécification à condition de finir la preuve de la fonction
\CodeInline{insert}. Cette seconde fonction réalise des actions plus
complexes, nous partirons de cette version annotée :


\CodeBlockInput[50][84]{c}{insert-sort-auto.c}


À nouveau, la preuve que cette fonction maintient la permutation du tableau est
la partie la plus difficile de notre travail. Le fait que cette fonction
garantisse que les valeurs sont bien triées est déjà établie. Utiliser la
même technique que pour la fonction \CodeInline{insertion\_sort} n'est pas si
simple ici. En effet, la seconde partie du tableau a été « tournée » ce qui
rend la propriété un peu plus complexe. Du coup, commençons par séparer notre
tableau à la position d'insertion en deux parties, où nous montrons
respectivement que :


\begin{itemize}
    \item pour la première partie, puisqu'elle est inchangée, pour tout $v$
          le nombre d'occurrences n'a pas changé non plus ;
    \item pour la seconde partie, puisqu'elle a tourné, pour tout $v$, le
          nombre d'occurrences n'a pas changé.
\end{itemize}


D'abord, définissons une fonction lemme qui permet d'explicitement
couper une plage de valeur en deux sous-parties dans lesquelles nous pouvons
compter séparément :


\CodeBlockInput[57][77]{c}{insert-sort-auto-proved.c}


Nous pouvons noter que cette propriété est prouvée d'une manière qui est très
similaire à ce que nous avons écrit dans le corps de la boucle de la fonction
\CodeInline{insertion\_sort}, nous commençons au point à partir duquel nous
voulons compter et nous montrons que la propriété reste vraie pour le reste
du tableau.


Nous pouvons utiliser notre fonction pour couper le tableau à la bonne position
après la boucle. Cependant, nous ne pouvons le faire que pour le nouveau contenu
du tableau. En effet, pour établir cela pour le tableau original, nous devons
appeler la fonction sur le tableau original pour lequel nous ne connaissons pas
encore la valeur de $i$. Par conséquent, écrivons une autre version de la
propriété « \textit{split} » qui nous montrer que nous pouvons couper le tableau à toute
position, donc rendons la variable \CodeInline{split} universellement quantifiée,
et utilisons la fonction précédente pour montrer que cette nouvelle propriété est
vraie.


\CodeBlockInput[79][102]{c}{insert-sort-auto-proved.c}


Et nous pouvons souper notre tableau original et le nouveau :


\begin{CodeBlock}{c}
void insert(int* a, size_t beg, size_t last){
  size_t i = last ;
  int value = a[i] ;
  // split before modifying
  //@ ghost l_occurrences_of_split(a, beg, last+1);

  /*@ LOOP ANNOT */
  while(i > beg && a[i - 1] > value){
    a[i] = a[i - 1] ;
    --i ;
  }
  a[i] = value ;
  // Assertions ...

  // split after modifying, now we know "i"
  //@ ghost l_occurrences_of_explicit_split(a, beg, i, last+1);
}
\end{CodeBlock}


Maintenant, les seules parties restantes de la preuve sont de montrer qu'un tableau
inchangé est une permutation et ensuite que la rotation maintient également une
permutation. Ici, nous avons besoin d'une macro. Commençons avec la plus facile :
le tableau inchangé, que l'on a prouvé quasiment à l'identique dans la fonction
\CodeInline{insertion\_sort}. Nous commençons par construire notre contexte de
preuve :


\CodeBlockInput[142][158]{c}{insert-sort-auto-proved.c}


La fonction \CodeInline{unchanged\_permutation\_premise} assure que nous avons
modifié le tableau (et donc créé un nouvel état mémoire) et que le tableau est
inchangé entre la précondition et la postcondition. Nous pouvons construire
notre macro lemme :


\CodeBlockInput[131][139]{c}{insert-sort-auto-proved.c}


qui correspond presque à ce que nous avons écrit pour \CodeInline{insert\_sort},
et utiliser cette macro là où nous en avons besoin dans la fonction
\CodeInline{insert}.


\CodeBlockInput[249][251]{c}{insert-sort-auto-proved.c}


La seule propriété restante est la plus complexe et concerne le prédicat
\CodeInline{rotate\_left}. Écrivons d'abord un contexte pour préparer notre
macro.


\CodeBlockInput[187][204]{c}{insert-sort-auto-proved.c}


Comment pouvons-nous prouver cette propriété ? Nous devons d'abord constater
que puisque tous les éléments depuis le début jusqu'à l'avant-dernier ont été
décalées d'une cellule, le nombre d'occurrences dans cette partie décalée n'a
pas changé. Ensuite, nous devons montrer que le nombre d'occurrences de $v$
respectivement dans la dernière cellule du tableau original et la première
cellule du nouveau tableau est le même (puisque l'élément correspondant est le
même). À nouveau, nous nous reposons sur la fonction \CodeInline{split} pour compter
séparément les éléments décalés et l'élément qui est déplacé de la fin vers le
début. Cependant, l'appel correspondant dans le tableau original doit à nouveau
être réalisée avant le code qui modifie le tableau original (voir ligne 198) dans
le code précédent, et nouvs devons prendre cela en compte quand nous insérerons
notre utilisation de la macro dans la fonction \CodeInline{insert}.


Présentons maintenant la macro qui est utilisée pour prouver que notre lemme
est valide :


\CodeBlockInput[160][185]{c}{insert-sort-auto-proved.c}


L'invariant de boucle est très similaire à ce que nous avons écrit jusqu'à
maintenant, la seule différence est que nous devons tenir compte du glissement
des éléments. De plus, pour l'invariant, nous avons dû ajouter une assertion
pour aider les prouveurs automatiques à remarquer que le dernier élément de
chaque plage est le même (notons que selon les versions des prouveurs ou la
puissance de la machine, cela peut parfois ne pas être nécessaire). Une différence
plus importante comparativement à nos exemples précédents est le fait qu'ici, nous
devons fournir plus d'information aux SMT solveurs en ajoutant d'autres appels
de fonction fantôme (ligne 170, pour couper le premier élément du tableau), ainsi
que des assertions pour guider les dernières étapes de preuve :


\begin{itemize}
    \item 175--179 : nous rappelons que le tableau original peut être coupé au
          niveau du dernier élément,
    \item 180--184 : nous montrons que comme le premier élément du tableau est le
          dernier élément du tableau original (182), le nombre d'occurrences pour
          toute valeur dans ces plages est le même (183--185).
\end{itemize}


Nous pouvons utiliser cette macro dans notre programme :


\CodeBlockInput[245][247]{c}{insert-sort-auto-proved.c}


Cependant, nous avons besoin de montrer que la plage au label \CodeInline{Pre} peut
être coupée à  \CodeInline{last}. Pour cela, nous utilisons une autre variante de la
fonction \CodeInline{split}, qui montre que toute sous-plage peut être coupée avant
le dernier élément (si elle n'est pas vide) :


\CodeBlockInput[104][128]{c}{insert-sort-auto-proved.c}


que nous pouvons ensuite appeler avant la boucle de la fonction \CodeInline{insert} :


\CodeBlockInput[215][220]{c}{insert-sort-auto-proved.c}


Notons que selon les versions des prouveurs automatiques, les assertions en lignes
180 à 184 de la macro, à propos de l'élément au début et à la fin du tableau,
pourraient ne pas être prouvées à cause de la complexité du contexte de preuve.
Aidons les solveurs une dernière fois en ajoutant un dernier lemme, automatiquement
prouvé par les solveurs SMT, qui nous énonce la relation en question pour tout
tableau et toute position du tableau :


\CodeBlockInput[49][54]{c}{insert-sort-auto-proved.c}


qui nous garantit que la fonction annotée résultante est entièrement prouvée :


\CodeBlockInput[206][254]{c}{insert-sort-auto-proved.c}


Nous mettons finalement en valeur le fait que le contexte de preuve peut rendre
le travail vraiment difficile pour les solveurs SMT. Tout simplement, si nous
inversons les preuves à propos du chaque partie du tableau, à savoir, en
commençant par la partie \CodeInline{unchanged} puis la partie \CodeInline{rotate},
la preuve a de très bonnes chances d'échouer, car elle fait grossir le contexte de
preuve pour la preuve la plus difficile.


\levelThreeTitle{Exercices}


\levelFourTitle{La somme des N premiers entiers}


En utilisant des fonctions lemmes, nous pouvons prouver que le lemme à
propos de la somme des N premiers entiers. Vous avez peut-être déjà fait cette
preuve au lycée, maintenant, il est temps de faire cette preuve en C et ACSL.
Écrire un contrat pour la fonction suivante qui exprimer en postcondition que la
somme des N premiers entiers est \CodeInline{N(N+1)/2}. Compléter le corps de la
fonction avec une boucle pour prouver la propriété. Nous conseillons de légèrement
modifier l'invariant pour faire disparaître la division (qui sur les entiers a
certaines propriétés qui rendent son utilisation difficile avec des solveurs SMT
en fonction des contraintes qui existent sur les valeurs utilisées).


\CodeBlockInput[1][12]{c}{ex-1-sum-of-n-integers.c}


Maintenant, généralisons à toutes bornes avec la somme de tous les entiers entre
deux bornes \CodeInline{fst} et \CodeInline{lst}. Nous fournissons la fonction
logique et le contrat, à vous d'écrire le corps de la fonction de manière à vérifier
la postcondition. À nouveau, nous conseillons d'exprimer l'invariant sans division.


\CodeBlockInput[16][30]{c}{ex-1-sum-of-n-integers.c}


Finalement, prouver cette fonction :


\CodeBlockInput[32][39]{c}{ex-1-sum-of-n-integers.c}


Cela ne devrait pas être trop difficile, et ce que nous obtenons est une preuve
que nous avons écrit une optimisation correcte pour la fonction qui calcule la
somme des N premiers entiers.


\levelFourTitle{Propriétés à propos du comptage d'occurrence}


Dans cet exercice, nous voulons prouver un ensemble de propriétés intéressantes
à propos de notre définition logique \CodeInline{l\_occurrences\_of} :


\CodeBlockInput{c}{ex-2-l_occurrences_of-props.c}


La fonction \CodeInline{occ\_bounds} doit énoncer que le nombre d'occurrences
de \CodeInline{v} dans un tableau est compris entre 0 et \CodeInline{len}.


La fonction \CodeInline{not\_in\_occ\_0} doit énoncer que si \CodeInline{v}
n'est pas dans le tableau alors le nombre d'occurrences de \CodeInline{v} est 0.


La fonction \CodeInline{occ\_monotonic} doit énoncer que le nombre d'occurrences
de \CodeInline{v} dans un tableau entre 0 et \CodeInline{pos} est inférieur
ou égal au nombre d'occurrences de \CodeInline{v} entre 0 et \CodeInline{more} si
\CodeInline{more} est supérieur ou égal à \CodeInline{pos}


La fonction \CodeInline{occ\_0\_not\_in} doit énoncer que si le nombre
d'occurrences de \CodeInline{v} dans le tableau est 0 alors \CodeInline{v} n'est
pas dans le tableau. Notons que \CodeInline{occ\_monotonic} serait probablement
utile.


La fonction \CodeInline{occ\_pos\_find} doit trouver un indice \CodeInline{i}
tel que \CodeInline{arr[i]} est \CodeInline{v}, à supposer que le nombre
d'occurrences de \CodeInline{v} est positif. \CodeInline{occ\_monotonic} peut
être utile.


Finalement, la fonction \CodeInline{occ\_pos\_exists} doit traduire le contrat
de la fonction précédente en utilisant une variable quantifiée existentitellement,
et utiliser la fonction précédente pour obtenir gratuitement la preuve.


Pour toutes ces fonctions, WP doit être paramétré avec le contrôle d'absence
d'erreurs d'exécution ainsi que les options \CodeInline{-warn-unsigned-overflow}
et \CodeInline{-warn-unsigned-downcast}.


\levelFourTitle{Un vrai exemple avec la somme}


Reprendre la preuve effectuée dans le chapitre précédent pour
l'exercice~\ref{l4:proof-methodologies-triggering-lemmas-exercises-sum}. Modifier
les annotations pour assurer que plus aucun lemme classique n'est nécessaire.
Voici un squelette pour le fichier :



\CodeBlockInput{c}{ex-3-sum-content.c}