Dafny: Translate general LHSs for var and := (not yet for call, no compilation yet)

5 files changed, 135 insertions, 64 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index c82d3803..75025b2f 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -85,7 +85,7 @@ TypeTests.dfy(87,8): Error: sorry, cannot instantiate 'array' type with a subran
 NatTypes.dfy(7,5): Error: value assigned to a nat must be non-negative

 Execution trace:

     (0,0): anon0

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

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

 Execution trace:

     (0,0): anon0

     NatTypes.dfy(19,3): anon10_LoopHead

@@ -111,7 +111,7 @@ Execution trace:
     (0,0): anon0

     (0,0): anon5_Else

     (0,0): anon6_Then

-NatTypes.dfy(86,16): Error: value assigned to a nat must be non-negative

+NatTypes.dfy(86,19): Error: value assigned to a nat must be non-negative

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

@@ -450,7 +450,7 @@ ParseErrors.dfy(18,18): error: chaining not allowed from the previous operator
 9 parse errors detected in ParseErrors.dfy

 

 -------------------- Array.dfy --------------------

-Array.dfy(10,12): Error: assignment may update an array element not in the enclosing method's modifies clause

+Array.dfy(10,8): Error: assignment may update an array element not in the enclosing method's modifies clause

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Then

@@ -465,13 +465,13 @@ Execution trace:
 Array.dfy(48,20): Error: assertion violation

 Execution trace:

     (0,0): anon0

-Array.dfy(56,12): Error: assignment may update an array element not in the enclosing method's modifies clause

+Array.dfy(56,8): Error: assignment may update an array element not in the enclosing method's modifies clause

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Then

     (0,0): anon2

     (0,0): anon6_Then

-Array.dfy(63,12): Error: assignment may update an array element not in the enclosing method's modifies clause

+Array.dfy(63,8): Error: assignment may update an array element not in the enclosing method's modifies clause

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Then

@@ -490,10 +490,10 @@ Execution trace:
     (0,0): anon7_Else

     (0,0): anon8_Then

     (0,0): anon9_Then

-Array.dfy(131,10): Error: assignment may update an array element not in the enclosing method's modifies clause

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

 Execution trace:

     (0,0): anon0

-Array.dfy(138,10): Error: assignment may update an array element not in the enclosing method's modifies clause

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

 Execution trace:

     (0,0): anon0

 

@@ -598,8 +598,31 @@ Execution trace:
     (0,0): anon10

     Basics.dfy(66,95): anon18_Else

     (0,0): anon12

+Basics.dfy(86,16): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon10_Then

+Basics.dfy(99,12): Error: left-hand sides 0 and 1 may refer to the same location

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3

+    (0,0): anon11_Else

+    (0,0): anon6

+    (0,0): anon12_Then

+Basics.dfy(105,10): Error: left-hand sides 0 and 1 may refer to the same location

+Execution trace:

+    (0,0): anon0

+    (0,0): anon10_Then

+    (0,0): anon3

+    (0,0): anon11_Then

+    (0,0): anon6

+    (0,0): anon12_Then

+    (0,0): anon9

+Basics.dfy(119,10): Error: left-hand sides 0 and 1 may refer to the same location

+Execution trace:

+    (0,0): anon0

 

-Dafny program verifier finished with 7 verified, 2 errors

+Dafny program verifier finished with 9 verified, 6 errors

 

 -------------------- ControlStructures.dfy --------------------

 ControlStructures.dfy(5,3): Error: missing case in case statement: Blue

@@ -638,112 +661,112 @@ ControlStructures.dfy(72,3): Error: alternative cases fail to cover all possibil
 Execution trace:

     (0,0): anon0

     (0,0): anon5_Else

-ControlStructures.dfy(218,18): Error: assertion violation

+ControlStructures.dfy(215,18): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    ControlStructures.dfy(197,3): anon62_LoopHead

+    ControlStructures.dfy(194,3): anon62_LoopHead

     (0,0): anon62_LoopBody

-    ControlStructures.dfy(197,3): anon63_Else

+    ControlStructures.dfy(194,3): anon63_Else

     (0,0): anon3

-    ControlStructures.dfy(197,3): anon64_Else

+    ControlStructures.dfy(194,3): anon64_Else

     (0,0): anon5

-    ControlStructures.dfy(201,5): anon65_LoopHead

