Validation initiale

.gitignore

@@ -0,0 +1,40 @@
+###########
+# General #
+###########
+
+TAGS
+*.aux
+*.lia.cache
+*.glob
+*.vo
+*.cm*
+*.back
+*.o
+*.a
+*.annot
+*~
+*_DEP
+*.depend
+\#*
+.\#*
+.DS_Store
+*.tmp
+/.git_version
+*~
+frama_c_journal.ml
+
+#build
+Makefile.plugin.generated
+configure
+autom4te.cache
+/.depend
+/config.log
+/config.status
+/frama-c-*.tar.gz
+/.log.autoconf
+/.Makefile.user
+/ocamlgraph/
+META.*
+*.script.back
+*.frama-c*
+*.out

binary_search/binary_search.c

@@ -0,0 +1,34 @@
+/*@ predicate sorted{L}(long *t, integer a, integer b) =
+  @    \forall integer i,j; a <= i <= j <= b ==> t[i] <= t[j];
+  @*/
+
+/*@ requires n >= 0 && \valid(t+(0..n-1));
+  @ ensures -1 <= \result < n;
+  @ behavior success:
+  @   ensures \result >= 0 ==> t[\result] == v;
+  @ behavior failure:
+  @   assumes sorted(t,0,n-1);
+  @   ensures \result == -1 ==>
+  @     \forall integer k; 0 <= k < n ==> t[k] != v;
+  @*/
+int binary_search(long t[], int n, long v) {
+  int l = 0, u = n-1;
+  /*@ loop assigns l, u;
+    @ loop invariant
+    @   0 <= l && u <= n-1;
+    @ for failure:
+    @   loop invariant
+    @   \forall integer k; 0 <= k < n && t[k] == v ==> l <= k <= u;
+    @ loop variant u-l;
+    @*/
+  while (l <= u ) {
+    //int m = (l + u) / 2;
+    //bug fix
+    int m = l + ((u-l)/2);
+    //@ assert l <= m <= u;
+    if (t[m] < v) l = m + 1;
+    else if (t[m] > v) u = m - 1;
+    else return m;
+  }
+  return -1;
+}

fact/fact.c

@@ -0,0 +1,24 @@
+/*@ axiomatic Fact {
+     predicate isFact(integer n, integer fact);
+     axiom Fact_1: isFact(0,1);
+     axiom Fact_2: \forall integer n,r1; n > 0 ==> isFact(n-1,r1)
+                                              ==> isFact(n,n*r1);
+}
+*/
+
+/*@ requires n >= 0;
+  @ ensures isFact(n,\result);
+*/
+int fact (int n) {
+  int y = 1;
+  int x = n;
+  /*@ loop invariant 0 <= x <= n;
+    @ loop invariant \forall integer r1; isFact(x,r1) ==> isFact(n,y*r1);
+    @ loop assigns y,x;
+    @ loop variant x;*/
+  while (x > 1) {
+    y = y * x;
+    x = x - 1;
+  };
+  return y;
+}

find/find.c

@@ -0,0 +1,29 @@
+/*@ requires \valid(t+(0 .. n-1));
+  @ requires n >= 0;
+  @ assigns \nothing;
+  @ behavior some:
+	assumes \exists integer i; 0 <= i < n && t[i] == val;
+	ensures 0 <= \result < n;
+	ensures t[\result] == val;
+	ensures \forall integer i; 0 <= i < \result ==> t[i] != val;
+  @ behavior none:
+	assumes \forall integer i; 0 <= i < n ==> t[i] != val;
+	ensures \result == n;
+  @ complete behaviors;
+  @ disjoint behaviors;
+*/
+int find(int * t, int n, int val){
+	int i = 0;
+
+	/*@ loop invariant 0 <= i <= n;
+	  @ loop invariant \forall integer k; 0 <= k < i ==> t[k] != val;
+	  @ loop assigns i;
+	  @ loop variant n-i;
+	*/
+	for(i = 0; i < n; i++){
+		if(t[i] == val){
+			return i;		
+		}
+	}
+	return n;
+}

find_first/find_first_of.c

