Dafny: added translation of Assign case of the parallel statement

Dafny: discovered and fixed bug in no-overlap check of multi-dimensional array update, and changed previously incorrect MatrixFun.dfy test case (the new version is also a more efficient program)

1 files changed, 5 insertions, 5 deletions

diff --git a/Test/dafny1/MatrixFun.dfy b/Test/dafny1/MatrixFun.dfy
index 5c69ac50..8f9d87ed 100644
--- a/Test/dafny1/MatrixFun.dfy
+++ b/Test/dafny1/MatrixFun.dfy
@@ -34,14 +34,14 @@ method MirrorImage<T>(m: array2<T>)
 method Flip<T>(m: array2<T>)

   requires m != null && m.Length0 == m.Length1;

   modifies m;

-  ensures (forall i,j :: 0 <= i && i < m.Length0 && 0 <= j && j < m.Length1 ==> m[i,j] == old(m[j,i]));

+  ensures (forall i,j :: 0 <= i < m.Length0 && 0 <= j < m.Length1 ==> m[i,j] == old(m[j,i]));

 {

   var N := m.Length0;

   var a := 0;

-  var b := 0;

+  var b := 1;

   while (a != N)

-    invariant a <= b && b <= N;

-    invariant (forall i,j :: 0 <= i && i <= j && j < N ==>

+    invariant a < b <= N || (a == N && b == N+1);

+    invariant (forall i,j :: 0 <= i <= j < N ==>

                 (if i < a || (i == a && j < b)

                   then m[i,j] == old(m[j,i]) && m[j,i] == old(m[i,j])

                   else m[i,j] == old(m[i,j]) && m[j,i] == old(m[j,i])));

@@ -51,7 +51,7 @@ method Flip<T>(m: array2<T>)
       m[a,b], m[b,a] := m[b,a], m[a,b];

       b := b + 1;

     } else {

-      a := a + 1;  b := a;

+      a := a + 1;  b := a + 1;

     }

   }

 }