diff options
author | rustanleino <unknown> | 2010-06-11 02:02:36 +0000 |
---|---|---|
committer | rustanleino <unknown> | 2010-06-11 02:02:36 +0000 |
commit | fadc6a922eb99b83b898b55286e48f63ed0df751 (patch) | |
tree | 8aa3e8fa417e79fdfc96502ddcb5a5fdc13c7927 /Test/vacid0/SparseArray.dfy | |
parent | 9521767199e98aafb780421b859da3fb8773af42 (diff) |
Dafny: Added two additional heuristics for guessing missing loop decreases clauses (for loop guard A!=B and for loop guards with multiple conjuncts)
Diffstat (limited to 'Test/vacid0/SparseArray.dfy')
-rw-r--r-- | Test/vacid0/SparseArray.dfy | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/Test/vacid0/SparseArray.dfy b/Test/vacid0/SparseArray.dfy index da1f63bb..0e6aff05 100644 --- a/Test/vacid0/SparseArray.dfy +++ b/Test/vacid0/SparseArray.dfy @@ -55,7 +55,6 @@ class SparseArray<T> { // TODO: why doesn't this work instead of the next line? invariant (forall x :: x in s ==> x == zero);
invariant (forall i :: 0 <= i && i < |s| ==> s[i] == zero);
invariant |id| == k && (forall i :: 0 <= i && i < k ==> id[i] == i);
- decreases N - k;
{
s := s + [zero];
id := id + [k];
@@ -110,7 +109,6 @@ class SparseArray<T> { var i := 0;
while (i < n)
invariant i <= n && |arr| == i;
- decreases n - i;
{
var g: G;
arr := arr + [g];
|