@@ -0,0 +1,74 @@
+/*@ predicate HasValue{A}(int *a, integer m, integer n, integer v) = 
+      \exists int i; m <= i < n && a[i] == v;
+*/
+
+/*@ predicate HasValue{A}(int *a, integer n, integer v) =
+      HasValue(a, 0, n, v);
+*/
+
+/*@ predicate HasValueOf{A}(int *a, int m, int *b, int n) =
+      \exists integer i; 0 <= i < m && HasValue{A}(b, n, a[i]);
+*/
+
+/*@ requires \valid(t+(0 .. n-1));
+  @ requires n >= 0;
+  @ assigns \nothing;
+  @ behavior some:
+	assumes HasValue(t, n, val);
+	ensures bound: 0 <= \result < n;
+	ensures result: t[\result] == val;
+	ensures first: !HasValue(t, \result, val);
+  @ behavior none:
+	assumes !HasValue(t, n, val);
+	ensures result: \result == n;
+  @ complete behaviors;
+  @ disjoint behaviors;
+*/
+int find(int * t, int n, int val){
+	int i = 0;
+
+	/*@ loop invariant bound: 0 <= i <= n;
+	  @ loop invariant not_found: !HasValue(t,i,val);
+	  @ loop assigns i;
+	  @ loop variant n-i;
+	*/
+	for(i = 0; i < n; i++){
+		if(t[i] == val){
+			return i;		
+		}
+	}
+	return n;
+}
+
+
+/*@ requires \valid(a+(0 .. m-1));
+  @ requires \valid(b+(0 .. n-1));
+  @ requires n >= 0;
+  @ requires m >= 0;
+  @ assigns \nothing;
+  @ behavior found:
+	assumes HasValueOf(a, m, b, n);
+	ensures bound: 0 <= \result < m;
+	ensures result: HasValue(b, n, a[\result]);
+	ensures first: !HasValueOf(a, \result, b, n);
+  @ behavior not_found:
+	assumes !HasValueOf(a, m, b, n);
+	ensures result: \result == m;
+  @ complete behaviors;
+  @ disjoint behaviors;
+*/
+int find_first_of(int *a, int m, int *b, int n){
+  int i = 0;
+
+  /*@ loop invariant bound: 0 <= i <= m;
+    @ loop invariant not_found: !HasValueOf(a, i, b, n);
+    @ loop assigns i;
+    @ loop variant m-i;
+   */
+  for(int i = 0; i < m; i++){
+    if(find(b, n, a[i]) < n){
+      return i;
+    }
+  }
+  return m;
+}

find_quatuor/letplay.c

@@ -0,0 +1,24 @@
+/*@ requires \valid_read(s + (0 .. n - 1));
+  @ requires n >= 0 && n % 4 == 0;
+  @ assigns \nothing;
+  @ ensures 0 <= \result <= n;
+  @ ensures 0 <= \result < n ==> s[\result] == '\0';
+  @ ensures \forall integer i; 0 <= i < \result ==> s[i] != '\0';*/
+int strnlen_ref (char *s, int n){
+  int i = 0;
+  /*@ ghost int p = 0;*/
+  /*@ loop invariant i == p*4;
+    @ loop invariant 0 <= i <= n;
+    @ loop invariant \forall integer k; 0 <= k < i ==> s[k] != '\0';
+    @ loop assigns i,p;
+    @ loop variant n - i;
+  */
+ while (i < n) {
+   if (s[i] == '\0') return i; i++;
+   if (s[i] == '\0') return i; i++;
+   if (s[i] == '\0') return i; i++;
+   if (s[i] == '\0') return i; i++;
+   /*@ ghost p = p + 1;*/
+  }
+  return n;
+}

insertion_sort/insertion_sort.c

