summaryrefslogtreecommitdiff
path: root/Test/VSI-Benchmarks/b2.dfy
diff options
context:
space:
mode:
authorGravatar rustanleino <unknown>2010-03-13 03:30:09 +0000
committerGravatar rustanleino <unknown>2010-03-13 03:30:09 +0000
commitd83d1f3813e2765db4e3855adcb10fc3319a737f (patch)
treee6291ebf6ab4993644926825d8e35379ef05a002 /Test/VSI-Benchmarks/b2.dfy
parentc48d205507068bcce227645acc7a07add0561820 (diff)
Dafny: Added definedness checks for all statements (previously, some were missing)
Boogie: Added {:subsumption <n>} attribute to assert statements, which overrides the /subsumption command-line setting
Diffstat (limited to 'Test/VSI-Benchmarks/b2.dfy')
-rw-r--r--Test/VSI-Benchmarks/b2.dfy2
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/VSI-Benchmarks/b2.dfy b/Test/VSI-Benchmarks/b2.dfy
index 457bc894..7d964061 100644
--- a/Test/VSI-Benchmarks/b2.dfy
+++ b/Test/VSI-Benchmarks/b2.dfy
@@ -17,7 +17,7 @@ class Benchmark2 {
var high := a.Length();
while (low < high)
- invariant 0 <= low && high <= a.Length();
+ invariant 0 <= low && low <= high && high <= a.Length();
invariant (forall i :: 0 <= i && i < low ==> a.Get(i) < key);
invariant (forall i :: high <= i && i < a.Length() ==> key < a.Get(i));
decreases high - low;