From 43a89884e1af0902d5ab701f8d5b9e8eb3c9b431 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Fri, 4 May 2012 15:19:31 +0200
Subject: [PATCH] binary search does not generate invalid VC
---
testcases/BinarySearch.scala | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/testcases/BinarySearch.scala b/testcases/BinarySearch.scala
index 5ee63b316..986ee41ae 100644
--- a/testcases/BinarySearch.scala
+++ b/testcases/BinarySearch.scala
@@ -23,9 +23,10 @@ object BinarySearch {
low = i + 1
}) invariant(
res >= -1 &&
- res > a.length &&
+ res < a.length &&
0 <= low &&
low <= high + 1 &&
+ high >= -1 &&
high < a.length &&
(if (res >= 0)
a(res) == key else
--
GitLab