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

3 files changed, 36 insertions, 17 deletions

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 224c5ffd..3d993797 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -358,9 +358,13 @@ axiom (forall h: HeapType, a: ref ::
     Seq#Length(Seq#FromArray(h, a)) == _System.array.Length(a));

 axiom (forall h: HeapType, a: ref :: { Seq#FromArray(h,a): Seq BoxType }

    (forall i: int :: 0 <= i && i < Seq#Length(Seq#FromArray(h, a)) ==> Seq#Index(Seq#FromArray(h, a), i) == read(h, a, IndexField(i))));

-axiom (forall<alpha> h: HeapType, o: ref, f: Field alpha, v: alpha, a: ref ::

-  { Seq#FromArray(update(h, o, f, v), a) }

-    o != a ==> Seq#FromArray(update(h, o, f, v), a) == Seq#FromArray(h, a) );

+axiom (forall h0, h1: HeapType, a: ref ::

+  { Seq#FromArray(h1, a), $HeapSucc(h0, h1) }

+  $IsGoodHeap(h0) && $IsGoodHeap(h1) && $HeapSucc(h0, h1) &&

+  (forall i: int ::

+    0 <= i && i < _System.array.Length(a) ==> read(h0, a, IndexField(i)) == read(h1, a, IndexField(i)))

+  ==>

+  Seq#FromArray(h0, a) == Seq#FromArray(h1, a));

 axiom (forall h: HeapType, i: int, v: BoxType, a: ref ::

   { Seq#FromArray(update(h, a, IndexField(i), v), a) }

     0 <= i && i < _System.array.Length(a) ==> Seq#FromArray(update(h, a, IndexField(i), v), a) == Seq#Update(Seq#FromArray(h, a), i, v) );

@@ -389,7 +393,9 @@ axiom (forall<T> s: Seq T, i: int, v: T, n: int ::
 // Extension axiom, triggers only on Takes from arrays.

 axiom (forall h: HeapType, a: ref, n0, n1: int ::

   { Seq#Take(Seq#FromArray(h, a), n0), Seq#Take(Seq#FromArray(h, a), n1) }

-    n0 + 1 == n1 && 0 <= n0 && n1 <= _System.array.Length(a) ==> Seq#Take(Seq#FromArray(h, a), n1) == Seq#Build(Seq#Take(Seq#FromArray(h, a), n0), read(h, a, IndexField(n0): Field BoxType)) );

+    0 <= n0 && n0 + 1 == n1 && n1 <= _System.array.Length(a) ==>

+      Seq#Take(Seq#FromArray(h, a), n1) ==

+      Seq#Build(Seq#Take(Seq#FromArray(h, a), n0), read(h, a, IndexField(n0): Field BoxType)) );

 // drop commutes with build.

 axiom (forall<T> s: Seq T, v: T, n: int ::

   { Seq#Drop(Seq#Build(s, v), n) }

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;

diff --git a/Test/dafny0/Array.dfy.expect b/Test/dafny0/Array.dfy.expect
index 86a19c51..081fd258 100644
--- a/Test/dafny0/Array.dfy.expect
+++ b/Test/dafny0/Array.dfy.expect
@@ -61,47 +61,47 @@ Execution trace:
     (0,0): anon10_Then

     (0,0): anon11_Then

     (0,0): anon12_Else

-Array.dfy(150,6): Error: insufficient reads clause to read array element

+Array.dfy(163,6): Error: insufficient reads clause to read array element

 Execution trace:

     (0,0): anon0

     (0,0): anon7_Else

     (0,0): anon8_Then

     (0,0): anon9_Then

-Array.dfy(158,6): Error: insufficient reads clause to read array element

+Array.dfy(171,6): Error: insufficient reads clause to read array element

 Execution trace:

     (0,0): anon0

     (0,0): anon7_Else

     (0,0): anon8_Then

     (0,0): anon9_Then

-Array.dfy(174,6): Error: assignment may update an array element not in the enclosing context's modifies clause

+Array.dfy(187,6): Error: assignment may update an array element not in the enclosing context's modifies clause

 Execution trace:

     (0,0): anon0

-Array.dfy(181,6): Error: assignment may update an array element not in the enclosing context's modifies clause

+Array.dfy(194,6): Error: assignment may update an array element not in the enclosing context's modifies clause

 Execution trace:

     (0,0): anon0

-Array.dfy(206,1): Error BP5003: A postcondition might not hold on this return path.

-Array.dfy(205,11): Related location: This is the postcondition that might not hold.

+Array.dfy(219,1): Error BP5003: A postcondition might not hold on this return path.

+Array.dfy(218,11): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

-Array.dfy(230,1): Error BP5003: A postcondition might not hold on this return path.

-Array.dfy(229,11): Related location: This is the postcondition that might not hold.

+Array.dfy(243,1): Error BP5003: A postcondition might not hold on this return path.

+Array.dfy(242,11): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

-Array.dfy(236,1): Error BP5003: A postcondition might not hold on this return path.

-Array.dfy(235,11): Related location: This is the postcondition that might not hold.

+Array.dfy(249,1): Error BP5003: A postcondition might not hold on this return path.

+Array.dfy(248,11): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

-Array.dfy(251,10): Error: value assigned to a nat must be non-negative

+Array.dfy(264,10): Error: value assigned to a nat must be non-negative

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Then

     (0,0): anon2

     (0,0): anon6_Then

-Array.dfy(252,5): Error: value assigned to a nat must be non-negative

+Array.dfy(265,5): Error: value assigned to a nat must be non-negative

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Then

     (0,0): anon2

     (0,0): anon6_Then

 

-Dafny program verifier finished with 41 verified, 20 errors

+Dafny program verifier finished with 46 verified, 20 errors