+    ControlStructures.dfy(198,5): anon65_LoopHead

     (0,0): anon65_LoopBody

-    ControlStructures.dfy(201,5): anon66_Else

+    ControlStructures.dfy(198,5): anon66_Else

     (0,0): anon8

-    ControlStructures.dfy(201,5): anon67_Else

+    ControlStructures.dfy(198,5): anon67_Else

     (0,0): anon10

     (0,0): anon71_Then

-    ControlStructures.dfy(213,9): anon72_LoopHead

+    ControlStructures.dfy(210,9): anon72_LoopHead

     (0,0): anon72_LoopBody

-    ControlStructures.dfy(213,9): anon73_Else

+    ControlStructures.dfy(210,9): anon73_Else

     (0,0): anon20

     (0,0): anon74_Then

     (0,0): anon29

-ControlStructures.dfy(235,21): Error: assertion violation

+ControlStructures.dfy(232,21): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    ControlStructures.dfy(197,3): anon62_LoopHead

+    ControlStructures.dfy(194,3): anon62_LoopHead

     (0,0): anon62_LoopBody

-    ControlStructures.dfy(197,3): anon63_Else

+    ControlStructures.dfy(194,3): anon63_Else

     (0,0): anon3

-    ControlStructures.dfy(197,3): anon64_Else

+    ControlStructures.dfy(194,3): anon64_Else

     (0,0): anon5

-    ControlStructures.dfy(201,5): anon65_LoopHead

+    ControlStructures.dfy(198,5): anon65_LoopHead

     (0,0): anon65_LoopBody

-    ControlStructures.dfy(201,5): anon66_Else

+    ControlStructures.dfy(198,5): anon66_Else

     (0,0): anon8

-    ControlStructures.dfy(201,5): anon67_Else

+    ControlStructures.dfy(198,5): anon67_Else

     (0,0): anon10

     (0,0): anon71_Then

-    ControlStructures.dfy(213,9): anon72_LoopHead

+    ControlStructures.dfy(210,9): anon72_LoopHead

     (0,0): anon72_LoopBody

-    ControlStructures.dfy(213,9): anon73_Else

+    ControlStructures.dfy(210,9): anon73_Else

     (0,0): anon20

-    ControlStructures.dfy(213,9): anon74_Else

+    ControlStructures.dfy(210,9): anon74_Else

     (0,0): anon22

     (0,0): anon75_Then

     (0,0): after_4

-    ControlStructures.dfy(224,7): anon77_LoopHead

+    ControlStructures.dfy(221,7): anon77_LoopHead

     (0,0): anon77_LoopBody

-    ControlStructures.dfy(224,7): anon78_Else

+    ControlStructures.dfy(221,7): anon78_Else

     (0,0): anon33

-    ControlStructures.dfy(224,7): anon79_Else

+    ControlStructures.dfy(221,7): anon79_Else

     (0,0): anon35

     (0,0): anon81_Then

     (0,0): anon38

     (0,0): after_9

     (0,0): anon86_Then

     (0,0): anon53

-ControlStructures.dfy(238,30): Error: assertion violation

+ControlStructures.dfy(235,30): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    ControlStructures.dfy(197,3): anon62_LoopHead

+    ControlStructures.dfy(194,3): anon62_LoopHead

     (0,0): anon62_LoopBody

-    ControlStructures.dfy(197,3): anon63_Else

+    ControlStructures.dfy(194,3): anon63_Else

     (0,0): anon3

-    ControlStructures.dfy(197,3): anon64_Else

+    ControlStructures.dfy(194,3): anon64_Else

     (0,0): anon5

-    ControlStructures.dfy(201,5): anon65_LoopHead

+    ControlStructures.dfy(198,5): anon65_LoopHead

     (0,0): anon65_LoopBody

-    ControlStructures.dfy(201,5): anon66_Else

+    ControlStructures.dfy(198,5): anon66_Else

     (0,0): anon8

-    ControlStructures.dfy(201,5): anon67_Else

+    ControlStructures.dfy(198,5): anon67_Else

     (0,0): anon10

     (0,0): anon68_Then

     (0,0): after_5

     (0,0): anon87_Then

     (0,0): anon88_Then

     (0,0): anon58

-ControlStructures.dfy(241,17): Error: assertion violation

