diff options
author | rustanleino <unknown> | 2010-05-06 23:35:04 +0000 |
---|---|---|
committer | rustanleino <unknown> | 2010-05-06 23:35:04 +0000 |
commit | ac513a64b44e33847f84750c8382f0aa2f4ed745 (patch) | |
tree | c4d5429738810b1b9965e10abd5c09dd3c5da0b6 /Binaries/DafnyPrelude.bpl | |
parent | a2f70f46e1a4dfb513df45657178399269cec67d (diff) |
Dafny:
* Recoded frame axioms to be more goal directed
* Added Main test driver to Test/VSI-Benchmarks/b2.dfy
Diffstat (limited to 'Binaries/DafnyPrelude.bpl')
-rw-r--r-- | Binaries/DafnyPrelude.bpl | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 04da0993..d9ff2f63 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -227,6 +227,10 @@ const unique alloc: Field bool; function DeclType<T>(Field T) returns (ClassName);
function $HeapSucc(HeapType, HeapType) returns (bool);
+axiom (forall<alpha> h: HeapType, r: ref, f: Field alpha, x: alpha :: { h[r,f:=x] }
+ $HeapSucc(h, 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));
axiom (forall h: HeapType, k: HeapType :: { $HeapSucc(h,k) }
$HeapSucc(h,k) ==> (forall o: ref :: { k[o,alloc] } h[o,alloc] ==> k[o,alloc]));
|