diff --git a/content/conception_formelle/99-DM_framac/Makefile b/content/conception_formelle/99-DM_framac/Makefile index 5ec72c0..3603ec3 100644 --- a/content/conception_formelle/99-DM_framac/Makefile +++ b/content/conception_formelle/99-DM_framac/Makefile @@ -44,6 +44,6 @@ framac: --volume=./code/:/data \ --userns "keep-id:uid=9000,gid=9000" \ -e DISPLAY=$$DISPLAY \ - --entrypoint=/bin/bash framac + framac .PHONY: echo view clean build-container framac diff --git a/content/conception_formelle/99-DM_framac/TD-TP.tex b/content/conception_formelle/99-DM_framac/TD-TP.tex index 4459200..2c60673 100644 --- a/content/conception_formelle/99-DM_framac/TD-TP.tex +++ b/content/conception_formelle/99-DM_framac/TD-TP.tex @@ -50,7 +50,7 @@ Pour répondre aux questions, vous avez deux choix : \item Soit compléter le présent document .tex en plaçant vos réponses dans les blocs solutionorbox prévues à cet effet. Pour cela, référez-vous aux macros définies dans les sujets de TD. Si vous avez besoin de compiler avec la police OpenDyslexic, faites-le avec la ligne suivante : \verb#latexmk -xelatex -usepretex='\def\dyslexic{}' TD-TP.tex# - \item Soit produire un document pdf par d’autres moyens (autre logiciel, scan), tant que c’est lisible, ça me conviendra. +\item Soit produire un document pdf par d’autres moyens (autre logiciel, scan), tant que c’est lisible, ça me conviendra. \end{itemize} Vous devrez rendre (sur la page moodle du cours) : @@ -283,8 +283,8 @@ int abs2(int n) 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 $ \\ + loop invariant $I_4$: $\exists j \in \mathbb{N}; 0 \le j \le i \implies tab[j] == min $ \\ + loop invariant $I_5$: $\exists j \in \mathbb{N}; 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. @@ -314,7 +314,7 @@ int abs2(int n) Cette fonction ne nécessite pas de clause \code{assign}, par contre la boucle en nécessite 3 : - \begin{lstlisting} + \begin{lstlisting}[numbers=none] /*@ loop assign i, min, max; */ @@ -332,6 +332,7 @@ int abs2(int n) \begin{itemize} \item $0 < n \le INT_MAX $ \item les éléments du tableaux existent de 0 à $n - 1 $ + \item les éléments du tableaux sont compris entre \code{INT_MIN / 2} et \code{INT_MAX / 2}. Réduite le domaine des variables permet de s'assurer que le retour de la fonction ne provoquera pas un overflow. Il aurait été possible de ne prendre que les enier positifs ou negatifs. \end{itemize} \end{solutionorbox} @@ -346,8 +347,8 @@ int max_dist(int *tab, unsigned int n) \begin{solutionorbox} - Cette fonction incorrecte prend en paramètre deux éléments -- un tableau et un entier positif -- et en retrourne un -- un entier. C'est exactement la même chose que pour notre fonction correcte. Le contrat s'écrirait alors comme ci-dessous pour Frama-C : - \begin{lstlisting} + Cette fonction incorrecte prend en paramètre deux éléments -- un tableau et un entier positif -- et retrourne une entier. C'est exactement la même chose que pour notre fonction correcte. Le contrat s'écrirait alors comme ci-dessous pour Frama-C : + \begin{lstlisting}[numbers=none] \*@ require 0 < n <= UINT_MAX; require \valid(tab+(0..n-1)); @@ -359,9 +360,14 @@ int max_dist(int *tab, unsigned int n) \part Donnez une postcondition vérifiée par la fonction correcte qui n’est pas vérifiée par celle-ci. Vos invariants devraient permettre de la vérifier (si vous l’écrivez sans valeur absolue). - \begin{solutionorbox} - + \begin{lstlisting}[numbers=none] + /*@ + ensures \exists integer i,j; 0 <= i <= j < n ==> \result == abs(tab[i]-tab[j]); + */ + + La valeur retrournée par notre fonction correcte provient de la différence entre deux élements du tableau. + \end{lstlisting} \end{solutionorbox} @@ -412,31 +418,70 @@ int min_dist(int *tab, unsigned int n) \part Quelle condition doit-être vraie à la sortie de la boucle extérieure (i.e, $\WLP(23,\psi))$, pour $\psi$ la post-condition ? \begin{solutionorbox} - METTEZ VOTRE RÉPONSE ICI. + \begin{alignat*} + \forall integer i,j; 0 \le i < j < n - 1 \implies min >= abs(tab[i]-tab[j]) + \end{alignat*} \end{solutionorbox} \part Calculez $\WLP(14-17,J)$ pour un invariant J quelconque. \begin{solutionorbox} - METTEZ VOTRE RÉPONSE ICI. + \begin{alignat*}{3} + \WLP(14-17,J) & \equiv && \WLP(14-16,J) \\ + & \equiv && abs(tab[i] - tab[j]) < min\_i \implies \WLP(16,J) \\ + & && \wedge \lnot (abs(tab[i] - tab[j])) < min\_i \implies J \\ + & \equiv && (abs(tab[i] - tab[j])) < min\_i \\ + & && \implies min\_i \leftarrow abs(tab[i] - tab[j]) \implies J \\ + & && \wedge \lnot (abs(tab[i] - tab[j])) < min\_i \implies J \\ + \end{alignat*} \end{solutionorbox} \part Calculez $\WLP(19-21,I)$ pour un invariant I quelconque (pour déterminer ce qui doit être vrai à la sortie de la boucle interne, en fonction de I). \begin{solutionorbox} - METTEZ VOTRE RÉPONSE ICI. + \begin{alignat*}{3} + \WLP(19-21,I) & \equiv && \WLP(19-20,\WLP(21,I)) \\ + & \equiv && min\_i < min \implies min \leftarrow min\_i \implies I\\ + & && \wedge \lnot (min\_i < min ) \implies I + \end{alignat*} \end{solutionorbox} \part Calculez $\WLP(10-21,I)$ pour un invariant I quelconque, en admettant que l’invariant de la boucle interne (14-17) est J. \begin{solutionorbox} - METTEZ VOTRE RÉPONSE ICI. + \begin{alignat*}{3} + \WLP(10-21,I) & \equiv && \WLP(14-17,\WLP(19-21,J)) \\ + & && \implies min\_i \leftarrow abs(tab[i] - tab[j]) \implies J) \\ + & && \wedge \lnot (abs(tab[i] - tab[j])) < min\_i \implies J \\ + \end{alignat*} \end{solutionorbox} \part Donnez les clauses loop assigns et assigns pour cette fonction. \begin{solutionorbox} - METTEZ VOTRE RÉPONSE ICI. + Comme pour la fonction \code{max_dist()}, celle-ci ne nécessite pas d'\texttt{assigns} : aucun élément non-local n'est modifié. + + Pour la première boucle : + \begin{lstlisting}[numbers=none] + /*@ + loop assigns min, i; + */ + while(i < n - 1) + { + // [...] + } + \end{lstlisting} + + Pour la seconde + \begin{lstlisting}[numbers=none] + /*@ + loop assigns j, min, min_i; + */ + while(i < n - 1) + { + // [...] + } + \end{lstlisting} \end{solutionorbox} \part Proposez des invariants pour les deux boucles -- on ne vous demande pas de démontrer la correction sur papier, mais uniquement de vérifier avec frama-c que vos invariants en sont et sont suffisants. @@ -453,7 +498,14 @@ int min_dist(int *tab, unsigned int n) \end{itemize} \begin{solutionorbox} - METTEZ VOTRE RÉPONSE ICI. + \begin{lstlisting}[numbers=none] + loop invariant I1: \at(i, LoopEntry) <= i < n - 1; + loop invariant I2: ; + \end{lstlisting} + \begin{lstlisting}[numbers=none] + loop invariant J1: \at(j, LoopEntry) <= j < n; + loop invariant J2: \exists integer k; k == n && \at(min_i, LoopCurrent) >= min_i; + \end{lstlisting} \end{solutionorbox} \part Déterminez les pré-conditions qui permettent de démontrer ce contrat de fonction et que les gardes RTE sont satisfaites. @@ -465,14 +517,25 @@ int min_dist(int *tab, unsigned int n) \part Démontrez la terminaison de la fonction en donnant un variant de boucle pour chaque boucle et en démontrant qu’ils décroissent à chaque tour de boucle et qu’ils sont toujours positifs (vous pouvez utiliser les calculs des questions précédentes). \begin{solutionorbox} - METTEZ VOTRE RÉPONSE ICI. + \begin{alignat*}{3} + \WLP(8-22,n-i < at(n - i,12) & && \\ + \wedge j-n < at(n - i,15) & \equiv && n - (i + 1) < at(n - i, 12) \wedge j-n < at(n - i,15)\\ + & \equiv && (n - i - 1) < n - i \wedge n - j - 1 < n - j \\ + & \equiv && - 1 < 0 \wedge -1 < 0\\ + & \equiv && \top \wedge \top + \end{alignat*} \end{solutionorbox} \part Trouvez une fonction très simple (d’une instruction) qui satisfait le même contrat de fonction. \begin{solutionorbox} - METTEZ VOTRE RÉPONSE ICI. + \begin{lstlisting}[numbers=none] + int min_dist(int *ta, unsigned int n) + { + return 0 + } + \end{lstlisting} \end{solutionorbox} \part Donnez une postcondition vérifiée par la fonction correcte qui n’est pas vérifiée par celle-ci. diff --git a/content/conception_formelle/99-DM_framac/code/max_dist.c b/content/conception_formelle/99-DM_framac/code/max_dist.c index a72525e..1f86b97 100644 --- a/content/conception_formelle/99-DM_framac/code/max_dist.c +++ b/content/conception_formelle/99-DM_framac/code/max_dist.c @@ -9,7 +9,7 @@ int max_dist(int *tab, unsigned int n) /*@ loop assigns i, max, min; loop invariant I1: \at(i, LoopEntry) <= i <= n; - loop invariant I2: min <= max; + loop invariant I2: INT_MIN /2 <= min <= max <= INT_MAX/2; loop invariant I3: \forall integer j; (\at(i, LoopEntry) <= j < i ==> max >= tab[j] >= min); loop invariant I4: \exists integer j; ( 0 < j < i ==> max == tab[j]); loop invariant I5: \exists integer j; ( 0 < j < i ==> min == tab[j]); @@ -23,5 +23,9 @@ int max_dist(int *tab, unsigned int n) max = tab[i]; i++; } + //@ assert (INT_MIN / 2) <= min; + //@ assert min <= (INT_MAX / 2); + //@ assert (INT_MIN / 2) <= max; + //@ assert max <= (INT_MAX / 2); return max - min; } diff --git a/content/conception_formelle/99-DM_framac/code/max_dist.h b/content/conception_formelle/99-DM_framac/code/max_dist.h index eaeeb93..47ceec0 100644 --- a/content/conception_formelle/99-DM_framac/code/max_dist.h +++ b/content/conception_formelle/99-DM_framac/code/max_dist.h @@ -2,9 +2,12 @@ #include "abs.h" /*@ - requires 0 < n < UINT_MAX; + requires 0 < n <= UINT_MAX; requires \valid_read(tab+(0..n-1)); + requires \forall integer i; 0 <= i < n ==> INT_MIN / 2 <= tab[i] <= INT_MAX/2; terminates \true; ensures \forall integer a,b; 0 <= a < b < n ==> \result >= abs(tab[a]-tab[b]); + ensures \exists integer i,j; 0 < i < j < n ==> \result == abs(tab[i]-tab[j]); + assigns \nothing; */ int max_dist(int *tab, unsigned int n); diff --git a/content/conception_formelle/99-DM_framac/code/min_dist.c b/content/conception_formelle/99-DM_framac/code/min_dist.c index 61e7727..5c6389e 100644 --- a/content/conception_formelle/99-DM_framac/code/min_dist.c +++ b/content/conception_formelle/99-DM_framac/code/min_dist.c @@ -3,10 +3,21 @@ int min_dist(int *tab, unsigned int n) { int min = abs(tab[0] - tab[1]); unsigned int i = 0; + /*@ + loop invariant I1: \at(i, LoopEntry) <= i < n - 1; + loop invariant I2: \exists integer k; (k == n - 1 ==> \at(min, LoopCurrent) >= min); + loop assigns i, min; + loop variant n - i; + */ while (i < n - 1) { int min_i = abs(tab[i] - tab[i + 1]); unsigned int j = i + 2; + /*@ + loop invariant J1: \at(j, LoopEntry) <= j < n; + loop assigns i, j , min, min_i; + loop variant n - j; + */ while (j < n) { int d = abs(tab[i] - tab[j]); @@ -19,4 +30,4 @@ int min_dist(int *tab, unsigned int n) i++; } return min; -} \ No newline at end of file +} diff --git a/content/conception_formelle/99-DM_framac/code/min_dist.h b/content/conception_formelle/99-DM_framac/code/min_dist.h index e92e2d2..32eee45 100644 --- a/content/conception_formelle/99-DM_framac/code/min_dist.h +++ b/content/conception_formelle/99-DM_framac/code/min_dist.h @@ -1,6 +1,12 @@ #include -#include "abs-cor.h" +#include "abs.h" -/*@ ensures \forall integer i; 0 <= i < n ==> (\forall integer j; i < j < n ==> \result <= abs(tab[i]-tab[j])); +/*@ + requires 1 < n <= UINT_MAX; + requires \valid_read(tab+(0..n-1)); + requires \forall integer i; 0 <= i < n ==> (INT_MIN / 2 <= tab[i] <= INT_MAX/2); + terminates \true; + assigns \nothing; + ensures \forall integer i; 0 <= i < n ==> (\forall integer j; i < j < n ==> \result <= abs(tab[i]-tab[j])); */ -int min_dist(int *tab, unsigned int n); \ No newline at end of file +int min_dist(int *tab, unsigned int n); diff --git a/content/conception_formelle/99-DM_framac/code/test.c b/content/conception_formelle/99-DM_framac/code/test.c new file mode 100644 index 0000000..3ddb23f --- /dev/null +++ b/content/conception_formelle/99-DM_framac/code/test.c @@ -0,0 +1,31 @@ +#include +#include "abs.h" +/*@ + requires 0 < n < INT_MAX; + requires \valid_read(tab+(0..n-1)); + requires \forall integer a,b; 0 <= a < b < n ==> tab[a] - tab[b] <= INT_MAX; + ensures \forall integer a,b; 0 <= a < b < n ==> \result >= abs(tab[a]-tab[b]); + */ +int max_dist ( int *tab, int n) +{ + int max = tab[0]; + int min = tab[0]; + unsigned int i = 1; + /*@ + loop assigns i, max, min; + loop invariant I1: \at(i, LoopEntry) <= i <= n; + loop invariant I2: min <= max; + loop invariant I3: \forall integer j; (\at(i, LoopEntry) <= j < i ==> max >= tab[j] >= min); + loop variant n - i; + */ + + while ( i < n) + { + if ( tab[i] > max) max = tab[i]; + if ( tab[i] < min) min = tab[i]; + i++; + } + //@ assert INT_MIN <= max <= INT_MAX; + //@ assert INT_MIN <= min <= INT_MAX; + return max - min; +} diff --git a/content/conception_formelle/99-DM_framac/container/entrypoint.sh b/content/conception_formelle/99-DM_framac/container/entrypoint.sh index c86b2c7..4c753ec 100755 --- a/content/conception_formelle/99-DM_framac/container/entrypoint.sh +++ b/content/conception_formelle/99-DM_framac/container/entrypoint.sh @@ -2,4 +2,4 @@ # export DBUS_SESSION_BUS_ADDRESS=`dbus-daemon --fork --config-file=/usr/share/dbus-1/session.conf --print-address` eval $(opam env) || exit 10 -frama-c-gui +bash