diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-10-03 23:27:22 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-10-03 23:27:22 -0700 |
| commit | caa2c1d6c2aa2976d5ef055e412374832981e566 (patch) | |
| tree | 0b64a8d60d10cbfc04bf26e807600c33e0d9d0ee /Binaries | |
| parent | 4df8708df80d343bb40db88438798605f76eb873 (diff) | |
Dafny: complete implementation of iterators
Diffstat (limited to 'Binaries')
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 6 |
1 files changed, 6 insertions, 0 deletions
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 --------------------------------------------
// ---------------------------------------------------------------
|