remove invariants of BubbleSort to identify a clearer bug

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
-    }
-  }
-
 }