Improved axiom that knows that array-to-sequence converstion depends only on those heap location that hold the array elements

1 files changed, 13 insertions, 0 deletions

diff --git a/Test/dafny0/Array.dfy b/Test/dafny0/Array.dfy
index 1b41267e..f6477708 100644
--- a/Test/dafny0/Array.dfy
+++ b/Test/dafny0/Array.dfy
@@ -137,6 +137,19 @@ class A {
     a != null && 0 <= j && j <= a.Length &&

     a[j..j] == []

   }

+

+  predicate Q0(s: seq<int>)

+  predicate Q1(s: seq<int>)

+  method FrameTest(a: array<int>) returns (b: array<int>)

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

+  {

+    b := CreateArray(a);

+    assert Q0(a[..]);  // this should still be known after the call to CreateArray

+    assert Q1(b[..]);

+  }

+  method CreateArray(a: array<int>) returns (b: array<int>)

+    requires a != null;

+    ensures fresh(b) && Q1(b[..]);

 }

 

 type B;