From ac513a64b44e33847f84750c8382f0aa2f4ed745 Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Thu, 6 May 2010 23:35:04 +0000
Subject: Dafny: * Recoded frame axioms to be more goal directed * Added Main
 test driver to Test/VSI-Benchmarks/b2.dfy

---
 Binaries/DafnyPrelude.bpl | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'Binaries')

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]));
 
-- 
cgit v1.2.3