diff --git a/mytest/Bubble.scala b/mytest/Bubble.scala index b8d7e5661580222ab202a008c03f6a3e21df9d01..4312fed85bd6b0f98e4f871c02af956d9f4ea612 100644 --- a/mytest/Bubble.scala +++ b/mytest/Bubble.scala @@ -17,7 +17,9 @@ object Bubble { } j = j + 1 }) invariant( + j >= 0 && j <= i && + i < size && isArray(sortedArray, size) && partitioned(sortedArray, size, 0, i, i+1, size-1) && partitioned(sortedArray, size, 0, j-1, j, j) && @@ -25,7 +27,8 @@ object Bubble { ) i = i - 1 }) invariant( - i >= 0 && + i >= -1 && + i < size && isArray(sortedArray, size) && partitioned(sortedArray, size, 0, i, i+1, size-1) && sorted(sortedArray, size, i, size-1)