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

1 files changed, 53 insertions, 0 deletions

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)

+}