Fist commit (WIP)

1 files changed, 66 insertions, 0 deletions

diff --git a/tests/sources/0601_heap_sort.c b/tests/sources/0601_heap_sort.c
new file mode 100644
index 0000000..dd12e1a
--- /dev/null
+++ b/tests/sources/0601_heap_sort.c
@@ -0,0 +1,66 @@
+// Example from Cousot Habwachs POPL 1978
+
+// Heap sort, where array  operations are abstracted away
+// to get a non-deterministic scalar program
+
+// expected results: with polyhedra, no assertion failure
+
+int L,R,I,J;
+int N = rand(1,100000);  // array size
+
+L = N/2 + 1;
+R = N;
+
+if (L >= 2) {
+  L = L - 1; 
+  // model the assignment "K = TAB[L]"
+  assert(1 <= L && L <= N);
+}
+else {
+  // model the assignments "K = TAB[R]; TAB[R] = TAB[1]"
+   assert(1 <= R && R <= N);
+   assert(1 <= 1 && 1 <= N);
+   R = R - 1;
+}
+
+while (R >= 2) {
+  I = L;
+  J = 2*I;
+
+  while (J <= R && rand(0,1)==0) {
+    if (J <= R-1) {
+      // model the comparison "TAB[J] < TAB[J+1]"
+      assert(1 <= J && J <= N);
+      assert(1 <= (J+1) && (J+1) <= N);
+      if (rand(0,1)==0) { J = J + 1; }
+    }
+
+    // model the comparison "K < TAB[J]"
+    assert(1 <= J && J <= N);
+    if (rand(0,1)==0) {
+      // model the assignment "TAB[I] = TAB[J]"
+      assert(1 <= I && I <= N);
+      assert(1 <= J && J <= N);   
+      I = J;
+      J = 2*J;
+    }
+  }
+
+  // model the assignment "TAB[I] = K"
+  assert(1 <= I && I <= N);
+
+  if (L >= 2) {
+    L = L - 1; 
+    // model the assignment "K = TAB[L]"
+    assert(1 <= L && L <= N);
+  }
+  else {
+    // model the assignments "K = TAB[R]; TAB[R] = TAB[1]"
+    assert(1 <= R && R <= N);
+    assert(1 <= 1 && 1 <= N);
+    R = R - 1;
+  }
+
+  // model the assignment "TAB[1] = K"
+  assert(1 <= 1 && 1 <= N);
+}