diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-10-03 13:31:25 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-10-03 13:31:25 -0700 |
| commit | 3db6f751759a687b63dfe9998138239b890cafe4 (patch) | |
| tree | 5a637d4da58c14a7ed565a8fb1f28b26cc78ac80 /Binaries | |
| parent | 4df80035e37102d59f9084de62261eb783127856 (diff) | |
Dafny: more part of verifying iterators
Diffstat (limited to 'Binaries')
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 26 |
1 files changed, 22 insertions, 4 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 572a1e29..02d0f344 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -606,14 +606,32 @@ axiom (forall h: HeapType, k: HeapType :: { $HeapSucc(h,k) } // -- Useful macros ----------------------------------------------
// ---------------------------------------------------------------
-// havoc $Heap \ {this} \ S
-procedure {:inline} $YieldHavoc(this: ref, S: Set BoxType);
+// havoc everything in $Heap, except {this}+rds+nw
+procedure $YieldHavoc(this: ref, rds: 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) ==>
+ $o == this || rds[$Box($o)] || nw[$Box($o)] ==>
+ 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);
+ 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 ==>
+ 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);
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 ||
- S[$Box($o)]);
+ $o == this || mod[$Box($o)] || nw[$Box($o)]);
+ ensures $HeapSucc(old($Heap), $Heap);
// ---------------------------------------------------------------
// -- Non-determinism --------------------------------------------
|