Introduces purely functional array benchmarks

This commit use array with a purely functional styles to process them.
In particular, it uses recursive function instead of while loop.
Those benchmarks are easier to debug than the equivalent ones relying
on imperative features, because they do not go through any code
transformations.

Note that they still have the same limitation as the imperative ones
(cannot prove inductive properties), which shows that the imperative
transformation are not responsible for the limitation in proving
validity of program over arrays.

testcases/BinarySearchFun.scala

+import leon.Utils._
+
+object BinarySearchFun {
+
+  def binarySearch(a: Array[Int], key: Int, low: Int, high: Int): Int = ({
+    require(a.length > 0 && sorted(a, low, high) &&
+        0 <= low && low <= high + 1 && high < a.length
+    )
+
+    if(low <= high) {
+      val i = (high + low) / 2
+      val v = a(i)
+
+      if(v == key) i
+      else if (v > key) binarySearch(a, key, low, i - 1)
+      else binarySearch(a, key, i + 1, high)
+    } else -1
+  }) ensuring(res =>
+      res >= -1 &&
+      res < a.length &&
+      (if (res >= 0)
+          a(res) == key else
+          (high < 0 || (!occurs(a, low, (high+low)/2, key) && !occurs(a, (high+low)/2, high, key)))
+      )
+    )
+
+
+  def occurs(a: Array[Int], from: Int, to: Int, key: Int): Boolean = {
+    require(a.length >= 0 && to <= a.length && from >= 0)
+    def rec(i: Int): Boolean = {
+      require(i >= 0)
+      if(i >= to)
+        false
+      else {
+       if(a(i) == key) true else rec(i+1)
+      }
+    }
+    if(from >= to)
+      false
+    else
+      rec(from)
+  }
+
+
+  def sorted(a: Array[Int], l: Int, u: Int) : Boolean = {
+    require(a.length >= 0 && l >= 0 && l <= u + 1 && u < a.length)
+    val t = sortedWhile(true, l, l, u, a)
+    t._1
+  }
+
+  def sortedWhile(isSorted: Boolean, k: Int, l: Int, u: Int, a: Array[Int]): (Boolean, Int) = {
+    require(a.length >= 0 && l >= 0 && l <= u+1 && u < a.length && k >= l && k <= u + 1)
+    if(k < u) {
+      sortedWhile(if(a(k) > a(k + 1)) false else isSorted, k + 1, l, u, a)
+    } else (isSorted, k)
+  }
+}
+
+// vim: set ts=4 sw=4 et:

testcases/BubbleFun.scala

@@ -19,7 +19,7 @@ object BubbleFun {
         val t = sortNestedWhile(sortedArray, 0, i, size)
         sortWhile(t._2, t._1, i - 1, size)
       } else (j, sortedArray, i)
-    }) ensuring(res => isArray(res._2, size) && 
+    }) ensuring(res => isArray(res._2, size) &&
                        sorted(res._2, size, res._3, size - 1) &&
                        partitioned(res._2, size, 0, res._3, res._3+1, size-1) &&
                        res._3 >= 0 && res._3 <= 0 /*&& content(res._2, size) == content(sortedArray, size)*/
@@ -32,7 +32,7 @@ object BubbleFun {
               partitioned(sortedArray, size, 0, i, i+1, size-1) &&
               partitioned(sortedArray, size, 0, j-1, j, j))
       if(j < i) {
-        val newSortedArray = 
+        val newSortedArray =
           if(sortedArray(j) > sortedArray(j + 1))
             sortedArray.updated(j, sortedArray(j + 1)).updated(j+1, sortedArray(j))
           else
@@ -91,7 +91,7 @@ object BubbleFun {
     // ------------- partitioned ------------------
     def partitioned(a: Map[Int,Int], size: Int, l1: Int, u1: Int, l2: Int, u2: Int) : Boolean = {
       require(isArray(a, size) && size < 5 && l1 >= 0 && u1 < l2 && u2 < size)
-      if(l2 > u2 || l1 > u1) 
+      if(l2 > u2 || l1 > u1)
         true
       else {
         val t = partitionedWhile(l2, true, l1, l1, size, u2, l2, u1, a)
@@ -114,20 +114,20 @@ object BubbleFun {
           (if (a(i) > a(j))
             false
           else
-            isPartitionned), 
+            isPartitionned),
           j + 1, i, l1, u1, size, u2, a, l2)
       } else (isPartitionned, j)
     }
 
 
     //------------ isArray -------------------
-    def isArray(a: Map[Int,Int], size: Int): Boolean = 
+    def isArray(a: Map[Int,Int], size: Int): Boolean =
       if(size <= 0)
         false
       else
         isArrayRec(0, size, a)
 
-    def isArrayRec(i: Int, size: Int, a: Map[Int,Int]): Boolean = 
+    def isArrayRec(i: Int, size: Int, a: Map[Int,Int]): Boolean =
       if (i >= size)
         true
       else {
@@ -141,13 +141,15 @@ object BubbleFun {
     // ----------------- content ------------------
     def content(a: Map[Int, Int], size: Int): Set[Int] = {
       require(isArray(a, size) && size < 5)
-      var i = 0
-      var s = Set.empty[Int]
-      while(i < size) {
-        s = s ++ Set(a(i))
-        i = i + 1
-      }
-      s
+      contentRec(a, size, 0)
+    }
+
+    def contentRec(a: Map[Int, Int], size: Int, i: Int): Set[Int] = {
+      require(isArray(a, size) && i >= 0)
+      if(i < size)
+        Set(a(i)) ++ contentRec(a, size, i+1)
+      else
+        Set.empty[Int]
     }
 
 }