+ControlStructures.dfy(238,17): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    ControlStructures.dfy(197,3): anon62_LoopHead

+    ControlStructures.dfy(194,3): anon62_LoopHead

     (0,0): anon62_LoopBody

-    ControlStructures.dfy(197,3): anon63_Else

+    ControlStructures.dfy(194,3): anon63_Else

     (0,0): anon3

-    ControlStructures.dfy(197,3): anon64_Else

+    ControlStructures.dfy(194,3): anon64_Else

     (0,0): anon5

-    ControlStructures.dfy(201,5): anon65_LoopHead

+    ControlStructures.dfy(198,5): anon65_LoopHead

     (0,0): anon65_LoopBody

-    ControlStructures.dfy(201,5): anon66_Else

+    ControlStructures.dfy(198,5): anon66_Else

     (0,0): anon8

-    ControlStructures.dfy(201,5): anon67_Else

+    ControlStructures.dfy(198,5): anon67_Else

     (0,0): anon10

     (0,0): anon71_Then

-    ControlStructures.dfy(213,9): anon72_LoopHead

+    ControlStructures.dfy(210,9): anon72_LoopHead

     (0,0): anon72_LoopBody

-    ControlStructures.dfy(213,9): anon73_Else

+    ControlStructures.dfy(210,9): anon73_Else

     (0,0): anon20

-    ControlStructures.dfy(213,9): anon74_Else

+    ControlStructures.dfy(210,9): anon74_Else

     (0,0): anon22

     (0,0): anon75_Then

     (0,0): after_4

-    ControlStructures.dfy(224,7): anon77_LoopHead

+    ControlStructures.dfy(221,7): anon77_LoopHead

     (0,0): anon77_LoopBody

-    ControlStructures.dfy(224,7): anon78_Else

+    ControlStructures.dfy(221,7): anon78_Else

     (0,0): anon33

-    ControlStructures.dfy(224,7): anon79_Else

+    ControlStructures.dfy(221,7): anon79_Else

     (0,0): anon35

     (0,0): anon82_Then

     (0,0): anon85_Then

diff --git a/Test/dafny0/Basics.dfy b/Test/dafny0/Basics.dfy
index 16fd7d87..b9ba5102 100644
--- a/Test/dafny0/Basics.dfy
+++ b/Test/dafny0/Basics.dfy
@@ -65,3 +65,56 @@ method ChallengeTruth(j: int, k: int)
   // but this is not equally true:

   assert j <= j + k != k + j + 1 < k+k+j <=/*this is the error*/ j+j+k < k+k+j+j == 2*k + 2*j == 2*(k+j);

 }

+

+// --------- multi assignments --------------------------------

+

+class Multi {

+  var x: int;

+  var y: int;

+}

+

+method TestMulti(m: Multi, p: Multi)

+  requires m != null && p != null;

+  modifies m, p;

+{

+  m.x := 10;

+  m.y := 12;

+  p.x := 20;

+  p.y := 22;

+  if (*) {

+    assert p.x == 20;

+    assert m.x == 10;  // error: m and p may be the same

+  }

+  var t, u;

+  u, m.x, t := 100, u + t + m.x, 200;

+  m.x := 0;

+  u, m.x, t := 200, u + t + m.x, 400;

+  assert m.x == 300;

+  if (p.x != 300) {

+    p.x, m.x := m.x, p.x;

+  }

+  assert p.x == 300;

+  if (*) {

+    p.x, m.y := 10, 10;

+    p.x, m.x := 8, 8;  // error: duplicate assignment (since m and p may be the same)

+  }

+

+  var a, b := new int[20], new int[30];

+  a[4], b[10], a[0], a[3], b[18] := 0, 1, 2, 3, 4;

+  a[4], b[b[18]] := 271, 272;

+  a[4], a[b[18]] := 273, 274;  // error: duplicate assignment (since b[18] is 4)

+}

+

+class MyBoxyClass<T> {

+  var f: T;

+}

+

+method TestBoxAssignment<T>(x: MyBoxyClass<int>, y: MyBoxyClass<T>, t: T)

+  requires x != null && y != null;

+  modifies x, y;

+{

+  y.f := t;

+  x.f := 15;

+  // all together now:

+  y.f, x.f := t, 15;  // error: duplicate assignment (if T==int and x==y)

+}

