diff options
author | leino <unknown> | 2015-06-25 18:10:42 -0700 |
---|---|---|
committer | leino <unknown> | 2015-06-25 18:10:42 -0700 |
commit | 3d6b2b77830f7f2bc4f3e61d4d3c8a163123dd31 (patch) | |
tree | ebb5f6b327343e7e120cd4dff434ed3131326696 /Test | |
parent | e1326254214bcd2546ab5ca992cf4c26e4aa99ed (diff) |
Removed unneeded :heapQuantifier from test case (rendinging this attribute currently unused in the test suite)
Diffstat (limited to 'Test')
-rw-r--r-- | Test/dafny0/SeqFromArray.dfy | 4 | ||||
-rw-r--r-- | Test/hofs/WhileLoop.dfy | 10 |
2 files changed, 7 insertions, 7 deletions
diff --git a/Test/dafny0/SeqFromArray.dfy b/Test/dafny0/SeqFromArray.dfy index aa131f98..3a8760ba 100644 --- a/Test/dafny0/SeqFromArray.dfy +++ b/Test/dafny0/SeqFromArray.dfy @@ -83,8 +83,8 @@ method M(a: array<int>, c: array<int>, m: nat, n: nat, k: nat, l: nat) case l+m <= c.Length && forall i :: 0 <= i < m ==> a[i] == c[l+i] =>
assert a[..m] == c[l..l+m];
case l+a.Length <= c.Length && forall i :: k <= i < a.Length ==> a[i] == c[l+i] =>
- assert a[k..] == c[l+k..l+a.Length];
+ assert a[k..] == c[l+k..l+a.Length];
case l+k+m <= c.Length && forall i :: k <= i < k+m ==> a[i] == c[l+i] =>
- assert a[k..k+m] == c[l+k..l+k+m];
+ assert a[k..k+m] == c[l+k..l+k+m];
}
}
diff --git a/Test/hofs/WhileLoop.dfy b/Test/hofs/WhileLoop.dfy index f79562e9..2c91a8cc 100644 --- a/Test/hofs/WhileLoop.dfy +++ b/Test/hofs/WhileLoop.dfy @@ -34,14 +34,14 @@ method OneShot(n: int) { method HeapQuant(n: int) { var f : int -> int := x => x; - var i := new Ref<int>; + var i := new Ref; ghost var r := 0; i.val := 0; - while (i.val < n) - invariant forall u {:heapQuantifier} :: f.requires(u); - invariant forall u {:heapQuantifier} :: f.reads(u) == {}; + while i.val < n + invariant forall u :: f.requires(u); + invariant forall u :: f.reads(u) == {}; invariant r == i.val; - invariant forall u {:heapQuantifier} :: f(u) == u + r; + invariant forall u :: f(u) == u + r; { i.val, r := i.val + 1, r + 1; f := x => f(x) + 1; |