From 75c930149ade9d3cf05804a0853d400f11ed8534 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Wed, 11 Apr 2012 16:03:38 +0200
Subject: [PATCH] some fixes in the invariants
---
mytest/Bubble.scala | 5 ++++-
1 file changed, 4 insertions(+), 1 deletion(-)
diff --git a/mytest/Bubble.scala b/mytest/Bubble.scala
index b8d7e5661..4312fed85 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)
--
GitLab