Dafny: allow class names to be used when referring to static functions (and, soon, methods), and test cases for new name resolution rules

1 files changed, 44 insertions, 0 deletions

diff --git a/Test/dafny0/Basics.dfy b/Test/dafny0/Basics.dfy
new file mode 100644
index 00000000..1eeb2d92
--- /dev/null
+++ b/Test/dafny0/Basics.dfy
@@ -0,0 +1,44 @@
+class Global {

+  static function G(x: int): int { x+x }

+  static method N(x: int) returns (ghost r: int)

+    ensures r == Global.G(x);

+  {

+    if {

+      case true =>  r := G(x+0);

+      case true =>

+        var g: Global;

+        r := g.G(x);

+      case true =>

+        var g: Global := null;

+        r := g.G(x);

+      case true =>

+        r := Global.G(x);

+    }

+  }

+}

+

+method TestCalls(k: nat) {

+  var g: Global, h: Global;

+  assume g != h;

+  ghost var r: int;

+  ghost var s := Global.G(k);

+

+//  call r := Global.N(k);

+//  assert r == s;

+

+  call r := g.N(k);

+  assert r == s;

+  call r := h.N(k);

+  assert r == s;

+

+  g := null;

+  call r := g.N(k);

+  assert r == s;

+

+//  call r := Global.N(r);

+  if (k == 0) {

+    assert r == s;

+  } else {

+//    assert r == s;  // error: G(k) and G(k+k) are different

+  }

+}