Added axiom to transfer array element-type information onto the elements themselves.

Other serendipitous axiom improvements.

3 files changed, 41 insertions, 5 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));

 

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 06f4e9e9..987fc28b 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -470,6 +470,12 @@ ResolutionErrors.dfy(773,23): Error: function calls are allowed only in specific
 ResolutionErrors.dfy(783,4): Error: ghost variables are allowed only in specification contexts

 ResolutionErrors.dfy(794,36): Error: ghost variables are allowed only in specification contexts

 ResolutionErrors.dfy(803,17): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')

+ResolutionErrors.dfy(817,6): Error: RHS (of type B) not assignable to LHS (of type object)

+ResolutionErrors.dfy(818,6): Error: RHS (of type int) not assignable to LHS (of type object)

+ResolutionErrors.dfy(819,6): Error: RHS (of type B) not assignable to LHS (of type object)

+ResolutionErrors.dfy(824,6): Error: RHS (of type G) not assignable to LHS (of type object)

+ResolutionErrors.dfy(825,6): Error: RHS (of type Dt) not assignable to LHS (of type object)

+ResolutionErrors.dfy(826,6): Error: RHS (of type CoDt) not assignable to LHS (of type object)

 ResolutionErrors.dfy(427,2): Error: More than one default constructor

 ResolutionErrors.dfy(48,13): Error: 'this' is not allowed in a 'static' context

 ResolutionErrors.dfy(109,9): Error: ghost variables are allowed only in specification contexts

@@ -543,7 +549,7 @@ ResolutionErrors.dfy(541,20): Error: ghost variables are allowed only in specifi
 ResolutionErrors.dfy(543,7): Error: let-such-that expressions are allowed only in ghost contexts

 ResolutionErrors.dfy(544,18): Error: unresolved identifier: w

 ResolutionErrors.dfy(651,11): Error: lemmas are not allowed to have modifies clauses

-114 resolution/type errors detected in ResolutionErrors.dfy

+120 resolution/type errors detected in ResolutionErrors.dfy

 

 -------------------- ParseErrors.dfy --------------------

 ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator

@@ -669,7 +675,7 @@ Execution trace:
     (0,0): anon2

     (0,0): anon6_Then

 

-Dafny program verifier finished with 34 verified, 20 errors

+Dafny program verifier finished with 41 verified, 20 errors

 

 -------------------- MultiDimArray.dfy --------------------

 MultiDimArray.dfy(53,21): Error: assertion violation

diff --git a/Test/dafny0/Array.dfy b/Test/dafny0/Array.dfy
index 4cd06e53..47bfe489 100644
--- a/Test/dafny0/Array.dfy
+++ b/Test/dafny0/Array.dfy
@@ -258,16 +258,27 @@ class Cdefg<T> {
 

 class MyClass {

   ghost var Repr: set<object>;

+  predicate Valid()

+    reads this, Repr;

 }

 

-method AllocationBusinessA(a: array<MyClass>, j: int)

+method AllocationBusiness0(a: array<MyClass>, j: int)

   requires a != null && 0 <= j < a.Length;

   requires a[j] != null;

 {

   var c := new MyClass;

   assert c !in a[j].Repr;  // the proof requires allocation axioms for arrays

 }

-method AllocationBusinessB(a: array2<MyClass>, i: int, j: int)

+

+method AllocationBusiness1(a: array<MyClass>, j: int)

+  requires a != null && 0 <= j < a.Length;

+  requires a[j] != null && a[j].Valid();

+{

+  var c := new MyClass;

+  assert a[j].Valid();  // the allocation should not have invalidated the validity of a[j]

+}

+

+method AllocationBusiness2(a: array2<MyClass>, i: int, j: int)

   requires a != null && 0 <= i < a.Length0 && 0 <= j < a.Length1;

   requires a[i,j] != null;

 {