diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-10-04 00:41:44 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-10-04 00:41:44 -0700 |
| commit | 2d5a393b81ef2b389278f161460a1f98719c0aa6 (patch) | |
| tree | 128e993567d6f392c11e3ab4f068da5f2a817db3 /Binaries | |
| parent | 86da04e8be269d13874191c81cee0e2110d6373e (diff) | |
Dafny: fixed merge
Diffstat (limited to 'Binaries')
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index fafc9484..342b72c1 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -615,22 +615,22 @@ procedure $YieldHavoc(this: ref, rds: Set BoxType, nw: Set BoxType); read($Heap, $o, $f) == read(old($Heap), $o, $f));
ensures $HeapSucc(old($Heap), $Heap);
-// havoc everything in $Heap, except rds-mod-{this}
-procedure $IterHavoc0(this: ref, rds: Set BoxType, mod: Set BoxType);
+// havoc everything in $Heap, except rds-modi-{this}
+procedure $IterHavoc0(this: ref, rds: Set BoxType, modi: Set BoxType);
modifies $Heap;
ensures (forall<alpha> $o: ref, $f: Field alpha :: { read($Heap, $o, $f) }
$o != null && read(old($Heap), $o, alloc) ==>
- rds[$Box($o)] && !mod[$Box($o)] && $o != this ==>
+ rds[$Box($o)] && !modi[$Box($o)] && $o != this ==>
read($Heap, $o, $f) == read(old($Heap), $o, $f));
ensures $HeapSucc(old($Heap), $Heap);
-// havoc $Heap at {this}+mod+nw
-procedure $IterHavoc1(this: ref, mod: Set BoxType, nw: Set BoxType);
+// havoc $Heap at {this}+modi+nw
+procedure $IterHavoc1(this: ref, modi: Set BoxType, nw: Set BoxType);
modifies $Heap;
ensures (forall<alpha> $o: ref, $f: Field alpha :: { read($Heap, $o, $f) }
$o != null && read(old($Heap), $o, alloc) ==>
read($Heap, $o, $f) == read(old($Heap), $o, $f) ||
- $o == this || mod[$Box($o)] || nw[$Box($o)]);
+ $o == this || modi[$Box($o)] || nw[$Box($o)]);
ensures $HeapSucc(old($Heap), $Heap);
procedure $IterCollectNewObjects(prevHeap: HeapType, newHeap: HeapType, this: ref, NW: Field (Set BoxType))
|