diff options
author | 2010-03-13 03:30:09 +0000 | |
---|---|---|
committer | 2010-03-13 03:30:09 +0000 | |
commit | d83d1f3813e2765db4e3855adcb10fc3319a737f (patch) | |
tree | e6291ebf6ab4993644926825d8e35379ef05a002 /Test/VSI-Benchmarks/b2.dfy | |
parent | c48d205507068bcce227645acc7a07add0561820 (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.dfy | 2 |
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;
|