New content: WP vs Disjkstra WP

code/statements/basic/wp-plugin-calculus-toy.c

@@ -0,0 +1,29 @@
+/* run.config
+  DONTRUN:
+*/
+
+int x ;
+int y ;
+
+// 8.
+/*@ requires P(x) ;
+    ensures P(x) ;
+    ensures P(y) ;
+*/
+void toy(void){
+  // 7.
+  if(x > 0){
+    // 6.
+    x ++ ;
+    // 5.
+    //@ assert Q(x);
+  } else {
+    // 4.
+    y ++ ;
+    // 3.
+    //@ check Q(y);
+  }
+  // 2.
+  x = x * y ;
+  // 1.
+}

english/statements/basic.tex

@@ -713,6 +713,134 @@
 Section~\ref{l2:acsl-logic-definitions-axiomatic}).
 
 
+\levelThreeTitle{WP plugin vs. Dijkstra's WP calculus}
+
+
+One might have notice from the beginning of this section that the $wp$ function
+starts from the postcondition and, instruction after instruction, changes the
+formula until it reaches the beginning of the function, when it generates the
+verification condition (as briefly explained in
+Section~\ref{l3:statements-basic-consequence}), that we must verify.
+
+
+However, one might have also noticed that from the very beginning of this book,
+in most examples, we do not have \emph{one} verification condition to verify,
+but \emph{several}. On a theoretical aspect, this is not a crucial difference,
+but on a practical aspect, it allows generating simpler verification conditions,
+thus easier to verify using SMT solvers.
+
+
+In fact, the WP plugin generates several verification conditions in parallel
+during the WP calculus. Each time it meets a new instruction, the $wp$ function
+is applied for this instruction on all verification conditions involved in the
+program path the instruction belongs to (to guarantee this, the conditional
+rule is also handled slightly differently, but we will not detail this aspect).
+However, when this step includes the proof of a property (for example, an
+\CodeInline{assert} annotation), instead of applying the rule by adding it as a
+conjunction, it is simply added separately to the set of verification conditions
+to prove. Intuitively: we start a new weakest precondition calculus in parallel
+from this program point.
+
+
+Let us illustrate this on a toy example:
+
+
+\CodeBlockInput{c}{wp-plugin-calculus-toy.c}
+
+
+We start (in 1) with two verification conditions:
+\begin{itemize}
+  \item \CodeInline{VC1: P(x)},
+  \item \CodeInline{VC2: P(y)}.
+\end{itemize}
+We apply the transformer of assignment on each of them, thus we reach 2 with:
+\begin{itemize}
+  \item \CodeInline{VC1: P(x * y)},
+  \item \CodeInline{VC2: P(y)}.
+\end{itemize}
+In 2, we have to deal with the conditional. Instead of directly applying the
+standard WP rule, we split the analysis in two sets of verification conditions,
+initially equivalent. Let us consider the \CodeInline{else} branch, then the
+\CodeInline{then} branch.
+
+
+From 2 to 3, we meet the \CodeInline{check} annotation, thus we add a new
+verification condition, we get the set:
+\begin{itemize}
+  \item \CodeInline{VC1: P(x * y)},
+  \item \CodeInline{VC2: P(y)},
+  \item \CodeInline{VC3: Q(y)}.
+\end{itemize}
+Then, we apply the assignment rule, and we get in 4:
+\begin{itemize}
+  \item \CodeInline{VC1: P(x * (y+1))},
+  \item \CodeInline{VC2: P(y+1)},
+  \item \CodeInline{VC3: Q(y+1)}.
+\end{itemize}
+
+
+From 2 to 5, we meet the \CodeInline{assert} annotation, thus we add this
+knowledge to all verification conditions, and we create a new one:
+\begin{itemize}
+  \item \CodeInline{VC1: Q(x) ==> P(x * y)},
+  \item \CodeInline{VC2: Q(x) ==> P(y)},
+  \item \CodeInline{VC4: Q(x)}.
+\end{itemize}
+Then we apply the assignment rule, and we get in 6:
+\begin{itemize}
+  \item \CodeInline{VC1: Q(x+1) ==> P((x+1) * y)},
+  \item \CodeInline{VC2: Q(x+1) ==> P(y)},
+  \item \CodeInline{VC4: Q(x+1)}.
+\end{itemize}
+
+
+Now we have to reconcile the two sets. Let us not enter into the details (just
+notice the introduced primed variables, the trick is here) of how it is done, we
+get, in 7, something like:
+\begin{CodeBlock}{text}
+  VC1:
+    ((x <= 0 ==> y' == y+1 && x' == x) &&
+     (x >  0 ==> y' == y   && x' == x+1 && Q(x+1))) ==>
+       P(x' * y')
+
+  VC2:
+    ((x <= 0 ==> y' == y+1) &&
+     (x >  0 ==> y' == y    && Q(x+1))) ==>
+       P(y')
+  VC3:
+    (x <= 0) ==> Q(x+1)
+
+  VC4:
+    (x >  0) ==> Q(x+1)
+\end{CodeBlock}
+
+
+Finally, we meet the precondition, and we obtain in 8:
+\begin{CodeBlock}{text}
+  VC1:
+    P(x) ==>
+      ((x <= 0 ==> y' == y+1 && x' == x) &&
+       (x >  0 ==> y' == y   && x' == x+1 && Q(x+1))) ==>
+         P(x' * y')
+
+  VC2:
+    P(x) ==>
+      ((x <= 0 ==> y' == y+1) &&
+       (x >  0 ==> y' == y    && Q(x+1))) ==>
+         P(y')
+  VC3:
+    P(x) ==> (x <= 0) ==> Q(x+1)
+
+  VC4:
+    P(x) ==> (x >  0) ==> Q(x+1)
+\end{CodeBlock}
+
+
+We can see that for each property that must be proved, we have built a separate
+verification condition that gathers the knowledge available along the path that
+leads to the program point where its verification is asked.
+
+
 \levelThreeTitle{Exercises}
 
 

french/statements/basic.tex

@@ -744,6 +744,140 @@
 (nous parlerons des axiomes dans la section~\ref{l2:acsl-logic-definitions-axiomatic}).
 
 
+\levelThreeTitle{WP plugin vs. WP calculus de Dijkstra}
+
+
+Depuis le début de cette section, nous avons vu que la fonction $wp$ démarre
+depuis la postcondition et, instruction après instruction, change la formule
+jusqu'à atteindre le début de la fonction, où elle génère la condition de
+vérification (comme brièvement expliqué dans la
+section~\ref{l3:statements-basic-consequence}), que nous devons vérifier.
+
+
+Ceci dit, le lecteur attentif aura peut-être également remarqué que depuis le
+début de ce livre, dans la plupart des exemples, nous n'avons pas \textit{une}
+condition de vérification à vérifier, mais \textit{plusieurs}. Sur un aspect
+théorique, cela ne fait pas grande différence, mais d'un point de vue pratique,
+cela permet de générer des conditions de vérification plus simples à vérifier
+pour les solveurs SMT.
+
+
+En fait, le greffon WP génère plusieurs conditions de vérifications en parallèle
+pendant le calcul de WP. À chaque fois qu'il rencontre une nouvelle instruction,
+la fonction $wp$ est appliqué pour cette instruction sur toutes les conditions
+de vérifications rencontrées sur le chemin de programme auquel l'instruction
+appartient (pour garantir cela, la règle de la conditionnelle est sensiblement
+différente de ce que nous avons présentés, mais nous n'entrerons pas dans ces
+détails). Cependant, quand cette étape inclut la preuve d'une propriété (par
+exemple, une assertion), au lieu d'appliquer la règle en l'ajoutant comme une
+conjonction, elle est simplement ajoutée à l'ensemble des conditions de
+vérification à prouver. Intuitivement : nous commençons un nouveau calcul de plus
+faible précondition en parallèle à partir de ce point de programme.
+
+
+Illustrons cela sur cet exemple jouet :
+
+
+\CodeBlockInput{c}{wp-plugin-calculus-toy.c}
+
+
+Nous commençons (en 1) avec deux conditions de vérification :
+\begin{itemize}
+  \item \CodeInline{VC1: P(x)},
+  \item \CodeInline{VC2: P(y)}.
+\end{itemize}
+Nous appliquons la règle que l'affectation sur chacune d'elle, et nous atteignons
+2 avec :
+\begin{itemize}
+  \item \CodeInline{VC1: P(x * y)},
+  \item \CodeInline{VC2: P(y)}.
+\end{itemize}
+En 2, nous devons traiter la conditionnelle. Au lieu de directement appliquer
+la règle standard de WP, nous séparons l'analyse en deux ensembles de conditions
+de vérification, initialement équivalents. Considérons d'abord la branche
+\CodeInline{else} puis la branche \CodeInline{then}.
+
+
+De 2 à 3, nous rencontrons une annotation \CodeInline{check}, donc nous ajoutons
+une nouvelle condition de vérification et nous obtenons l'ensemble :
+\begin{itemize}
+  \item \CodeInline{VC1: P(x * y)},
+  \item \CodeInline{VC2: P(y)},
+  \item \CodeInline{VC3: Q(y)}.
+\end{itemize}
+Ensuite, nous appliquons la règle de l'affectation, et nous obtenons en 4 :
+\begin{itemize}
+  \item \CodeInline{VC1: P(x * (y+1))},
+  \item \CodeInline{VC2: P(y+1)},
+  \item \CodeInline{VC3: Q(y+1)}.
+\end{itemize}
+
+
+De 2 à 5, nous rencontrons une annotation \CodeInline{assert}, nous ajoutons
+donc cette connaissance à toutes les conditions de vérification, et nous en
+créons une nouvelle :
+\begin{itemize}
+  \item \CodeInline{VC1: Q(x) ==> P(x * y)},
+  \item \CodeInline{VC2: Q(x) ==> P(y)},
+  \item \CodeInline{VC4: Q(x)}.
+\end{itemize}
+Ensuite, nous appliquons la règle de l'affectation et nous obtenons en 6 :
+\begin{itemize}
+  \item \CodeInline{VC1: Q(x+1) ==> P((x+1) * y)},
+  \item \CodeInline{VC2: Q(x+1) ==> P(y)},
+  \item \CodeInline{VC4: Q(x+1)}.
+\end{itemize}
+
+
+Maintenant, nous devons réconcilier les deux ensembles. Nous omettons certains
+détails ici (l'astuce se trouve dans les variables $v'$ qui sont introduites et
+qui permettent de séparer les valeurs en fonction de la condition), et nous
+obtenons en 7, quelque chose comme :
+\begin{CodeBlock}{text}
+  VC1:
+    ((x <= 0 ==> y' == y+1 && x' == x) &&
+     (x >  0 ==> y' == y   && x' == x+1 && Q(x+1))) ==>
+       P(x' * y')
+
+  VC2:
+    ((x <= 0 ==> y' == y+1) &&
+     (x >  0 ==> y' == y    && Q(x+1))) ==>
+       P(y')
+  VC3:
+    (x <= 0) ==> Q(x+1)
+
+  VC4:
+    (x >  0) ==> Q(x+1)
+\end{CodeBlock}
+
+
+Finalement, nous atteignons la précondition, et nous obtenons en 8 :
+\begin{CodeBlock}{text}
+  VC1:
+    P(x) ==>
+      ((x <= 0 ==> y' == y+1 && x' == x) &&
+       (x >  0 ==> y' == y   && x' == x+1 && Q(x+1))) ==>
+         P(x' * y')
+
+  VC2:
+    P(x) ==>
+      ((x <= 0 ==> y' == y+1) &&
+       (x >  0 ==> y' == y    && Q(x+1))) ==>
+         P(y')
+  VC3:
+    P(x) ==> (x <= 0) ==> Q(x+1)
+
+  VC4:
+    P(x) ==> (x >  0) ==> Q(x+1)
+\end{CodeBlock}
+
+
+Nous pouvons voir que pour chaque propriété que nous devons prouver, nous avons
+construit une condition de vérification spécifique qui rassemble la connaissance
+disponible le long du chemin de programme qui atteint le point où la vérification
+est demandée.
+
+
 \levelThreeTitle{Exercices}