From 80c3df7377a8537d8d92257584a6663e8f6cc42c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Fri, 18 May 2012 09:50:49 +0200
Subject: [PATCH] remove invariants of BubbleSort to identify a clearer bug
---
demo/BubbleSortBug.scala | 39 ++-------------------------------------
1 file changed, 2 insertions(+), 37 deletions(-)
diff --git a/demo/BubbleSortBug.scala b/demo/BubbleSortBug.scala
index d8d1c4eb9..a25554f03 100644
--- a/demo/BubbleSortBug.scala
+++ b/demo/BubbleSortBug.scala
@@ -18,23 +18,9 @@ object BubbleSortBug {
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, j+1, j+1)
- )
+ }) invariant(j >= 0 && j <= i && i < sa.length)
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)
- )
+ }) invariant(i >= 0 && i < sa.length)
sa
}) ensuring(res => sorted(res, 0, a.length-1))
@@ -50,25 +36,4 @@ object BubbleSortBug {
isSorted
}
- 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
- }
- }
-
}
--
GitLab