Add FramaC TDM

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

@@ -0,0 +1,15 @@
+#include "abs.h"
+
+int abs(int n)
+{
+    int res = n;
+    if (n < 0)
+        res = -n;
+    return res;
+}
+
+int abs2(int n)
+{
+    int aux = n % 2 + (n + 1) % 2;
+    return n * aux;
+}

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

@@ -0,0 +1,17 @@
+#ifndef __FORMALISM__
+#define __FORMALISM__
+
+#include <limits.h>
+
+/*@ logic integer abs(integer n) = 0<n?n:-n;*/
+
+/*@ terminates \true;
+    ensures \result == abs(n);
+ */
+int abs(int n);
+
+/*@ terminates \true;
+    ensures \result == abs(n);*/
+int abs2(int n);
+
+#endif

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

@@ -0,0 +1,14 @@
+#include <limits.h>
+#include "abs.h"
+
+/*
+    Le résultat doit être une valeur v telle que il existe i et j telle que v est t[i]-t[j], et que c’est le minimum pour l’ensemble des indices i des maximum pour les indices j des abs(t[i]-t[j]).
+
+    Une précondition peu évidente à trouver vous est spécifiée (elle vient de l’utilisation de abs, et empêche de prouver un seul invariant, donc je préfère vous la donner).
+    De même, la post-condition principale vous est donnée. Commencez par la démontrer, puis, comme dans les exercices précédents, observez que ce n’est pas suffisant et donnez et démontrez la post-condition manquante.
+ */
+/*@
+    requires \forall integer i; 0 <= i < n ==> INT_MAX > tab[i] >= 0;ensures \forall integer l; 0 <= l < n ==> (\exists integer b; 0 <= b < n && \forall integer k; 0 <= k < n ==> abs(tab[l]-tab[b]) >= abs(tab[l] - tab[k]) && \result <= abs(tab[l]-tab[b]));
+
+*/
+int diameter(int *tab, unsigned int n);

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

@@ -0,0 +1,17 @@
+#include "max_dist.h"
+
+int max_dist(int *tab, unsigned int n)
+{
+    int min = tab[0];
+    int max = tab[0];
+    unsigned int i = 1;
+    while (i < n)
+    {
+        if (tab[i] < min)
+            min = tab[i];
+        if (tab[i] > max)
+            max = tab[i];
+        i++;
+    }
+    return max - min;
+}

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

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

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

@@ -0,0 +1,22 @@
+#include "min_dist.h"
+int min_dist(int *tab, unsigned int n)
+{
+    int min = abs(tab[0] - tab[1]);
+    unsigned int i = 0;
+    while (i < n - 1)
+    {
+        int min_i = abs(tab[i] - tab[i + 1]);
+        unsigned int j = i + 2;
+        while (j < n)
+        {
+            int d = abs(tab[i] - tab[j]);
+            if (d < min_i)
+                min_i = d;
+            j++;
+        }
+        if (min_i < min)
+            min = min_i;
+        i++;
+    }
+    return min;
+}

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

@@ -0,0 +1,6 @@
+#include <limits.h>
+#include "abs-cor.h"
+
+/*@ 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);