From 238ab28b283a1d4d25deafcc919acbd244b811ad Mon Sep 17 00:00:00 2001
From: Viktor Kuncak <vkuncak@gmail.com>
Date: Tue, 24 Jul 2012 23:49:46 +0200
Subject: [PATCH] array bubble sort that actually works
---
.../master-thesis-regis/ArrayBubbleSort.scala | 81 +++++++++++++++++++
1 file changed, 81 insertions(+)
create mode 100644 testcases/master-thesis-regis/ArrayBubbleSort.scala
diff --git a/testcases/master-thesis-regis/ArrayBubbleSort.scala b/testcases/master-thesis-regis/ArrayBubbleSort.scala
new file mode 100644
index 000000000..14595f2c6
--- /dev/null
+++ b/testcases/master-thesis-regis/ArrayBubbleSort.scala
@@ -0,0 +1,81 @@
+import leon.Utils._
+
+object ArrayBubbleSort {
+ def sorted(a: Array[Int], l: Int, u: Int): Boolean = {
+ require(a.length >= 0 && l >= 0 && u < a.length && l <= u)
+ if (l==u) true else a(l) <= a(l+1) && sorted(a,l+1,u)
+ }
+
+ /* The calculus of Computation textbook */
+ def bubbleSort(a: Array[Int]): Array[Int] = ({
+ require(a.length >= 1)
+ var i = a.length - 1
+ var j = 0
+ val sa = a.clone
+ (while(i > 0) {
+ j = 0
+ (while(j < i) {
+ if(sa(j) > sa(j+1)) {
+ val tmp = sa(j)
+ sa(j) = sa(j+1)
+ sa(j+1) = tmp
+ }
+ j = j + 1
+ }) invariant(
+ j >= 0 &&
+ j <= i &&
+ i < sa.length &&
+ sa.length >= 0 &&
+ partitioned(sa, 0, i, i+1, sa.length-1) &&
+ sorted(sa, i, sa.length-1) &&
+ partitioned(sa, 0, j-1, j, j)
+ )
+ i = i - 1
+ }) invariant(
+ i >= 0 &&
+ i < sa.length &&
+ sa.length >= 0 &&
+ partitioned(sa, 0, i, i+1, sa.length-1) &&
+ sorted(sa, i, sa.length-1)
+ && sa.length == a.length // necessary
+ )
+ sa
+ }) ensuring(res => sorted(res, 0, a.length-1))
+
+ def partitioned(a: Array[Int], l1: Int, u1: Int, l2: Int, u2: Int): Boolean = {
+ require(a.length >= 0 && l1 >= 0 && u1 < l2 && u2 < a.length)
+ if(l2 > u2 || l1 > u1)
+ true
+ else {
+ var i = l1
+ var j = l2
+ var isPartitionned = true
+ (while(i <= u1) {
+ j = l2
+ (while(j <= u2) {
+ if(a(i) > a(j))
+ isPartitionned = false
+ j = j + 1
+ }) invariant(j >= l2 && i <= u1)
+ i = i + 1
+ }) invariant(i >= l1)
+ isPartitionned
+ }
+ }
+
+/* // This also work as the definition of sorted and partitioned, and verifies:
+
+ def sorted(a: Array[Int], l: Int, u: Int): Boolean = {
+ require(a.length >= 0 && l >= 0 && u < a.length && l <= u)
+ var k = l
+ var isSorted = true
+ (while(k < u) {
+ if(a(k) > a(k+1))
+ isSorted = false
+ k = k + 1
+ }) invariant(k <= u && k >= l)
+ isSorted
+ }
+
+*/
+}
--
GitLab