new-content: counter-examples

english/function-contract/contract.tex

@@ -386,7 +386,7 @@
 
 
 
-What does WP do using these properties? In fact, it transforms them
+How does WP deal with these properties? In fact, it transforms them
 into a logic formula and then asks different provers if it is
 possible to satisfy this formula (to find, for each variable, a value
 that can make the formula true), and it determines if the property can
@@ -398,30 +398,54 @@
 automatic solvers.
 
 
+Often, automatic solvers do not give extensive feedback after attempting a
+proof. When they succeed in proving a verification condition, the answer is
+``yes'', which is fine because we do not really need more information most of
+the time in this case. But they can fail, either because the property cannot be
+proved (for example if it is simply wrong or if some hypotheses are missing) or
+because the proof is beyond the capability of the solver. When they fail, they
+generally return ``unknown'' or reach a ``timeout''. In such a case, it may be
+hard to know why. Reading verification conditions can sometimes be helpful, but
+it requires a bit of practice to be efficient. Exploring the proof with the
+Coq Proof Assistant can also help, but one must be familiar with this tool, and
+the encoding of the C semantics often makes the proof context hard to read.
+
+In some situations, automatic solvers can be a better help. When they return a
+timeout, we cannot really have more information, but when they return
+``unknown'', some solvers are able to produce counter-examples provided that we
+ask them to do so.  By default, WP does not enable this behavior since it may
+reduce proof performances, but it can be enabled with the option 
+\CodeInline{-wp-counter-examples}. Not all solvers can provide counter-examples,
+but for example the CVC5 prover produces counter-examples that can be used to
+understand proof failures. Let us run again Frama-C on our example with the
+following options:
+\begin{CodeBlock}{shell}
+frama-c abs.c -wp -wp-rte -wp-counter-examples -wp-prover alt-ergo,cvc5
+\end{CodeBlock}
+
+
+Let us analyze this command line:
+\begin{itemize}
+  \item we have seen \CodeInline{-wp} and \CodeInline{-wp-rte}, they
+        respectively enable the WP plug-in and the runtime error analysis,
+  \item \CodeInline{-wp-counter-examples} enables counter-examples requests,
+  \item \CodeInline{-wp-prover alt-ergo,cvc5} tells to WP to run both Alt-Ergo
+        and CVC5 on all verification conditions.
+\end{itemize}
+
 
-When automatic solvers cannot ensure that our properties are verified,
-it is sometimes hard to understand why. Indeed, provers are generally
-not able to answer something other than ``yes'', ``no'' or ``unknown'',
-they are not able to extract the reason of a ``no'' or an ``unknown''.
-There exist tools that can explore a proof tree to extract this kind of
-information, currently Frama-C does not provide such a tool. Reading
-verification conditions can sometimes be helpful, but it requires a bit of
-practice to be efficient. Finally, one of the best way to understand the reason
-why a proof fails is to try to do it interactively with Coq. However, it
-requires one to be quite comfortable with this language to be able to understand
-the verification conditions generated by WP, since these conditions
-need to encode some elements of the C semantics that can make them quite
-hard to read.
+Using this command line, we get:
 
+\image{1-abs-2-counter-example}
 
 
-If we go back to our view of the verification conditions (see the 
-button highlighted with a red square in the previous screenshot),
-we can see that our hypotheses are not
-sufficient to determine that the property ``absence of overflow'' is true (and
-as our program stands, overflow is indeed possible), so we need to
-add some hypotheses to
-guarantee that our function will be well-behaved: a precondition.
+In this screenshot (be sure to toggle on the CE selector), we see that for the
+\textit{Probe} \CodeInline{val}, which represents the input of the function,
+CVC5 has determined that if we set it to -2147483648 (\CodeInline{INT\_MIN}),
+we have a counter example to the property ``absence of overflow''. And indeed,
+we previously said that the property cannot be proved precisely because it is
+not possible for the value \CodeInline{INT\_MIN}. We need to add some hypotheses
+to guarantee that our function will behave correctly: a precondition.
 
 
 

