Going forward, but gently...

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

@@ -318,6 +318,9 @@ int abs2(int n)
         /*@
           loop assign i, min, max;
         */
+        while ( i < n )
+        {
+            // ...
         \end{lstlisting}
     \end{solutionorbox}
 
@@ -343,7 +346,14 @@ int max_dist(int *tab, unsigned int n)
 
 
     \begin{solutionorbox}
-        METTEZ VOTRE RÉPONSE ICI.
+        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}
+        \*@
+            require 0 < n <= UINT_MAX;
+            require \valid(tab+(0..n-1));
+            ensures \result >= 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.
@@ -351,7 +361,7 @@ int max_dist(int *tab, unsigned int n)
 
 
     \begin{solutionorbox}
-        METTEZ VOTRE RÉPONSE ICI.
+        
     \end{solutionorbox}
 
 

content/conception_formelle/99-DM_framac/code/abs.h

@@ -6,16 +6,20 @@
 /*@ logic integer abs(integer n) = 0<n?n:-n;*/
 
 /*@
-    requires INT_MIN <= n;
+    requires INT_MIN < n < INT_MAX;
     terminates \true;
     ensures \result == abs(n);
+    assigns \nothing;
  */
 int abs(int n);
 
 /*@
-    requires INT_MIN <= n * (int)((int)n % 2 + ((int)n +1)%2) <= INT_MAX;
+    requires INT_MIN < n < INT_MAX;
+    requires INT_MIN <= n * (int)((int)n % 2 + ((int)n + 1)%2) <= INT_MAX;
     terminates \true;
-    ensures \result == abs(n);*/
+    ensures \result == abs(n);
+    assigns \nothing;
+*/
 int abs2(int n);
 
 #endif

content/conception_formelle/99-DM_framac/code/max_dist.c

@@ -5,6 +5,16 @@ int max_dist(int *tab, unsigned int n)
     int min = tab[0];
     int max = 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 invariant I4: \exists integer j; ( 0 < j < i ==> max == tab[j]);
+        loop invariant I5: \exists integer j; ( 0 < j < i ==> min == tab[j]);
+        loop variant n - i;
+    */
     while (i < n)
     {
         if (tab[i] < min)

content/conception_formelle/99-DM_framac/code/max_dist.h

@@ -1,6 +1,10 @@
 #include <limits.h>
 #include "abs.h"
 
-/*@ ensures \forall integer a,b; 0 <= a < b < n ==> \result >= abs(tab[a]-tab[b]);
+/*@
+ requires 0 < n < UINT_MAX;
+ requires \valid_read(tab+(0..n-1));
+ terminates \true;
+ ensures \forall integer a,b; 0 <= a < b < n ==> \result >= abs(tab[a]-tab[b]);
  */
 int max_dist(int *tab, unsigned int n);