diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-06-01 10:11:59 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-06-01 10:11:59 -0700 |
| commit | 15fbe91aaf4a29f310f613ee53eb2058ba18dfef (patch) | |
| tree | f7bd60b8410a3ca3c6e1bfad26df63362d5caf39 /Binaries | |
| parent | aaff53080fb15b89134ab81880d89af31d16896e (diff) | |
Dafny: fixed soundness problem with HeapSucc axiom
Diffstat (limited to 'Binaries')
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index a358e3c0..30992d46 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -347,6 +347,7 @@ var $Heap: HeapType where $IsGoodHeap($Heap); function $HeapSucc(HeapType, HeapType): bool;
axiom (forall<alpha> h: HeapType, r: ref, f: Field alpha, x: alpha :: { update(h, r, f, x) }
+ $IsGoodHeap(update(h, r, f, x)) ==>
$HeapSucc(h, update(h, r, f, x)));
axiom (forall a,b,c: HeapType :: { $HeapSucc(a,b), $HeapSucc(b,c) }
$HeapSucc(a,b) && $HeapSucc(b,c) ==> $HeapSucc(a,c));
|