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 | 7f2783976dbdfe1392e40cf749922372f32e7ed7 (patch) | |
| tree | 0b867f4b6c284aa3bfc750fcc9e8c7d78a591732 /Binaries/DafnyPrelude.bpl | |
| parent | 06c6bfd2134bd9412b909d77887673b47a88b72b (diff) | |
Dafny: more part of verifying iterators
Diffstat (limited to 'Binaries/DafnyPrelude.bpl')
| -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 --------------------------------------------
|