Improved power of axioms Seq#FromArray

3 files changed, 119 insertions, 5 deletions

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 91d8a01a..eea23383 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -872,7 +872,10 @@ axiom (forall<T> s: Seq T, n: int :: { Seq#Length(Seq#Take(s,n)) }
   0 <= n ==>

     (n <= Seq#Length(s) ==> Seq#Length(Seq#Take(s,n)) == n) &&

     (Seq#Length(s) < n ==> Seq#Length(Seq#Take(s,n)) == Seq#Length(s)));

-axiom (forall<T> s: Seq T, n: int, j: int :: { Seq#Index(Seq#Take(s,n), j) } {:weight 25}

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

+  {:weight 25}

+  { Seq#Index(Seq#Take(s,n), j) }

+  { Seq#Index(s, j), Seq#Take(s,n) }

   0 <= j && j < n && j < Seq#Length(s) ==>

     Seq#Index(Seq#Take(s,n), j) == Seq#Index(s, j));

 

@@ -881,9 +884,16 @@ axiom (forall<T> s: Seq T, n: int :: { Seq#Length(Seq#Drop(s,n)) }
   0 <= n ==>

     (n <= Seq#Length(s) ==> Seq#Length(Seq#Drop(s,n)) == Seq#Length(s) - n) &&

     (Seq#Length(s) < n ==> Seq#Length(Seq#Drop(s,n)) == 0));

-axiom (forall<T> s: Seq T, n: int, j: int :: { Seq#Index(Seq#Drop(s,n), j) } {:weight 25}

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

+  {:weight 25}

+  { Seq#Index(Seq#Drop(s,n), j) }

   0 <= n && 0 <= j && j < Seq#Length(s)-n ==>

     Seq#Index(Seq#Drop(s,n), j) == Seq#Index(s, j+n));

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

+  {:weight 25}

+  { Seq#Index(s, k), Seq#Drop(s,n) }

+  0 <= n && n <= k && k < Seq#Length(s) ==>

+    Seq#Index(Seq#Drop(s,n), k-n) == Seq#Index(s, k));

 

 axiom (forall<T> s, t: Seq T ::

   { Seq#Append(s, t) }

@@ -894,9 +904,18 @@ function Seq#FromArray(h: Heap, a: ref): Seq Box;
 axiom (forall h: Heap, a: ref ::

   { Seq#Length(Seq#FromArray(h,a)) }

   Seq#Length(Seq#FromArray(h, a)) == _System.array.Length(a));

-axiom (forall h: Heap, a: ref, i: int ::

-  { Seq#Index(Seq#FromArray(h, a): Seq Box, i) }

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

+axiom (forall h: Heap, a: ref :: 

+  { Seq#FromArray(h, a) } 

+  (forall i: int ::

+    // it's important to include both triggers, so that assertions about the

+    // the relation between the array and the sequence can be proved in either

+    // direction

+    { read(h, a, IndexField(i)) }

+    { Seq#Index(Seq#FromArray(h, a): Seq Box, i) } 

+    0 <= i &&

+    i < Seq#Length(Seq#FromArray(h, a))  // this will trigger the previous axiom to get a connection with _System.array.Length(a)

+    ==>

+    Seq#Index(Seq#FromArray(h, a), i) == read(h, a, IndexField(i))));

 axiom (forall h0, h1: Heap, a: ref ::

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

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

diff --git a/Test/dafny0/SeqFromArray.dfy b/Test/dafny0/SeqFromArray.dfy
new file mode 100644
index 00000000..d4c98424
--- /dev/null
+++ b/Test/dafny0/SeqFromArray.dfy
@@ -0,0 +1,90 @@
+// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+method Main() { }

+

+method H(a: array<int>, c: array<int>, n: nat, j: nat)

+  requires a != null && c != null

+  requires j < n == a.Length == c.Length

+{

+  var A := a[..];

+  var C := c[..];

+

+  if {

+    case A[j] == C[j] =>

+      assert a[j] == c[j];

+    case forall i :: 0 <= i < n ==> A[i] == C[i] =>

+      assert a[j] == c[j];

+    case forall i :: 0 <= i < n ==> A[i] == C[i] =>

+      assert forall i :: 0 <= i < n ==> a[i] == c[i];

+    case A == C =>

+      assert forall i :: 0 <= i < n ==> A[i] == C[i];

+    case A == C =>

+      assert forall i :: 0 <= i < n ==> a[i] == c[i];

+    case true =>

+  }

+}

+

+method K(a: array<int>, c: array<int>, n: nat)

+  requires a != null && c != null

+  requires n <= a.Length && n <= c.Length

+{

+  var A := a[..n];

+  var C := c[..n];

+  if {

+    case A == C =>

+      assert forall i :: 0 <= i < n ==> A[i] == C[i];

+    case A == C =>

+      assert forall i :: 0 <= i < n ==> a[i] == c[i];

+    case true =>

+  }

+}

+

+method L(a: array<int>, c: array<int>, n: nat)

+  requires a != null && c != null

+  requires n <= a.Length == c.Length

+{

+  var A := a[n..];

+  var C := c[n..];

+  var h := a.Length - n;

+  if {

+    case A == C =>

+      assert forall i :: 0 <= i < h ==> A[i] == C[i];

+    case A == C =>

+      assert forall i :: 0 <= i < h ==> a[n+i] == c[n+i];

+    case true =>

+  }

+}

+

+method M(a: array<int>, c: array<int>, m: nat, n: nat, k: nat, l: nat)

+  requires a != null && c != null

+  requires k + m <= a.Length;

+  requires l + n <= c.Length

+{

+  if {

+    case true =>

+      var A := a[k..k+m];

+      var C := c[l..l+n];

+      if A == C {

+        if * {

+          assert m == n;

+        } else if * {

+          assert forall i :: 0 <= i < n ==> A[i] == C[i];

+        } else if * {

+          assert forall i :: k <= i < k+n ==> A[i-k] == C[i-k];

+        } else if * {

+          assert forall i :: 0 <= i < n ==> A[i] == a[k+i];

+        } else if * {

+          assert forall i :: 0 <= i < n ==> C[i] == c[l+i];

+        } else if * {

+          assert forall i :: 0 <= i < n ==> a[k+i] == c[l+i];

+        }

+      } 

+    case l+k+m <= c.Length && forall i :: k <= i < k+m ==> a[i] == c[l+i] =>

+      assert a[k..k+m] == c[l+k..l+k+m];

+    case l+m <= c.Length && forall i :: 0 <= i < m ==> a[i] == c[l+i] =>

+      assert a[..m] == c[l..l+m];

+    case l+a.Length <= c.Length && forall i :: k <= i < a.Length ==> a[i] == c[l+i] =>

+      assert a[k..] == c[l+k..l+a.Length];

+  }

+}

diff --git a/Test/dafny0/SeqFromArray.dfy.expect b/Test/dafny0/SeqFromArray.dfy.expect
new file mode 100644
index 00000000..af845d3e
--- /dev/null
+++ b/Test/dafny0/SeqFromArray.dfy.expect
@@ -0,0 +1,5 @@
+

+Dafny program verifier finished with 10 verified, 0 errors

+Program compiled successfully

+Running...

+