ephase/cours
1
0
Fork 0
Code Issues Pull requests Releases Wiki Activity

finish Frama-C homework

Browse source
This commit is contained in:
Yorick Barbanneau 2023-05-09 21:48:51 +02:00
parent 97a81f159a
commit 0bbf6ffde1
8 changed files with 142 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

2
content/conception_formelle/99-DM_framac/Makefile
View file

@ -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

93
content/conception_formelle/99-DM_framac/TD-TP.tex
View file

@ -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.

6
content/conception_formelle/99-DM_framac/code/max_dist.c
View file

@ -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;
}

5
content/conception_formelle/99-DM_framac/code/max_dist.h
View file

@ -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);

11
content/conception_formelle/99-DM_framac/code/min_dist.c
View file

@ -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]);

10
content/conception_formelle/99-DM_framac/code/min_dist.h
View file

@ -1,6 +1,12 @@
#include <limits.h>
#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);

31
content/conception_formelle/99-DM_framac/code/test.c Normal file
View file

@ -0,0 +1,31 @@
#include <limits.h>
#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;
}

2
content/conception_formelle/99-DM_framac/container/entrypoint.sh
View file

@ -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