Dafny:

* Beginning of module implementation
* Changed "class" modifier (for functions and methods) to "static"

7 files changed, 338 insertions, 294 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 3186ae01..5dadda4b 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -12,23 +12,23 @@ class MyClass<T, U> {
     ensures t == t;

     ensures old(null) != this;

   {

-    x := 12;

-    while (x < 100)

-      invariant x <= 100;

-    {

-      x := x + 17;

-      if (x % 20 == 3) {

-        x := this.x + 1;

-      } else {

-        this.x := x + 0;

+      x := 12;

+      while (x < 100)

+        invariant x <= 100;

+      {

+        x := x + 17;

+        if (x % 20 == 3) {

+          x := this.x + 1;

+        } else {

+          this.x := x + 0;

+        }

+        call t, u, v := M(true, lotsaObjects)

+        var to: MyClass<T,U>;

+        call to, u, v := M(true, lotsaObjects)

+        call to, u, v := to.M(true, lotsaObjects)

+        assert v[x] != null ==> null !in v[2 .. x][1..][5 := v[this.x]][..10];

       }

-      call t, u, v := M(true, lotsaObjects)

-      var to: MyClass<T,U>;

-      call to, u, v := M(true, lotsaObjects)

-      call to, u, v := to.M(true, lotsaObjects)

-      assert v[x] != null ==> null !in v[2 .. x][1..][5 := v[this.x]][..10];

     }

-  }

 

   function F(x: int, y: int, h: WildData, k: WildData): WildData

   {

@@ -122,144 +122,154 @@ Execution trace:
     (0,0): anon0

     (0,0): anon4_Else

     (0,0): anon3

-SmallTests.dfy(162,7): Error: possible division by zero

+

+Dafny program verifier finished with 22 verified, 9 errors

+

+-------------------- Definedness.dfy --------------------

+Definedness.dfy(8,7): Error: possible division by zero

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(169,16): Error: possible division by zero

+Definedness.dfy(15,16): Error: possible division by zero

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(178,16): Error: target object may be null

+Definedness.dfy(24,16): Error: target object may be null

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(179,21): Error: target object may be null

+Definedness.dfy(25,21): Error: target object may be null

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

-SmallTests.dfy(180,17): Error: possible division by zero

+Definedness.dfy(26,17): Error: possible division by zero

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(187,16): Error: target object may be null

+Definedness.dfy(33,16): Error: target object may be null

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(204,18): Error: target object may be null

+Definedness.dfy(50,18): Error: target object may be null

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(209,18): Error: target object may be null

+Definedness.dfy(55,18): Error: target object may be null

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(231,9): Error: LHS expression must be well defined

+Definedness.dfy(77,9): Error: LHS expression must be well defined

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(232,12): Error: LHS expression must be well defined

+Definedness.dfy(78,12): Error: LHS expression must be well defined

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(233,7): Error: RHS expression must be well defined

+Definedness.dfy(79,7): Error: RHS expression must be well defined

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(238,18): Error: assert condition must be well defined

+Definedness.dfy(84,18): Error: assert condition must be well defined

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(239,5): Error: assume condition must be well defined

+Definedness.dfy(85,5): Error: assume condition must be well defined

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(244,16): Error: if guard must be well defined

+Definedness.dfy(90,16): Error: if guard must be well defined

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(251,19): Error: loop guard must be well defined

+Definedness.dfy(97,19): Error: loop guard must be well defined

 Execution trace:

     (0,0): anon0

-    SmallTests.dfy(251,5): anon8_LoopHead

+    Definedness.dfy(97,5): anon8_LoopHead

     (0,0): anon8_LoopBody

-    SmallTests.dfy(251,5): anon9_Else

+    Definedness.dfy(97,5): anon9_Else

     (0,0): anon3

-SmallTests.dfy(260,23): Error: decreases expression must be well defined at top of each loop iteration

+Definedness.dfy(106,23): Error: decreases expression must be well defined at top of each loop iteration

 Execution trace:

     (0,0): anon0

-    SmallTests.dfy(259,5): anon13_LoopHead

+    Definedness.dfy(105,5): anon13_LoopHead

     (0,0): anon13_LoopBody

     (0,0): anon14_Then

-SmallTests.dfy(266,17): Error: decreases expression must be well defined at top of each loop iteration

+Definedness.dfy(112,17): Error: decreases expression must be well defined at top of each loop iteration

 Execution trace:

     (0,0): anon0

-    SmallTests.dfy(259,5): anon13_LoopHead

+    Definedness.dfy(105,5): anon13_LoopHead

     (0,0): anon13_LoopBody

-    SmallTests.dfy(259,5): anon14_Else

+    Definedness.dfy(105,5): anon14_Else

     (0,0): anon3

     (0,0): anon15_Then

     (0,0): anon6

-    SmallTests.dfy(265,5): anon16_LoopHead

+    Definedness.dfy(111,5): anon16_LoopHead

     (0,0): anon16_LoopBody

     (0,0): anon17_Then

-SmallTests.dfy(276,22): Error: loop invariant must be well defined

+Definedness.dfy(122,22): Error: loop invariant must be well defined

 Execution trace:

     (0,0): anon0

-    SmallTests.dfy(275,5): anon7_LoopHead

+    Definedness.dfy(121,5): anon7_LoopHead

     (0,0): anon7_LoopBody

     (0,0): anon8_Then

-SmallTests.dfy(276,22): Error BP5004: This loop invariant might not hold on entry.

+Definedness.dfy(122,22): Error BP5004: This loop invariant might not hold on entry.

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(277,17): Error: decreases expression must be well defined at top of each loop iteration

+Definedness.dfy(123,17): Error: decreases expression must be well defined at top of each loop iteration

 Execution trace:

     (0,0): anon0

-    SmallTests.dfy(275,5): anon7_LoopHead

+    Definedness.dfy(121,5): anon7_LoopHead

     (0,0): anon7_LoopBody

     (0,0): anon8_Then

-SmallTests.dfy(286,24): Error: loop guard must be well defined

+Definedness.dfy(132,24): Error: loop guard must be well defined

 Execution trace:

     (0,0): anon0

-    SmallTests.dfy(286,5): anon7_LoopHead

+    Definedness.dfy(132,5): anon7_LoopHead

     (0,0): anon7_LoopBody

-    SmallTests.dfy(286,5): anon8_Else

+    Definedness.dfy(132,5): anon8_Else

     (0,0): anon3

-SmallTests.dfy(305,24): Error: loop guard must be well defined

+Definedness.dfy(151,24): Error: loop guard must be well defined

 Execution trace:

     (0,0): anon0

-    SmallTests.dfy(299,5): anon13_LoopHead

+    Definedness.dfy(145,5): anon13_LoopHead

     (0,0): anon13_LoopBody

-    SmallTests.dfy(299,5): anon14_Else

+    Definedness.dfy(145,5): anon14_Else

     (0,0): anon3

     (0,0): anon15_Then

     (0,0): anon6

-    SmallTests.dfy(305,5): anon16_LoopHead

+    Definedness.dfy(151,5): anon16_LoopHead

     (0,0): anon16_LoopBody

-    SmallTests.dfy(305,5): anon17_Else

+    Definedness.dfy(151,5): anon17_Else

     (0,0): anon9

-SmallTests.dfy(326,44): Error: loop invariant must be well defined

+Definedness.dfy(172,44): Error: loop invariant must be well defined

 Execution trace:

     (0,0): anon0

-    SmallTests.dfy(316,5): anon16_LoopHead

+    Definedness.dfy(162,5): anon16_LoopHead

     (0,0): anon16_LoopBody

-    SmallTests.dfy(316,5): anon17_Else

+    Definedness.dfy(162,5): anon17_Else

     (0,0): anon3

     (0,0): anon18_Then

     (0,0): anon6

-    SmallTests.dfy(324,5): anon19_LoopHead

+    Definedness.dfy(170,5): anon19_LoopHead

     (0,0): anon19_LoopBody

     (0,0): anon20_Then

-SmallTests.dfy(347,21): Error: collection expression must be well defined

+Definedness.dfy(193,21): Error: collection expression must be well defined

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(349,11): Error: foreach assignment may update an object not in the enclosing method's modifies clause

+Definedness.dfy(195,11): Error: foreach assignment may update an object not in the enclosing method's modifies clause

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(351,33): Error: range expression must be well defined

+Definedness.dfy(197,33): Error: range expression must be well defined

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(357,18): Error: RHS of assignment must be well defined

+Definedness.dfy(203,18): Error: RHS of assignment must be well defined

 Execution trace:

     (0,0): anon0

-SmallTests.dfy(366,23): Error: loop invariant must be well defined

+Definedness.dfy(212,23): Error: loop invariant must be well defined

 Execution trace:

     (0,0): anon0

-    SmallTests.dfy(364,5): anon7_LoopHead

+    Definedness.dfy(210,5): anon7_LoopHead

     (0,0): anon7_LoopBody

     (0,0): anon8_Then

-SmallTests.dfy(366,23): Error BP5004: This loop invariant might not hold on entry.

+Definedness.dfy(212,23): Error BP5004: This loop invariant might not hold on entry.

 Execution trace:

     (0,0): anon0

 

-Dafny program verifier finished with 43 verified, 38 errors

+Dafny program verifier finished with 21 verified, 29 errors

+

+-------------------- Modules0.dfy --------------------

+Modules0.dfy(13,7): Error: module T named among imports does not exist

+Modules0.dfy(24,7): Error: import graph contains a cycle: H -> I -> J -> G

+Modules0.dfy(7,8): Error: Duplicate name of top-level declaration: T

+3 resolution/type errors detected in Modules0.dfy

 

 -------------------- Queue.dfy --------------------

 

diff --git a/Test/dafny0/BinaryTree.dfy b/Test/dafny0/BinaryTree.dfy
index 5f56cf40..276b6c0e 100644
--- a/Test/dafny0/BinaryTree.dfy
+++ b/Test/dafny0/BinaryTree.dfy
@@ -48,7 +48,7 @@ class IntSet {
     footprint := root.footprint + {this};

   }

 

-  class method InsertHelper(x: int, n: Node) returns (m: Node)

+  static method InsertHelper(x: int, n: Node) returns (m: Node)

     requires n == null || n.Valid();

     modifies n.footprint;

     ensures m != null && m.Valid();

diff --git a/Test/dafny0/Definedness.dfy b/Test/dafny0/Definedness.dfy
new file mode 100644
index 00000000..4bf6ae30
--- /dev/null
+++ b/Test/dafny0/Definedness.dfy
@@ -0,0 +1,218 @@
+// ----------------- wellformed specifications ----------------------

+

+class SoWellformed {

+  var xyz: int;

+  var next: SoWellformed;

+

+  function F(x: int): int

+  { 5 / x }  // error: possible division by zero

+

+  function G(x: int): int

+    requires 0 < x;

+  { 5 / x }

+

+  function H(x: int): int

+    decreases 5/x;  // error: possible division by zero

+  { 12 }

+

+  function I(x: int): int

+    requires 0 < x;

+    decreases 5/x;

+  { 12 }

+

+  method M(a: SoWellformed, b: int) returns (c: bool, d: SoWellformed)

+    requires a.xyz == 7;  // error: not always defined

+    ensures c ==> d.xyz == -7;  // error: not always defined

+    decreases 5 / b;  // error: not always defined

+  {

+    c := false;

+  }

+

+  method N(a: SoWellformed, b: int) returns (c: bool, d: SoWellformed)

+    decreases 5 / b;

+    requires a.next != null;  // error: not always defined

+    requires a.next.xyz == 7;  // this is well-defined, given that the previous line is

+    requires b < -2;

+    ensures 0 <= b ==> d.xyz == -7 && !c;

+  {

+    c := true;

+  }

+

+  method O(a: SoWellformed, b: int) returns (c: bool, d: SoWellformed)

+    modifies a.next;  // this may not be well-defined, but that's okay for modifies clauses

+  {

+    c := true;

+  }

+

+  method P(a: SoWellformed, b: int) returns (c: bool, d: SoWellformed);

+    requires next != null;

+    modifies this;

+    ensures next.xyz < 100;  // error: may not be well-defined (if body sets next to null)

+

+  method Q(a: SoWellformed, s: set<SoWellformed>) returns (c: bool, d: SoWellformed);

+    requires next != null;

+    modifies s;

+    ensures next.xyz < 100;  // error: may not be well-defined (if this in s and body sets next to null)

+

+  method R(a: SoWellformed, s: set<SoWellformed>) returns (c: bool, d: SoWellformed);

+    requires next != null && this !in s;

+    modifies s;

+    ensures next.xyz < 100;  // fine

+}

+

+// ---------------------- welldefinedness checks for statements -------------------

+

+class StatementTwoShoes {

+  var x: int;

+

+  function method F(b: int): StatementTwoShoes

+    requires 0 <= b;

+  {

+    this

+  }

+

+  method M(p: StatementTwoShoes, a: int)

+    modifies this, p;

+  {

+    p.x := a;  // error: receiver may be null

+    F(a).x := a;  // error: LHS may not be well defined

+    x := F(a-10).x;  // error: RHS may not be well defined

+  }

+

+  method N(a: int, b: int)

+  {

+    assert 5 / a == 5 / a;  // error: expression may not be well defined

+    assume 20 / b == 5;  // error: expression may not be well defined

+  }

+

+  method O(a: int) returns (b: int)

+  {

+    if (20 / a == 5) {  // error: expression may not be well defined

+      b := a;

+    }

+  }

+

+  method P(a: int)

+  {

+    while (20 / a == 5) {  // error: expression may not be well defined

+      break;

+    }

+  }

+

+  method Q(a: int, b: int)

+  {

+    var i := 1;

+    while (i < a)

+      decreases F(i), F(a), a - i;  // error: component 1 may not be well defined

+    {

+      i := i + 1;

+    }

+    i := 1;

+    while (i < a)

+      decreases F(b), a - i;  // error: component 0 may not be well defined

+    {

+      i := i + 1;

+    }

+  }

+

+  method R(a: int)

+  {

+    var i := 0;

+    while (i < 100)  // The following produces 3 complaints instead of 1, because loop invariants are not subject to subsumption

+      invariant F(a) != null;  // error: expression may not be well defined, and error: loop invariant may not hold

+      decreases F(a), 100 - i;  // error: component 0 not well defined

+    {

+      i := i + 1;

+    }

+  }

+

+  method S(a: int)

+  {

+    var j := 0;

+    while (20 / a == 5 && j < 100)  // error: guard may not be well defined

+      invariant j <= 100;

+      decreases F(101 - j), 100 - j;

+    {

+      j := j + 1;

+    }

+  }

+

+  method T(a: int)

+    requires a != 0 && 20 / a == 5;

+  {

+    var k := a;

+    var j := 0;

+    while (20 / k == 5 && j < 100)  // fine

+      decreases 100 - j;

+    {

+      j := j + 1;

+    }

+    j := 0;

+    while (20 / k == 5 && j < 100)  // error: guard may not be well defined

+      decreases 100 - j;

+    {

+      havoc k;

+      j := j + 1;

+    }

+  }

+

+  method U()

+  {

+    var i := 0;

+    while (i < 100)

+      invariant i <= 100;

+      decreases 100 - i;

+      invariant F(123 - i) == this;

+    {

+      i := i + 1;

+    }

+    i := 0;

+    while (i < 100)

+      decreases 100 - i;

+      invariant F(if i==77 then -3 else i) == this;  // error: expression may not be well defined

+    {

+      i := i + 1;

+      if (i == 77) { i := i + 1; }

+    }

+  }

+

+  use function G(w: int): int { 5 }

+  function method H(x: int): int;

+

+  method V(s: set<StatementTwoShoes>, a: int, b: int)

+    modifies s;

+  {

+    use G(12 / b);  // fine, because there are no welldefinedness checks on use statements

+    foreach (m in s | m.x < 200)  // s may contain null, but the foreach excludes null

+    {

+      assume 0 <= m.x;

+      assert m.x < 1000;

+      use G(5 / m.x);  // fine, because there are no welldefinedness checks on use statements

+      m.x := m.x + 1;

+    }

+    foreach (m in s + {F(a)})  // error: collection expression may not be well defined

+    {

+      m.x := 5;  // error: possible modifies clause violation

+    }

+    foreach (m in s | F(H(m.x)) == this)  // error: range expression may not be well defined

+    {

+      m.x := H(m.x);

+    }

+    foreach (m in s)

+    {

+      m.x := 100 / m.x;  // error: RhS may not be well defined

+    }

+  }

+

+  method W(x: int)

+  {

+    var i := 0;

+    while (i < 100)

+      // The following line produces two complaints, thanks to the w-encoding of the loop's invariant definedness checking

+      invariant 5 / x != 5 / x;  // error: not well-defined, and error: loop invariant does not hold initially

+      decreases 100 - i;

+    {

+      i := i + 1;

+    }

+  }

+}

diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy
new file mode 100644
index 00000000..cf616fba
--- /dev/null
+++ b/Test/dafny0/Modules0.dfy
@@ -0,0 +1,34 @@
+module M {

+  class T { }

+  class U { }

+}

+

+module N {

+  class T { } // error: duplicate class name

+}

+

+module U imports N {  // fine, despite the fact that a class is called U--module names are in their own name space

+}

+

+module V imports T {  // error: T is not a module

+}

+

+module A imports B, M {

+  class Y { }

+}

+

+module B imports N, M {

+  class X { }

+}

+

+module G imports A, M, A, H, B {  // error: cycle in import graph

+}

+

+module H imports A, N, I {

+}

+

+module I imports J {

+}

+

+module J imports G, M {

+}

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index 3bf5ed3f..b627df75 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -151,222 +151,3 @@ class Modifies {
     }

   }

 }

-

-// ----------------- wellformed specifications ----------------------

-

-class SoWellformed {

-  var xyz: int;

-  var next: SoWellformed;

-

-  function F(x: int): int

-  { 5 / x }  // error: possible division by zero

-

-  function G(x: int): int

-    requires 0 < x;

-  { 5 / x }

-

-  function H(x: int): int

-    decreases 5/x;  // error: possible division by zero

-  { 12 }

-

-  function I(x: int): int

-    requires 0 < x;

-    decreases 5/x;

-  { 12 }

-

-  method M(a: SoWellformed, b: int) returns (c: bool, d: SoWellformed)

-    requires a.xyz == 7;  // error: not always defined

-    ensures c ==> d.xyz == -7;  // error: not always defined

-    decreases 5 / b;  // error: not always defined

-  {

-    c := false;

-  }

-

-  method N(a: SoWellformed, b: int) returns (c: bool, d: SoWellformed)

-    decreases 5 / b;

-    requires a.next != null;  // error: not always defined

-    requires a.next.xyz == 7;  // this is well-defined, given that the previous line is

-    requires b < -2;

-    ensures 0 <= b ==> d.xyz == -7 && !c;

-  {

-    c := true;

-  }

-

-  method O(a: SoWellformed, b: int) returns (c: bool, d: SoWellformed)

-    modifies a.next;  // this may not be well-defined, but that's okay for modifies clauses

-  {

-    c := true;

-  }

-

-  method P(a: SoWellformed, b: int) returns (c: bool, d: SoWellformed);

-    requires next != null;

-    modifies this;

-    ensures next.xyz < 100;  // error: may not be well-defined (if body sets next to null)

-

-  method Q(a: SoWellformed, s: set<SoWellformed>) returns (c: bool, d: SoWellformed);

-    requires next != null;

-    modifies s;

-    ensures next.xyz < 100;  // error: may not be well-defined (if this in s and body sets next to null)

-

-  method R(a: SoWellformed, s: set<SoWellformed>) returns (c: bool, d: SoWellformed);

-    requires next != null && this !in s;

-    modifies s;

-    ensures next.xyz < 100;  // fine

-}

-

-// ---------------------- welldefinedness checks for statements -------------------

-

-class StatementTwoShoes {

-  var x: int;

-

-  function method F(b: int): StatementTwoShoes

-    requires 0 <= b;

-  {

-    this

-  }

-

-  method M(p: StatementTwoShoes, a: int)

-    modifies this, p;

-  {

-    p.x := a;  // error: receiver may be null

-    F(a).x := a;  // error: LHS may not be well defined

-    x := F(a-10).x;  // error: RHS may not be well defined

-  }

-

-  method N(a: int, b: int)

-  {

-    assert 5 / a == 5 / a;  // error: expression may not be well defined

-    assume 20 / b == 5;  // error: expression may not be well defined

-  }

-

-  method O(a: int) returns (b: int)

-  {

-    if (20 / a == 5) {  // error: expression may not be well defined

-      b := a;

-    }

-  }

-

-  method P(a: int)

-  {

-    while (20 / a == 5) {  // error: expression may not be well defined

-      break;

-    }

-  }

-

-  method Q(a: int, b: int)

-  {

-    var i := 1;

-    while (i < a)

-      decreases F(i), F(a), a - i;  // error: component 1 may not be well defined

-    {

-      i := i + 1;

-    }

-    i := 1;

-    while (i < a)

-      decreases F(b), a - i;  // error: component 0 may not be well defined

-    {

-      i := i + 1;

-    }

-  }

-

-  method R(a: int)

-  {

-    var i := 0;

-    while (i < 100)  // The following produces 3 complaints instead of 1, because loop invariants are not subject to subsumption

-      invariant F(a) != null;  // error: expression may not be well defined, and error: loop invariant may not hold

-      decreases F(a), 100 - i;  // error: component 0 not well defined

-    {

-      i := i + 1;

-    }

-  }

-

-  method S(a: int)

-  {

-    var j := 0;

-    while (20 / a == 5 && j < 100)  // error: guard may not be well defined

-      invariant j <= 100;

-      decreases F(101 - j), 100 - j;

-    {

-      j := j + 1;

-    }

-  }

-

-  method T(a: int)

-    requires a != 0 && 20 / a == 5;

-  {

-    var k := a;

-    var j := 0;

-    while (20 / k == 5 && j < 100)  // fine

-      decreases 100 - j;

-    {

-      j := j + 1;

-    }

-    j := 0;

-    while (20 / k == 5 && j < 100)  // error: guard may not be well defined

-      decreases 100 - j;

-    {

-      havoc k;

-      j := j + 1;

-    }

-  }

-

-  method U()

-  {

-    var i := 0;

-    while (i < 100)

-      invariant i <= 100;

-      decreases 100 - i;

-      invariant F(123 - i) == this;

-    {

-      i := i + 1;

-    }

-    i := 0;

-    while (i < 100)

-      decreases 100 - i;

-      invariant F(if i==77 then -3 else i) == this;  // error: expression may not be well defined

-    {

-      i := i + 1;

-      if (i == 77) { i := i + 1; }

-    }

-  }

-

-  use function G(w: int): int { 5 }

-  function method H(x: int): int;

-

-  method V(s: set<StatementTwoShoes>, a: int, b: int)

-    modifies s;

-  {

-    use G(12 / b);  // fine, because there are no welldefinedness checks on use statements

-    foreach (m in s | m.x < 200)  // s may contain null, but the foreach excludes null

-    {

-      assume 0 <= m.x;

-      assert m.x < 1000;

-      use G(5 / m.x);  // fine, because there are no welldefinedness checks on use statements

-      m.x := m.x + 1;

-    }

-    foreach (m in s + {F(a)})  // error: collection expression may not be well defined

-    {

-      m.x := 5;  // error: possible modifies clause violation

-    }

-    foreach (m in s | F(H(m.x)) == this)  // error: range expression may not be well defined

-    {

-      m.x := H(m.x);

-    }

-    foreach (m in s)

-    {

-      m.x := 100 / m.x;  // error: RhS may not be well defined

-    }

-  }

-

-  method W(x: int)

-  {

-    var i := 0;

-    while (i < 100)

-      // The following line produces two complaints, thanks to the w-encoding of the loop's invariant definedness checking

-      invariant 5 / x != 5 / x;  // error: not well-defined, and error: loop invariant does not hold initially

-      decreases 100 - i;

-    {

-      i := i + 1;

-    }

-  }

-}

diff --git a/Test/dafny0/SumOfCubes.dfy b/Test/dafny0/SumOfCubes.dfy
index 389c885c..42a82fe6 100644
--- a/Test/dafny0/SumOfCubes.dfy
+++ b/Test/dafny0/SumOfCubes.dfy
@@ -1,12 +1,12 @@
 class SumOfCubes {

-  class use function SumEmUp(n: int, m: int): int

+  static use function SumEmUp(n: int, m: int): int

     requires 0 <= n && n <= m;

     decreases m - n;

   {

     if m == n then 0 else n*n*n + SumEmUp(n+1, m)

   }

 

-  class method Socu(n: int, m: int) returns (r: int)

+  static method Socu(n: int, m: int) returns (r: int)

     requires 0 <= n && n <= m;

     ensures r == SumEmUp(n, m);

   {

@@ -16,7 +16,7 @@ class SumOfCubes {
     call Lemma0(n, m);

   }

 

-  class method SocuFromZero(k: int) returns (r: int)

+  static method SocuFromZero(k: int) returns (r: int)

     requires 0 <= k;

     ensures r == SumEmUp(0, k);

   {

@@ -25,7 +25,7 @@ class SumOfCubes {
     call Lemma1(k);

   }

 

-  ghost class method Lemma0(n: int, m: int)

+  ghost static method Lemma0(n: int, m: int)

     requires 0 <= n && n <= m;

     ensures SumEmUp(n, m) == SumEmUp(0, m) - SumEmUp(0, n);

   {

@@ -42,14 +42,14 @@ class SumOfCubes {
     call Lemma3(0, k);

   }

 

-  class use function GSum(k: int): int

+  static use function GSum(k: int): int

     requires 0 <= k;

     decreases k;

   {

     if k == 0 then 0 else GSum(k-1) + k-1

   }

 

-  ghost class method Gauss(k: int) returns (r: int)

+  ghost static method Gauss(k: int) returns (r: int)

     requires 0 <= k;

     ensures r == GSum(k);

   {

@@ -57,7 +57,7 @@ class SumOfCubes {
     call Lemma2(k);

   }

 

-  ghost class method Lemma1(k: int)

+  ghost static method Lemma1(k: int)

     requires 0 <= k;

     ensures SumEmUp(0, k) == GSum(k) * GSum(k);

   {

@@ -73,7 +73,7 @@ class SumOfCubes {
     call Lemma3(0, k);

   }

 

-  ghost class method Lemma2(k: int)

+  ghost static method Lemma2(k: int)

     requires 0 <= k;

     ensures 2 * GSum(k) == k * (k - 1);

   {

@@ -87,14 +87,14 @@ class SumOfCubes {
     }

   }

 

-  class use function SumEmDown(n: int, m: int): int

+  static use function SumEmDown(n: int, m: int): int

     requires 0 <= n && n <= m;

     decreases m;

   {

     if m == n then 0 else SumEmDown(n, m-1) + (m-1)*(m-1)*(m-1)

   }

 

-  ghost class method Lemma3(n: int, m: int)

+  ghost static method Lemma3(n: int, m: int)

     requires 0 <= n && n <= m;

     ensures SumEmUp(n, m) == SumEmDown(n, m);

   {

diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index c1837b43..2bec0a4d 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -17,7 +17,8 @@ for %%f in (BQueue.bpl) do (
   %BPLEXE% %* %%f

 )

 

-for %%f in (TypeTests.dfy SmallTests.dfy Queue.dfy ListCopy.dfy

+for %%f in (TypeTests.dfy SmallTests.dfy Definedness.dfy

+            Modules0.dfy Queue.dfy ListCopy.dfy

             BinaryTree.dfy ListReverse.dfy ListContents.dfy

             SchorrWaite.dfy Termination.dfy Use.dfy DTypes.dfy

             TypeParameters.dfy Datatypes.dfy UnboundedStack.dfy