From ae34a9ea75baed0b929b0a062e691af84b4a7fb7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Thu, 4 Apr 2013 14:53:11 +0200
Subject: [PATCH] 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 | 59 +++++++++++++++++++++++++++++++++
testcases/BubbleFun.scala | 28 ++++++++--------
2 files changed, 74 insertions(+), 13 deletions(-)
create mode 100644 testcases/BinarySearchFun.scala
diff --git a/testcases/BinarySearchFun.scala b/testcases/BinarySearchFun.scala
new file mode 100644
index 000000000..1398f9b9e
--- /dev/null
+++ b/testcases/BinarySearchFun.scala
@@ -0,0 +1,59 @@
+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:
diff --git a/testcases/BubbleFun.scala b/testcases/BubbleFun.scala
index 5962eea28..4847fc8ac 100644
--- a/testcases/BubbleFun.scala
+++ b/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]
}
}
--
GitLab