english/function-contract/well-specified.tex

@@ -399,16 +399,19 @@
 of RTEs for this example), we get the following result:
 
 
-
 \image{2-incr_a_by_b-1}
 
 
-The reason is simply that we do not have any guarantee that the pointer
-\CodeInline{a} is different from the pointer \CodeInline{b}. Now, if these
-pointers are the same,
+Again, counter examples can help us understand the reason why the proof fails:
+
 
+\image{incr_a_by_b-counter-example}
 
 
+The SMT solver indicates that if we take the same value for the two input
+pointers, then the property is necessarily wrong, and indeed we do not have any
+guarantee that the pointer \CodeInline{a} is different from the pointer
+\CodeInline{b}. Now, if these pointers are the same,
 \begin{itemize}
 \item   the property \CodeInline{*a == \textbackslash{}old(*a) + *b} in fact
   means \CodeInline{*a == \textbackslash{}old(*a) + *a} which can only

french/function-contract/contract.tex

@@ -421,31 +421,61 @@
 pas appel aux prouveurs.
 
 
+Souvent, les prouveurs automatiques ne donnent pas beaucoup d'information après
+avoir tenté une preuve. Quand ils arrivent à prouver la condition de vérification,
+la réponse est « oui », ce qui est suffisant puisque nous n'avons généralement
+pas besoin de plus d'information. Mais ils peuvent échouer, soit parce que la
+propriété ne peut pas être prouvée (parce qu'il manque une hypothèse ou parce
+que la propriété est simplement fausse) ou parce que la preuve est au-delà des
+capacités du prouveur. Quand ils échouent, ils retournent généralement « inconnu »
+ou atteignent un \textit{timeout}. Dans un tel cas, il peut être difficile de
+savoir pourquoi. Dans ce cas, lire la condition de vérification générée peut 
+aider, mais cela demande un peu de pratique pour devenir vraiment efficace. 
+Explorer la preuve avec l'Assistant de Preuve Coq peut aider, mais il faut être
+familier de cet outil, et l'encodage de la sémantique du C peut rendre le
+contexte de preuve difficile à lire et manipuler.
+
+Dans certaines situations, les prouveurs peuvent être une meilleure aide. Quand
+ils atteignent un \textit{timeout}, on ne peut pas vraiment avoir mieux, mais
+quand ils produisent le résultat « inconnu », certains prouveurs peuvent
+produire des contre-exemples à condition de leur demander. Par défaut, WP
+n'active pas ce comportement, car il peut réduire les performances de la preuve,
+mais cela peut être activé à l'aide de l'option 
+\CodeInline{-wp-counter-examples}. Tous les prouveurs ne peuvent pas fournir des
+contre-exemples, mais CVC5 peut par exemple produire des contre-exemples qui
+peuvent être utilisées pour comprendre des échecs de preuve. Lançons à nouveau
+Frama-C sur notre exemple avec les options suivantes :
+\begin{CodeBlock}{shell}
+frama-c abs.c -wp -wp-rte -wp-counter-examples -wp-prover alt-ergo,cvc5
+\end{CodeBlock}
+
+
+Analysons cette ligne de commande :
+\begin{itemize}
+  \item nous avons vu les options \CodeInline{-wp} et \CodeInline{-wp-rte}, qui
+        permettent respectivement d'activer le greffon WP et la vérification
+        d'absence d'erreurs à l'exécution,
+  \item \CodeInline{-wp-counter-examples} active la génération des
+        contre-exemples,
+  \item \CodeInline{-wp-prover alt-ergo,cvc5} demande à WP de lancer à la fois
+        Alt-Ergo et CVC5 sur chaque condition de vérification.
+\end{itemize}
+
+
+En utilisant cette ligne de commande, nous obtenons le résultat suivant :
+
+
+\image{1-abs-2-counter-example}
+
 
