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 | 0cf1c052a1b3f89384a6c859fc8680851b6edce0 (patch) | |
| tree | ec658bed2c838a96d7935e0524285776749789af /Binaries | |
| parent | 8c2d89e567cc51bbe2595d8aa434d3684d26892c (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 --------------------------------------------
// ---------------------------------------------------------------
|