chapter_method.tex

\chapter{Aide à la preuve combinant NCD et SWD}
\label{sec:method}

\chapterintro


Dans ce chapitre nous présentons notre méthode de diagnostic des échecs de
preuve utilisant les techniques de détection présentées dans les
chapitres~\ref{sec:ncd} et~\ref{sec:swd}.
La partie~\ref{sec:method-ex} présente l'exemple sur lequel nous nous
appuierons dans ce chapitre, la partie~\ref{sec:method-proof-failures} rappelle
les différentes causes possibles d'un échec de preuve, la
partie~\ref{sec:method-presentation} présente notre méthode de diagnostic des
échecs de preuve et la partie~\ref{sec:method-suggestions} suggère les actions
à effectuer après diagnostic d'un échec de preuve.


\section{Exemple illustratif}
\label{sec:method-ex}


Nous illustrons sur le programme C donné en figure~\ref{fig:rgf1} les problèmes
qui se posent lors de la vérification déductive d'un programme et les solutions
que nous proposons.
Cet exemple provient d'un travail de spécification formelle et de vérification
déductive~\cite{Genestier/TAP15} que j'ai réalisé avec R. Genestier et
A. Giorgetti.
Il implémente un algorithme proposé dans \cite[page 235]{Arndt/10}.
L'exemple de la figure~\ref{fig:rgf1} concerne la génération de fonctions à
croissance limitée (ou RGF pour \textit{Restricted Growth Functions}).
Une fonction à croissance limitée de taille $n$ est une endofonction $r$ de
$\{0, ..., n-1\}$ telle que $r(0) = 0$ et $r(k) \le r(k-1)+1$ pour
$1 \le k \le n-1$.
Nous représentons une endofonction $r$ de $\{0, ..., n-1\}$ par les valeurs d'un
tableau C.
Le prédicat \acsl \lstinline{is_rgf} aux lignes 1--4 de la figure~\ref{fig:rgf1}
exprime cette propriété sur un tableau \lstinline'a' de taille \lstinline'n'.