-Lorsque les prouveurs automatiques ne parviennent pas à assurer que nos
-propriétés sont bien vérifiées, il est parfois difficile de comprendre
-pourquoi. En effet, les prouveurs sont généralement incapables de nous
-répondre autre chose que « oui », « non » ou « inconnu », ils ne sont pas
-capables d'extraire le « pourquoi » d'un « non » ou d'un « inconnu ». Il
-existe des outils qui
-sont capables d'explorer les arbres de preuve pour en extraire ce type
-d'information, Frama-C n'en possède pas à l'heure actuelle. La lecture des
-conditions de vérification peut parfois nous aider, mais cela demande un peu
-d'habitude pour pouvoir les déchiffrer facilement. Finalement, le meilleur
-moyen de comprendre la raison d'un échec est d'effectuer la preuve de manière
-interactive avec Coq. En revanche, il faut déjà avoir une certaine habitude de
-ce langage pour ne pas être perdu devant les conditions de vérification générées par
-WP, étant donné que celles-ci encodent les éléments de la sémantique de C, ce
-qui rend le code souvent indigeste.
-
-
-
-Si nous retournons dans notre tableau des conditions de vérification (bouton
-encadré en rouge dans la capture d'écran précédente), nous pouvons donc voir
-que les hypothèses n'ont pas suffi aux prouveurs pour déterminer que la
-propriété  « absence de débordement » est vraie (et nous l'avons dit : c'est
-normal), il nous faut donc ajouter une hypothèse supplémentaire pour garantir
-le bon fonctionnement de la fonction : une précondition d'appel.
+Sur cette capture d'écran (il faut bien activer le sélecteur CE), nous voyons
+que le \textit{Prove} \CodeInline{val}, qui représente la valeur d'entrée de la
+fonction, CVC5 a déterminé que si nous plaçons cette valeur à -2147483648
+(\CodeInline{INT\_MIN}), nous avons un contre-exemple à la propriété
+« absence de débordement ». Et effectivement, nous avons dit précédemment que
+cette propriété ne peut pas être prouvée pour la valeur \CodeInline{INT\_MIN}.
+Il nous faut donc ajouter une hypothèse supplémentaire pour garantir le bon
+fonctionnement de la fonction : une précondition d'appel.
 
 
 

french/function-contract/well-specified.tex

@@ -415,11 +415,17 @@
 \image{2-incr_a_by_b-1}
 
 
-La raison est simplement que rien ne garantit que le pointeur \CodeInline{a} est bien
-différent du pointeur \CodeInline{b}. Or, si les pointeurs sont égaux,
+À nouveau, les contre-exemples peuvent nous aider à comprendre la raison de
+l'échec de preuve :
 
 
+\image{incr_a_by_b-counter-example}
 
+
+Le prouveur automatique nous indique que si nous prenons la même valeur pour les
+deux pointeurs d'entrée, la propriété est nécessairement fausse, et effectivement
+rien ne garantit que le pointeur \CodeInline{a} est bien différent du pointeur
+\CodeInline{b}. Or, si les pointeurs sont égaux,
 \begin{itemize}
 \item la propriété \CodeInline{*a == \textbackslash{}old(*a) + *b} signifie en fait
 \CodeInline{*a == \textbackslash{}old(*a) + *a}, ce qui ne peut être vrai que si l'ancienne valeur
@@ -497,7 +503,7 @@
 la fonction valeur absolue n'a, au fond, pas  vraiment de précondition à
 satisfaire : c'est la machine cible qui détermine qu'une condition supplémentaire
 doit être vérifiée en raison du complément à deux. Comme nous le verrons dans le
-chapitre \ref{l1:proof-methodologies}, vérifier l'absence de \emph{runtime-errors}
+chapitre \ref{l1:proof-methodologies}, vérifier l'absence de \textit{runtime-errors}
 peut aussi impacter nos postconditions, pour l'instant laissons cela de côté.