diff --git a/Test/dafny0/ControlStructures.dfy b/Test/dafny0/ControlStructures.dfy
index 5012e003..c46eee3a 100644
--- a/Test/dafny0/ControlStructures.dfy
+++ b/Test/dafny0/ControlStructures.dfy
@@ -96,8 +96,7 @@ method DutchFlag(A: array<int>, N: int, l: int, r: int) returns (result: int)
   var pv := A[l];

   var i := l;

   var j := r-1;

-  // swap A[l] and A[j]

-  var tmp := A[l]; A[l] := A[j]; A[j] := tmp;

+  A[l], A[j] := A[j], A[l];

 

   while (i < j)

     invariant l <= i && i <= j && j < r;

@@ -110,11 +109,9 @@ method DutchFlag(A: array<int>, N: int, l: int, r: int) returns (result: int)
       case pv <= A[j-1] =>

         j := j - 1;

       case A[j-1] < pv && pv < A[i] =>

-        // swap A[j-1] and A[i]

-        tmp := A[i]; A[i] := A[j-1]; A[j-1] := tmp;

+        A[j-1], A[i] := A[i], A[j-1];

         assert A[i] < pv && pv < A[j-1];

-        i := i + 1;

-        j := j - 1;

+        i, j := i + 1, j - 1;

     }

   }

   result := i;

diff --git a/Test/dafny1/MatrixFun.dfy b/Test/dafny1/MatrixFun.dfy
index 81b3f4c9..5c69ac50 100644
--- a/Test/dafny1/MatrixFun.dfy
+++ b/Test/dafny1/MatrixFun.dfy
@@ -24,9 +24,7 @@ method MirrorImage<T>(m: array2<T>)
       invariant (forall i,j :: a+1 <= i && i < m.Length0 && 0 <= j && j < m.Length1 ==>

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

     {

-      var tmp := m[a, m.Length1-1-b];

-      m[a, m.Length1-1-b] := m[a, b];

-      m[a, b] := tmp;

+      m[a, m.Length1-1-b], m[a, b] := m[a, b], m[a, m.Length1-1-b];

       b := b + 1;

     }

     a := a + 1;

@@ -50,7 +48,7 @@ method Flip<T>(m: array2<T>)
     decreases N-a, N-b;

   {

     if (b < N) {

-      var tmp := m[a,b];  m[a,b] := m[b,a];  m[b,a] := tmp;

+      m[a,b], m[b,a] := m[b,a], m[a,b];

       b := b + 1;

     } else {

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

diff --git a/Test/dafny1/PriorityQueue.dfy b/Test/dafny1/PriorityQueue.dfy
index 6e19ab8f..49f6b909 100644
--- a/Test/dafny1/PriorityQueue.dfy
+++ b/Test/dafny1/PriorityQueue.dfy
@@ -62,7 +62,7 @@ class PriorityQueue {
       if (a[i/2] <= a[i]) {

         return;

       }

-      var tmp := a[i];  a[i] := a[i/2];  a[i/2] := tmp;

+      a[i/2], a[i] := a[i], a[i/2];

       i := i / 2;

     }

   }

@@ -104,7 +104,7 @@ class PriorityQueue {
       if (a[i] <= a[smallestChild]) {

         return;

       }

-      var tmp := a[i];  a[i] := a[smallestChild];  a[smallestChild] := tmp;

+      a[smallestChild], a[i] := a[i], a[smallestChild];

       i := smallestChild;

       assert 1 <= i/2/2 ==> a[i/2/2] <= a[i];

     }

@@ -175,7 +175,7 @@ class PriorityQueue_Alternative {
       if (a[i/2] <= a[i]) {

         return;

       }

-      var tmp := a[i];  a[i] := a[i/2];  a[i/2] := tmp;

+      a[i/2], a[i] := a[i], a[i/2];

       i := i / 2;

     }

   }

@@ -213,7 +213,7 @@ class PriorityQueue_Alternative {
       if (a[i] <= a[smallestChild]) {

         return;

       }

-      var tmp := a[i];  a[i] := a[smallestChild];  a[smallestChild] := tmp;

+      a[smallestChild], a[i] := a[i], a[smallestChild];

       i := smallestChild;

       assert 1 <= i/2/2 ==> a[i/2/2] <= a[i];

     }