From 268ed5f5396db56206309cdc3fe346213959456c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Wed, 9 May 2012 20:06:51 +0200
Subject: [PATCH] stronger loop invariant
---
testcases/BubbleSort.scala | 2 ++
1 file changed, 2 insertions(+)
diff --git a/testcases/BubbleSort.scala b/testcases/BubbleSort.scala
index f807c1b85..5249f4fbe 100644
--- a/testcases/BubbleSort.scala
+++ b/testcases/BubbleSort.scala
@@ -22,6 +22,7 @@ object BubbleSort {
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)
@@ -30,6 +31,7 @@ object BubbleSort {
}) invariant(
i >= 0 &&
i < sa.length &&
+ sa.length >= 0 &&
partitioned(sa, 0, i, i+1, sa.length-1) &&
sorted(sa, i, sa.length-1)
)
--
GitLab