From 6cdef59ade53baddabf304a3ada5294a2bfdc99c Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Fri, 3 Jan 2014 13:09:59 -0800
Subject: Embellished axioms about GenericAlloc and DtAlloc.

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

(limited to 'Binaries')

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 6b9cc3b6..d4e7575e 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -610,9 +610,9 @@ axiom (forall h, k: HeapType, d: DatatypeType ::
 function GenericAlloc(BoxType, HeapType): bool;
 axiom (forall h: HeapType, k: HeapType, d: BoxType ::
   { $HeapSucc(h, k), GenericAlloc(d, h) }
-  { $HeapSucc(h, k), GenericAlloc(d, k) }
   $HeapSucc(h, k) ==> GenericAlloc(d, h) ==> GenericAlloc(d, k));
 // GenericAlloc ==>
+//references
 axiom (forall b: BoxType, h: HeapType ::
   { GenericAlloc(b, h), h[$Unbox(b): ref, alloc] }
   GenericAlloc(b, h) ==>
@@ -641,9 +641,10 @@ axiom (forall b: BoxType, h: HeapType, t: BoxType ::
   { GenericAlloc(b, h), ($Unbox(b): Set BoxType)[t] }
   GenericAlloc(b, h) && ($Unbox(b): Set BoxType)[t] ==>
   GenericAlloc(t, h));
+//datatypes
 axiom (forall b: BoxType, h: HeapType ::
-  { GenericAlloc(b, h), DtType($Unbox(b): DatatypeType) }
-  GenericAlloc(b, h) ==> DtAlloc($Unbox(b): DatatypeType, h));
+  { GenericAlloc(b, h), DtAlloc($Unbox(b): DatatypeType, h) }
+  GenericAlloc(b, h) <==> DtAlloc($Unbox(b): DatatypeType, h));
 // ==> GenericAlloc
 axiom (forall b: bool, h: HeapType ::
   $IsGoodHeap(h) ==> GenericAlloc($Box(b), h));
-- 
cgit v1.2.3