\begin{figure}[tb]
  \centering
  \lstinputlisting[multicols=2]{listings/rgf_0.c}
  \caption{Fonction ``successeur'' d'une RGF \label{fig:rgf1}}
\end{figure}


La figure~\ref{fig:rgf1} présente une fonction principale \lstinline{f} et une
fonction auxiliaire \lstinline{g}.
La précondition de \lstinline{f} affirme que \lstinline{a} est un tableau
valide de taille \lstinline{n>0} (lignes 27--28) qui représente une RGF
(ligne 29).
La postcondition affirme que la fonction \lstinline'f' ne peut modifier que le
contenu du tableau \lstinline{a}, à l'exception du premier élément
\lstinline{a[0]} (ligne 30), et que le tableau \lstinline{a} en sortie de la
fonction est toujours une RGF (ligne 31).
De plus, si la fonction retourne 1, alors la RGF générée \lstinline{a} doit
respecter une propriété d'ordre lexicographique selon laquelle
il existe un indice $i$ ($0 \le i \le n-1$) tel qu'en fin de fonction, $a[i]$
est supérieur à sa valeur en début de fonction et $a[j]$ est inchangé pour tout
indice $j$ inférieur à $i$ (lignes 32--36).
Ici \lstinline{\at(a[j],Pre)} dénote la valeur de \lstinline{a[j]} dans l'état 
\lstinline{Pre} de la fonction, c'est-à-dire avant l'exécution de la fonction.

Observons maintenant le corps de la fonction \lstinline{f} de la
figure~\ref{fig:rgf1}. 
La boucle aux lignes 42--43 parcourt le tableau de droite à gauche afin de
trouver l'élément non-croissant le plus à droite, c'est-à-dire l'indice maximum
\lstinline{i} du tableau tel que \lstinline{a[i] <= a[i-1]}.
Si un tel indice est trouvé, la fonction incrémente \lstinline{a[i]} (ligne 46)
et remplit le reste du tableau avec \lstinline{0} (appel à la fonction
\lstinline{g}, line 47).
Le contrat de boucle (lignes 39--41) spécifie l'intervalle de valeurs de la
variable \lstinline'i', les variables que la boucle peut modifier, ainsi que
le variant de boucle qui permet d'assurer la terminaison de la boucle.
L'expression du variant de boucle doit être positive ou nulle au début de chaque
itération et doit décroître strictement entre deux itérations.

La fonction \lstinline{g} est utilisée pour remplir le tableau avec des zéros
à droite de l'indice \lstinline{i}.
En plus des contraintes de taille et de validité du tableau (lignes 12--13),
sa précondition demande que les éléments de \lstinline{a} jusqu'à l'indice
\lstinline{i} forment une RGF (lignes 14--15).
La fonction ne peut modifier que les éléments de \lstinline{a} à partir de
l'indice \lstinline{i+1} (ligne 16) et produit une RGF (line 17).
Les invariants de boucle précisent l'intervalle de valeurs de la variable de
boucle \lstinline{k} (ligne 20), et énoncent que la propriété \lstinline{is_rgf}
est satisfaite jusqu'à \lstinline{k} (ligne 21).
Cet invariant permet à un outil de vérification déductive de prouver la
postcondition.
L'annotation \lstinline{loop assigns} (ligne 22) énonce que la boucle peut
uniquement modifier les valeurs de \lstinline{k} et des éléments de
\lstinline{a} à partir de l'indice \lstinline{i+1}.
Le terme \lstinline{n-k} est le variant de la boucle (ligne 23).

Le lemme \lstinline'max_rgf' aux lignes 6--10 affirme que si un tableau
encode une RGF, alors chacun de ses éléments est au plus égal à son indice.
Ce lemme n'est pas prouvé automatiquement par \Wp mais peut néanmoins être
utilisé pour assurer l'absence de débordement d'entier signé à la ligne 46.

Les fonctions de la figure~\ref{fig:rgf1} peuvent être prouvées à l'aide de \Wp.

Supposons maintenant que cet exemple contient une des quatre erreurs suivantes :
\begin{enumerate}
\item \emph{soit} l'ingénieur validation oublie la précondition de la ligne 29,
\item \emph{soit} il se trompe dans l'affectation
  \lstinline[style=c]'a[i]=a[i]+2;' ligne 46,
\item \emph{soit} il écrit une clause
  \lstinline[style=c]'loop assigns i,a[1..n-1];' trop imprécise ligne 40,
\item \emph{soit} il oublie de fournir le lemme des lignes 6--10.
\end{enumerate}
Dans chacun de ces scénarios, la preuve du programme échoue (sur la précondition
de \lstinline{g} lors de son appel ligne 47 et/ou sur l'assertion ligne 45).

Les deux premiers cas présentent une non-conformité entre le code et
la spécification, dans le troisième cas l'échec de la preuve est dû à une
faiblesse de sous-contrat, et le dernier cas est dû à une limitation ou une
faiblesse du prouveur utilisé.


\section{Échecs de preuve}
\label{sec:method-proof-failures}


Rappelons les différentes causes possibles d'un échec de la vérification
déductive d'un programme.

\textbf{Non-conformité.}
Un échec de preuve peut être dû à une non-conformité du code d'un programme par
rapport à sa spécification formelle.
Le chapitre~\ref{sec:ncd} a défini la notion de non-conformité, de
contre-exemple de non-conformité (\NCCE) et a présenté une méthode de détection
des non-conformités (\NCD).

\textbf{Faiblesse de sous-contrat.}
Un échec de preuve peut également être dû à une faiblesse d'un (ou de plusieurs)
sous-contrat(s), ce qui cause un manque d'hypothèses et ne permet pas de prouver
une propriété.
Le chapitre~\ref{sec:swd} a défini la notion de sous-contrat, de faiblesse de
sous-contrat, de contre-exemple pour la faiblesse de sous-contrats (\SWCE) et
a présenté une méthode de détection de ces faiblesses (\SWD).

\textbf{Incapacité de prouveur.}
Quand il n'existe ni non-conformité, ni faiblesse de sous-contrats, l'échec de
preuve est dû aux limitations du prouveur.
Nous introduisons la notion d'incapacité de prouveur.

\begin{definition}[Incapacité de prouveur]
\label{def:prov-incap}
On dit qu'un échec de preuve du programme $P$ est lié à une
\emph{incapacité de prouveur} si pour tout cas de test $V$ pour la fonction $f$
respectant sa précondition, $P^{NC}$ et $P^{\GSW}$ ne rapportent aucune violation
d'annotation sur $V$.
En d'autres termes, il n'y a ni \NCCE, ni \GSWCE pour $P$.
\end{definition}

Cette catégorie contient entre autres les limitations techniques des prouveurs
comme par exemple la difficulté que peuvent rencontrer les prouveurs à
instancer les variables quantifiées dans un prédicat \lstinline'\exists'.
La nécessité d'écrire des lemmes pour aider le prouveur, voire d'avoir recours
à un assistant de preuve comme \coq définit également une incapacité de
prouveur.


\section{Présentation de la méthode}
\label{sec:method-presentation}


\begin{figure*}[bt]\centering
\begin{tikzpicture}
  \node(p) [data] {$P$};
  \node(ncd) [right of=p,test,node distance=1.7cm] {$\NCD(P)$};
  \node(ncce1) [below of=ncd,node distance=1.2cm] {\circled{1} $V$ est un \NCCE};
  \path[darrow] (ncd) -- node[left] {(\nc, $V$, $a$)} (ncce1);
  \path[arrow] (p) -- (ncd);
  \node(cwd) [right of=ncd,test,node distance=4cm] {$\CWD(P)$};
  \path[darrow] (ncd.east) -- node[above] {\no{} / \textsf{?}} (cwd);

  % CWD found a CE
  \node(cwce-ncce) [below of=cwd,node distance=1.2cm]{\circled{2} $V$ est un \CWCE};
  \path[darrow] (cwd) -- node[right] {(\cw, $V$, $a$, $S$)} (cwce-ncce);
  \path[darrow] (cwd) -- node[above,sloped,xshift=-3mm] {~~~(\nc, $V$, $a$)} (ncce1);

  % CWD did not found any CE
  \node(cov-2) [right of=cwd,test,node distance=4cm]{
    $\NCD(P)=~$\no$\land$\\ $\CWD(P)=~$\no};
  \path[darrow] (cwd.east) -- node[above] {\no{} / \textsf{?}} (cov-2);
  \node(pw) [below of=cov-2,node distance=1.45cm,align=center]{\circled{3} Incapacité\\ de prouveur};
  \path[darrow] (cov-2) -- node[right] {true} (pw);
  \node(qm) [right of=cwce-ncce,node distance=8cm] {\circled{4} Non classifié};
  \path[darrow] (cov-2) -| node[below left] {false} (qm);
\end{tikzpicture}
\vspace{-2mm}
\caption{Méthode de vérification combinant \NCD et \SWD en cas d'échec de
  preuve du programme $P$}
\label{fig:method-short}
\end{figure*}

La méthode que nous proposons est illustrée par la
figure~\ref{fig:method-short}.
Supposons que la preuve du programme annoté $P$ échoue pour une annotation
non-imbriquée $a\in\A$ quelconque, où $\A$ est l'ensemble des annotations
non-imbriquées de $f$ et des annotations du contrat de $f$.
La première étape est d'essayer de trouver une non-conformité entre le code et
la spécification en utilisant \NCD.
Si une telle non-conformité a été trouvée, un \NCCE est généré (cas \circled{1}
sur la figure~\ref{fig:method-short}) et l'échec de la preuve est classifié
comme une non-conformité.
Si cette première étape n'a pas pu générer de contre-exemple, l'étape \SWD
combine \SSWD et \GSWD et essaie de générer des \SWCE{}s pour les sous-contrats
pris un-à-un, sinon des \SWCE{}s pour l'ensemble des sous-contrats, jusqu'à ce
que le premier contre-exemple soit généré et classifié (soit comme un \NCCE
\circled{1}, soit comme un \SWCE \circled{2})
Si aucun contre-exemple n'a été trouvé, nous analysons le résultat de \NCD et
\SWD.
Si \NCD et \SWD ont retourné \textsf{no}, c'est-à-dire que \NCD et \GSWD ont
couvert tous les chemins du programme sans produire de contre-exemple, l'échec
de preuve est dû à une incapacité de prouveur \circled{3} (voir la
définition~\ref{def:prov-incap}).
Sinon, l'échec de preuve reste non classifié \circled{4}.
La figure~\ref{tab:versions-rgf} associe à chacun des quatre cas une version
modifiée de l'exemple illustratif de la figure~\ref{fig:rgf1}.
Dans chaque cas, nous détaillons les lignes modifiées dans le programme de la
figure~\ref{fig:rgf1} pour obtenir le nouveau programme, les résultats
intermédiaires de la vérification déductive, de \NCD et \SWD, et le verdict
final de la méthode (ainsi que le contre-exemple éventuellement généré).


\begin{figure*}[bt]\centering
  \includegraphics[scale=.85]{table_rgf.pdf}
  \caption{Résultats de la méthode sur différentes versions de l'exemple de la
    figure~\ref{fig:rgf1}.}
  \label{tab:versions-rgf}
\end{figure*}


La classification de l'échec de preuve, le contre-exemple $V$, le chemin
d'exécution $\pi_V$ activé par $V$, ainsi que l'annotation invalidée $a$ et
l'ensemble des sous-contrats trop faibles $S$ peuvent s'avérer très utiles à
l'ingénieur validation.
Supposons que l'on essaie de prouver avec \Wp une version modifiée de la
fonction $f$ de la figure~\ref{fig:rgf1} où la précondition de la ligne 29 est
manquante (\#1 sur la figure~\ref{tab:versions-rgf}).
La preuve de la précondition de $g$ (ligne 15) lors de l'appel de la fonction
ligne 47 échoue sans indiquer de raison précise. 
L'étape \NCD génère un \NCCE (cas \circled{1}) où la propriété
\lstinline'is_rgf(a,n)' est clairement fausse puisque \lstinline'a[0]' est
différent de zéro, et indique l'annotation non respectée (ligne 15).
Ceci permet à l'ingénieur validation de comprendre et corriger le problème.

Supposons maintenant que la clause de la ligne 40 a été écrite de manière
erronée de la manière suivante : \lstinline'loop assigns i, a[1..n-1];' (\#2 sur
la figure~\ref{tab:versions-rgf}).
La boucle aux lignes 42--43 préserve néanmoins son invariant.
L'étape \NCD ne trouve aucun \NCCE, puisque cette modification n'a introduit
aucune non-conformité entre le code et sa spécification.
L'étape $\SSWD$ pour le contrat de cette boucle détecte une faiblesse de
sous-contrat pour ce même contrat (cas \circled{2}), et indique que la
précondition de $g$ (ligne 15) est fausse lors de l'appel de la fonction
ligne 47.
Avec l'information de la faiblesse du sous-contrat de la boucle, l'ingénieur
validation essaiera de trouver la cause de la faiblesse et renforcera le contrat
de boucle en conséquence.

Supposons maintenant que nous voulions prouver l'absence de débordement
arithmétique à la ligne 46 de la figure~\ref{fig:rgf1}, et que le lemme aux
lignes 6--10 est manquant (\#4 sur la figure~\ref{tab:versions-rgf}).
La preuve échoue sans donner de raison précise puisque le prouveur n'effectue
pas l'induction nécessaire afin de déduire les bornes de \lstinline'a[i]'.
Ni \NCD ni \SWD n'ont réussi à produire de contre-exemple, et puisque le
programme initial comporte trop de chemins d'exécution faisables pour pouvoir
tous les couvrir dans le temps imparti, leur résultat est \textsf{?}
(non classifié) (cas \circled{4}).
Dans une telle situation, l'ingénieur validation peut décider de réduire le
domaine des entrées du programme.
Supposons dans ce cas qu'il choisisse de restreindre le domaine de
\lstinline'n' à l'aide de la précondition pour $f$ suivante :
\lstinline'requires n>0 && n<21;' (\#3 sur la figure~\ref{tab:versions-rgf}).
Avec cette nouvelle contrainte sur les entrées, l'application de la méthode
permet de couvrir tous les chemins du programme (respectant la nouvelle
précondition) avec \NCD et \SWD sans trouver de contre-exemple.
La méthode classifie l'échec de preuve du programme avec le domaine restreint
sur les variables comme une incapacité de prouveur (cas \circled{3}).
Ces résultats poussent l'ingénieur validation à penser que l'échec de la preuve
sur la variante \#4 du programme, pour un \lstinline'n' plus grand, est causé
par les mêmes raisons.
Ainsi, l'ingénieur validation préfèrera essayer une preuve interactive, ou
écrire des lemmes ou assertions supplémentaires, et ne perdra pas son temps à
chercher une non-conformité ou une faiblesse de contrat.


\section{Suggestions d'actions}
\label{sec:method-suggestions}


\begin{figure*}[bt]\centering
  \begin{tabular}{p{.5cm}|>{\centering\arraybackslash}p{5.6cm}|>{\centering\arraybackslash}p{7.8cm}}
    \textbf{Cas} & {\centering\textbf{Verdict}} & \textbf{Suggestions} \\
    \hline
    \circled{1} & Non-conformité du code vis-à-vis de l'annotation $a$:
    (\nc, $V$, $a$)
    &
    corriger l'annotation $a$
    ou le code menant à $a$ par le chemin d'exécution $\pi_V$,
    ou renforcer la précondition de la fonction sous vérification
    \\
    \hline
    \circled{2} & Faiblesse de sous-contrats parmi ceux de $S$ vis-à-vis de
    l'annotation $a$ :
    \ (\cw,~$V$,~$a$,~$S$)
    & renforcer un ou plusieurs sous-contrats de $S$ \\
    \hline
    \circled{3} & Incapacité de prouveur \newline (test complet)
    & ajouter des lemmes ou des assertions pour aider le prouveur,
    ou utiliser un autre prouveur plus approprié,
    ou utiliser un prouveur interactif (comme \coq) \\
    \hline
    \circled{4} & Non-classifié \newline (test incomplet)
    & renforcer la clause $\mbox{\lstinline'typically'}$
    ou le critère de couverture (par exemple $k$-path),
    ou augmenter le temps alloué à la génération de tests ({\em timeout}) \\
  \end{tabular}
  \caption{Suggestions d'actions pour chaque catégorie d'échec de preuve}
  \label{fig:suggestions}
\end{figure*}


À partir des différents résultats possibles de la méthode présentée dans la
partie~\ref{sec:method-presentation}, nous pouvons suggérer à l'ingénieur
validation les actions à effectuer une fois que l'échec de preuve a été
diagnostiqué, afin de l'aider dans son processus de spécification et de
vérification déductive.
Nos suggestions sont résumées en figure~\ref{fig:suggestions}.
Nous les expliquons ci-dessous.

Une \emph{non-conformité} du code vis-à-vis d'une annotation $a$ signifie qu'il
y a une incohérence entre la précondition, l'annotation $a$ et le code du
chemin de programme $\pi_V$ menant à $a$.
Grâce au contre-exemple $V$, les valeurs des variables à différents points du
programme suivant le chemin $\pi_V$ peuvent être tracées ou observées à l'aide
d'un débogueur \cite{Muller/FM11}.
Dans \framac, l'exécution de $V$ peut être observée à l'aide de \Value ou
\pathcrawler.
Ceci aide l'ingénieur validation dans sa compréhension de l'erreur.
En effet, si un \NCCE est généré, l'ingénieur n'a pas besoin de tenter une
preuve déductive ou de chercher une faiblesse de contrat dans la spécification,
puisque la raison de l'échec de la preuve est nécessairement liée à une
non-conformité entre le code et les annotations traversées par le chemin
d'exécution $\pi_V$.

Une \emph{faiblesse} d'un ensemble de sous-contrats $S$ signifie qu'au moins un
des sous-contrats de $C$ doit être renforcé.
Par les définitions~\ref{def:GSW} et~\ref{def:SSW}, la non-conformité est
exclue, ce qui veut dire que l'exécution de $P^{\NC}$ sur $V$ respecte
l'annotation $a$.
Notre suggestion pour l'ingénieur validation est donc de renforcer les
sous-contrats de $S$.
Dans le cas d'une faiblesse d'un seul sous-contrat, $S$ est un singleton donc
la suggestion est précise et aide l'utilisateur.
Ici encore, essayer une preuve interactive ou ajouter des assertions ou des
lemmes supplémentaires sera inutile puisque le contre-exemple témoigne de
l'impossibilité de prouver la propriété.

Pour une \emph{incapacité de prouveur}, l'ingénieur validation peut écrire des
lemmes ou des assertions, ou ajouter des hypothèses qui peuvent aider le
prouveur.
Il peut aussi essayer un autre prouveur automatique plus approprié au programme
à vérifier, ou encore, utiliser un assistant de preuve comme \coq afin de ne
pas souffrir des limitations des prouveurs automatiques, mais cette tâche peut
s'avérer longue et complexe.

Enfin, lorsque le verdict de la méthode est \emph{non classifié}, la génération
de tests pour \NCD et/ou \SWD ne parvient pas à conclure dans le temps imparti
(le {\em timeout} a été atteint), nous suggérons donc à l'ingénieur validation
de renforcer la précondition du programme pour le test afin de réduire le
domaine des entrées, ou de repousser le {\em timeout} afin de donner à la
méthode plus de temps pour conclure.


\section*{Conclusion du chapitre}


Dans ce chapitre nous avons rappelé les différentes causes possibles d'un échec
de preuve.
Nous avons présenté notre méthode de diagnostic des échecs de
preuve utilisant les techniques de détection présentées dans les
chapitres~\ref{sec:ncd} et~\ref{sec:swd}.
Enfin, nous avons suggéré des actions qu'un ingénieur validation peut effectuer
après qu'un échec de preuve ait été diagnostiqué et ce dans chacune des quatre
situations identifiées : non-conformité, faiblesse de sous-contrat, incapacité
du prouveur et test complet, et incapacité du prouveur et test incomplet
(non-classifié).
Ces suggestions d'actions sont une assistance à l'ingénieur validation dans son
processus de spécification et de vérification déductive d'un programme.