diff options
Diffstat (limited to 'Test/hofs')
-rw-r--r-- | Test/hofs/WhileLoop.dfy | 10 |
1 files changed, 5 insertions, 5 deletions
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; |