WIP, part one Done and part 2 most done

content/conception_formelle/99-DM_framac/TD-TP.tex

@@ -190,12 +190,19 @@ int abs2(int n)
             & \equiv && \top \\
         \end{alignat*}
 
+        Grâce au calcul $n \% 2 + (n + 1) \% 2$ nous obtiendrons 1 si \code{n} est positif et -1 sinon. Attention dans certain langages le modulo 2 d'un nombre négatif impair donne 1 et non pas -1, ce résultat est mathématiquement correct. C'est le cas de Python par exemple.
+
+        Nous pouvons en déduire le triplet de Hoare suivant:
+
+        $\{\forall n \in \Z\} \text{ abs } \{\result \leftarrow abs(n)\}$
     \end{solutionorbox}
 
+
     \part Quelle préconditions faut-il pour ne pas avoir de comportement indéterminé ? Justifiez.
 
     \begin{solutionorbox}
-        Comme pour \code{abs}, nous devons prendre en compte les limites du processeur, mais cette fois \code{n} devra être comprise entre 0 et \code{INT_MAX}.
+
+        Notre calcul de \textit{weakest precondition} ci-dessus ne prend pas en compte les limites de notre processeur sur la taille des variables. Ici nous devons nous assurer que le resultat du calcul $n * (n \% 2 + (n + 1)\%2$ soit compris entre \code{INT_MAX et INT_MIN}.
     \end{solutionorbox}
 
     \part Compléter le fichier \texttt{abs.h} de manière à ce que Frama-C puisse démontrer la post-condition fournie, en ajoutant les assertions RTE. Il est bien évidemment possible (et encouragé) de répondre aux questions précédentes grâce à celle-ci.
@@ -237,14 +244,21 @@ int abs2(int n)
     \part Quelle condition doit-être vraie à la sortie de la boucle (i.e, $\WLP(18,\psi))$, pour $\psi$ la post-condition ?
 
     \begin{solutionorbox}
-        METTEZ VOTRE RÉPONSE ICI.
+        La condition $min \le max$ doit être vérifiée à la sortie de la boucle
     \end{solutionorbox}
 
     \part Calculez $\WLP(12-16,I)$ pour un invariant I quelconque.
     Mettez-la en forme de manière à avoir la conjonction de 4 implications (en appliquant que $P \Rightarrow (Q\wedge R)$ est équivalent à $(P \Rightarrow Q) \wedge (P \Rightarrow R)$, et $P \Rightarrow Q \Rightarrow R$ est équivalent à $(P\wedge Q) \Rightarrow R$).
 
     \begin{solutionorbox}
-        METTEZ VOTRE RÉPONSE ICI.
+        \begin{alignat*}{3}
+            \WLP(12-16,I) & \equiv && \WLP(12-13,\WLP(14-15,\psi)) \\
+            & \equiv && \WLP(12-13, i < n \wedge tab[i] < min \implies [tab[i] \leftarrow min ]) \\
+            & \equiv && ( i < n \wedge tab[i] < min \implies [  min \leftarrow tab[i] ] ) \\
+            & &&\vee ( i < n \wedge tab[i] > max \implies [ max \leftarrow tab[i] ] ) \\
+            & \equiv && ( i < n \implies tab[i] < min \implies [  min \leftarrow tab[i] ] ) \\
+            & &&\vee ( i < n \implies tab[i] > max \implies [ max \leftarrow tab[i] ] ) \\
+        \end{alignat*}
     \end{solutionorbox}
 
     \part Proposez des invariants de boucle pour votre boucle.
@@ -266,31 +280,56 @@ int abs2(int n)
     Pour chacun des invariants, comme elles sont similaires, vous pouvez n’expliquer qu’une seule des quatre implications
 
     \begin{solutionorbox}
-        METTEZ VOTRE RÉPONSE ICI.
+        loop invariant $I_1$: $1 \le i < n;$ \\
+        loop invariant $I_2$: $min \le max;$ \\
+        loop invariant $I_3$: $\forall j; (0 \le j \le i \implies max \ge tab[j] \ge min) $ \\
+        loop invariant $I_4$: $\forall j \in \mathbb{N} \exists j, 0 \le j \le i \implies tab[j] == min $ \\
+        loop invariant $I_5$: $\forall j \in \mathbb{N} \exists j, 0 \le j \le i \implies tab[j] == max $ \\
+
+        Pour notre invariant $I_2$, les deux éléments dont égaux au départ (ils sont égaux à $tab[0]$),d'où le signe $\le$. Il est aussi tout à fait possible que tous les éléments du tableaux soient égaux, dans ce cas aussi max et min seront égaux.
+
+        Pour les invariants $I_4$ et $I_5$, la logique est la même: il existe un entier naturel $j$ compris entre 0 et $i$ pour llequel $tab[j] == min$. 
     \end{solutionorbox}
 
     \part Déduisez-en un triplet de \bsc{Hoare} valide pour votre fonction.
 
     \begin{solutionorbox}
-        METTEZ VOTRE RÉPONSE ICI.
+        $\{n > 0\}max\_dist\{min \le max\}$
     \end{solutionorbox}
 
     \part Démontrez la terminaison de la fonction en donnant un variant de boucle et en démontrant qu’il décroît à chaque tour de boucle et qu’il est toujours positif (vous pouvez utiliser le calcul de la question b).
 
     \begin{solutionorbox}
-        METTEZ VOTRE RÉPONSE ICI.
+        \begin{alignat*}{3}
+            \WLP(12-16,n-i < at(n - i,12) & \equiv && n - (i + 1) < at(n - i, 12) \\
+            & \equiv && n - i - 1) < n - i \\
+            & \equiv && - 1 < 0 \\
+            & \equiv && \top
+        \end{alignat*}
     \end{solutionorbox}
 
     \part Quelles sont les valeurs mémoires modifiées par cette fonction (et la boucle) ? Vous répondrez en donnant les clauses assigns et loop assigns correspondantes.
 
     \begin{solutionorbox}
-        METTEZ VOTRE RÉPONSE ICI.
+
+        Cette fonction ne nécessite pas de clause \code{assign}, par contre la boucle en nécessite 3 :
+
+        \begin{lstlisting}
+        /*@
+          loop assign i, min, max;
+        */
+        \end{lstlisting}
     \end{solutionorbox}
 
     \part Que manque-t’il comme précondition pour que la fonction ne puisse pas faire d’erreur à l’exécution ?
 
     \begin{solutionorbox}
-        METTEZ VOTRE RÉPONSE ICI.
+        Il faut s'assurer :
+
+        \begin{itemize}
+            \item $0 < n \le INT_MAX $
+            \item les éléments du tableaux existent de 0 à $n - 1 $
+        \end{itemize}
     \end{solutionorbox}
 
     \part Démontrez que la fonction suivante vérifie le même contrat de fonction :