From caa2c1d6c2aa2976d5ef055e412374832981e566 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Wed, 3 Oct 2012 23:27:22 -0700 Subject: Dafny: complete implementation of iterators --- Binaries/DafnyPrelude.bpl | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'Binaries') diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 02d0f344..e6d05bea 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -633,6 +633,12 @@ procedure $IterHavoc1(this: ref, mod: Set BoxType, nw: Set BoxType); $o == this || mod[$Box($o)] || nw[$Box($o)]); ensures $HeapSucc(old($Heap), $Heap); +procedure $IterCollectNewObjects(prevHeap: HeapType, newHeap: HeapType, this: ref, NW: Field (Set BoxType)) + returns (s: Set BoxType); + ensures (forall bx: BoxType :: { s[bx] } s[bx] <==> + read(newHeap, this, NW)[bx] || + ($Unbox(bx) != null && !read(prevHeap, $Unbox(bx):ref, alloc) && read(newHeap, $Unbox(bx):ref, alloc))); + // --------------------------------------------------------------- // -- Non-determinism -------------------------------------------- // --------------------------------------------------------------- -- cgit v1.2.3