@@ -0,0 +1,126 @@
+/*@ predicate sorted(int* tab, integer idx) = \forall integer x,y; 0 <= x < y < idx ==> tab[x] <= tab[y]; */
+
+/*@ predicate swap{L1, L2}(int *a, int *b, integer begin, integer i, integer j, integer end) =
+      begin <= i < end && begin <= j < end &&
+      \at(a[i], L1) == \at(b[j], L2) &&
+      \at(a[j], L1) == \at(b[i], L2) &&
+      \forall integer k; begin <= k < end && k != i && k != j ==> \at(a[k], L1) == \at(b[k], L2);
+*/
+
+/*@ predicate same_array{L1,L2}(int *a, int *b, integer begin, integer end) =
+      \forall integer k; begin <= k < end ==> \at(a[k],L1) == \at(b[k],L2);
+*/
+
+/*@ inductive same_elements{L1, L2}(int *a, int *b, integer begin, integer end) {
+      case refl{L1, L2}:
+        \forall int *a, int *b, integer begin, end;
+        same_array{L1,L2}(a, b, begin, end) ==>
+        same_elements{L1, L2}(a, b, begin, end);
+      case swap{L1, L2}: \forall int *a, int *b, integer begin, i, j, end;
+        swap{L1, L2}(a, b, begin, i, j, end) ==>
+        same_elements{L1, L2}(a, b, begin, end);
+      case trans{L1, L2, L3}: \forall int* a, int *b, int *c, integer begin, end;
+        same_elements{L1, L2}(a, b, begin, end) ==>
+        same_elements{L2, L3}(b, c, begin, end) ==>
+        same_elements{L1, L3}(a, c, begin, end);
+      case split {L1, L2}: \forall int *a, int *b, integer begin, i, end;
+        begin <= i < end ==>
+        same_elements{L1,L2}(a, b, begin, i) ==>
+        same_elements{L1,L2}(a, b, i, end) ==>
+        same_elements{L1,L2}(a, b, begin, end);
+}*/
+
+/*@ lemma partition {L1, L2}: \forall int *a, int *b, integer begin, i, j, end;
+        begin <= i <= j < end ==>
+        same_array{L1,L2}(a, b, begin, i) ==>
+        same_elements{L1,L2}(a, b, i, j) ==>
+        same_array{L1,L2}(a, b, j, end) ==>
+        same_elements{L1, L2}(a, b, begin, end);
+*/
+
+/*@ requires 0 <= n;
+    requires sorted(tab,n);
+    ensures \forall int j; 0 <= j < \result ==> tab[j] <= val;
+    ensures \forall int j; \result <= j < n ==> tab[j] > val;
+    ensures 0 <= \result <= n;
+    assigns \nothing;
+*/
+int chercher_limite(int tab[], int n, int val){
+  int i;
+  /*@ loop invariant 0 <= i <= n;
+      loop invariant \forall int j; 0 <= j < i ==> tab[j] <= val;
+      loop assigns i;
+      loop variant n - i;
+   */
+  for (i = 0; i < n; i++){
+    if(tab[i] > val){
+      return i;
+    }
+  }
+  return n;
+}
+
+/*@ requires 0 <= idx <= n;
+    requires \separated(tab+(0..n),gtab+(0..n));
+    requires same_array{Pre, Pre}(tab, gtab, 0, n);
+    ensures \forall int j; idx < j <= n ==> tab[j] == \at(tab[j-1],Pre);
+    ensures \forall int j; 0 <= j <= idx ==> tab[j] == \at(tab[j],Pre);
+    ensures same_elements{Pre, Post}(gtab, gtab, 0, n+1);
+    ensures \forall integer k; 0 <= k <= n && k != idx ==> tab[k] == gtab[k];
+    ensures \at(gtab[idx],Post) == \at(gtab[n],Pre);
+    assigns tab[0..n],gtab[0..n];
+*/
+void decale(int tab[], int n, int idx) /*@ ghost (int gtab[])*/{
+  int i;
+  /*@ loop invariant idx <= i <= n;
+      loop invariant \forall int j; i < j <= n ==> tab[j] == \at(tab[j-1],Pre);
+      loop invariant \forall int j; 0 <= j <= i ==> tab[j] == \at(tab[j],Pre);
+      loop invariant same_elements{Pre, Here}(gtab, gtab, 0, n+1);
+      loop invariant \forall integer k; i < k <= n ==> tab[k] == gtab[k];
+      loop invariant \forall integer k; 0 <= k < i  ==> tab[k] == gtab[k];
+      loop invariant \at(gtab[i],Here) == \at(gtab[n],Pre);
+      loop assigns i, tab[0..n], gtab[0..n];
+      loop variant i;
+   */
+  for (i = n; i > idx; i--){
+    /*@ ghost L1:;*/
+    tab[i] = tab[i-1];
+    /*@ ghost int temp = gtab[i];*/
+    /*@ ghost gtab[i] = gtab[i-1];*/
+    /*@ ghost gtab[i-1] = temp;*/
+    /*@ assert swap{L1, Here}(gtab, gtab, 0, i-1, i, n+1);*/
+  }
+  return;
+}
+
+/*@ ghost int *t;*/ //use a local array and seach how to handle the case n = 0
+
+/*@ requires 0 <= n;
+  requires \separated(tab+(0..n-1),t+(0..n-1));
+  requires same_array{Pre, Pre}(tab, t, 0, n);
+  ensures sorted(tab,n);
+  ensures same_elements{Pre, Post}(tab,tab, 0, n );
+  assigns tab[0..n-1],t[0..n-1];*/
+void tri_insertion(int tab[], int n){
+  int lim;
+  /*@ loop invariant 0 <= lim <= n;
+      loop invariant sorted(tab,lim);
+      loop invariant \forall int j; lim <= j < n ==> tab[j] == \at(tab[j],Pre);
+      loop invariant same_array{Here, Here}(tab, t, 0, n);
+      loop invariant same_elements{Pre, Here}(t,t, 0, n );
+      loop assigns tab[0..n-1],t[0..n-1],lim;
+      loop variant n - lim;
+   */
+  for (lim = 0; lim < n; lim++){
+  l1:;
+    int val = tab[lim];
+    int idx = chercher_limite(tab,lim,val);
+    decale(tab,lim,idx)/*@ ghost (t)*/;
+    /*@ assert same_elements{l1,Here}(t,t,0,n);*/
+    /*@ assert same_elements{Pre, Here}(t,t, 0, n );*/
+    tab[idx] = val;
+    /*@ assert sorted(tab,lim);*/
+    /*@ assert same_elements{Pre, Here}(t,t, 0, n );*/
+  }
+  return;
+}