summaryrefslogtreecommitdiff
path: root/Binaries
diff options
context:
space:
mode:
authorGravatar Rustan Leino <unknown>2014-03-20 15:49:02 -0700
committerGravatar Rustan Leino <unknown>2014-03-20 15:49:02 -0700
commit643f5f55677d454c95286654594504ef2c66fe8f (patch)
treebef8e8dba3438399541535d6b3c7e5bd9be37673 /Binaries
parent912adaa06621d89a47460d6a6befd8809ded5c85 (diff)
Added axiom to transfer array element-type information onto the elements themselves.
Other serendipitous axiom improvements.
Diffstat (limited to 'Binaries')
-rw-r--r--Binaries/DafnyPrelude.bpl21
1 files changed, 20 insertions, 1 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index b6fce82c..0662d12b 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -488,6 +488,7 @@ axiom (forall<T> x: T :: { $Box(x) } $Unbox($Box(x)) == x);
axiom (forall b: BoxType :: { $Unbox(b): int } $Box($Unbox(b): int) == b);
axiom (forall b: BoxType :: { $Unbox(b): ref } $Box($Unbox(b): ref) == b);
axiom (forall b: BoxType :: { $Unbox(b): Set BoxType } $Box($Unbox(b): Set BoxType) == b);
+axiom (forall b: BoxType :: { $Unbox(b): MultiSet BoxType } $Box($Unbox(b): MultiSet BoxType) == b);
axiom (forall b: BoxType :: { $Unbox(b): Seq BoxType } $Box($Unbox(b): Seq BoxType) == b);
axiom (forall b: BoxType :: { $Unbox(b): Map BoxType BoxType } $Box($Unbox(b): Map BoxType BoxType) == b);
axiom (forall b: BoxType :: { $Unbox(b): DatatypeType } $Box($Unbox(b): DatatypeType) == b);
@@ -583,6 +584,16 @@ axiom (forall f: Field BoxType, i: int :: { MultiIndexField(f,i) }
MultiIndexField_Inverse0(MultiIndexField(f,i)) == f &&
MultiIndexField_Inverse1(MultiIndexField(f,i)) == i);
+axiom (forall h: HeapType, a: ref, j: int ::
+ { $Unbox(read(h, a, IndexField(j))) : ref }
+ $IsGoodHeap(h) &&
+ a != null && read(h, a, alloc) &&
+ 0 <= j && j < _System.array.Length(a)
+ // It would be nice also to restrict this axiom to an 'a' whose type is
+ // really a reference type.
+ ==>
+ $Unbox(read(h, a, IndexField(j))) : ref == null ||
+ dtype($Unbox(read(h, a, IndexField(j))) : ref) == TypeParams(a, 0));
function DeclType<T>(Field T): ClassName;
@@ -664,12 +675,20 @@ axiom (forall r: ref, f: Field BoxType, h: HeapType ::
axiom (forall h: HeapType, r: ref, j: int ::
{ read(h, r, IndexField(j)) }
- $IsGoodHeap(h) && r != null && read(h, r, alloc)
+ $IsGoodHeap(h) && r != null && read(h, r, alloc) &&
+ 0 <= j && j < _System.array.Length(r)
==>
GenericAlloc(read(h, r, IndexField(j)), h));
axiom (forall h: HeapType, r: ref, m: Field BoxType, j: int ::
{ read(h, r, MultiIndexField(m, j)) }
$IsGoodHeap(h) && r != null && read(h, r, alloc)
+ // It would be best also to constrain MultiIndexField(m,j) to produce
+ // a proper field (that is, to refer to an array element within
+ // bounds. However, since the LengthX fields of multi-dimentional
+ // are produced on the fly, adding them would require more work.
+ // Thus, the model to keep in mind is that MultiIndexField then
+ // produces a field who value, when dereferenced for array 'r',
+ // is a box that has the desired allocation properties.
==>
GenericAlloc(read(h, r, MultiIndexField(m, j)), h));