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

4 files changed, 131 insertions, 5 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index d9d3a572..289a597d 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -402,11 +402,25 @@ Execution trace:
 Dafny program verifier finished with 3 verified, 3 errors

 

 -------------------- ResolutionErrors.dfy --------------------

+ResolutionErrors.dfy(39,13): Error: 'this' is not allowed in a 'class' context

 ResolutionErrors.dfy(10,16): Error: 'decreases *' is not allowed on ghost loops

 ResolutionErrors.dfy(22,11): Error: array selection requires an array2 (got array3<T>)

 ResolutionErrors.dfy(23,12): Error: sequence/array selection requires a sequence or array (got array3<T>)

 ResolutionErrors.dfy(24,11): Error: array selection requires an array4 (got array<T>)

-4 resolution/type errors detected in ResolutionErrors.dfy

+ResolutionErrors.dfy(45,14): Error: a field must be selected via an object, not just a class name

+ResolutionErrors.dfy(46,7): Error: unresolved identifier: F

+ResolutionErrors.dfy(47,14): Error: an instance function must be selected via an object, not just a class name

+ResolutionErrors.dfy(48,7): Error: unresolved identifier: G

+ResolutionErrors.dfy(50,2): Error: member M does not exist in class _default

+ResolutionErrors.dfy(52,2): Error: member N does not exist in class _default

+ResolutionErrors.dfy(55,8): Error: non-function expression is called with parameters

+ResolutionErrors.dfy(56,14): Error: member z does not exist in class Global

+ResolutionErrors.dfy(75,12): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny')

+ResolutionErrors.dfy(80,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')

+ResolutionErrors.dfy(81,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')

+ResolutionErrors.dfy(83,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')

+ResolutionErrors.dfy(85,12): Error: wrong number of arguments to datatype constructor Abc (found 2, expected 1)

+18 resolution/type errors detected in ResolutionErrors.dfy

 

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

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

@@ -540,6 +554,10 @@ Execution trace:
 

 Dafny program verifier finished with 6 verified, 1 error

 

+-------------------- Basics.dfy --------------------

+

+Dafny program verifier finished with 5 verified, 0 errors

+

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

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

 Execution trace:

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

+  }

+}

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 5ec0cc4c..b33d4d54 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -8,18 +8,82 @@ method GhostDivergentLoop()
    ghost var i := 0;

    while (i < 2)

       decreases *; // error: not allowed on a ghost loop

-	  invariant i <= 2;

-	  invariant (forall j :: 0 <= j && j < i ==> a[j] > 0);

+      invariant i <= 2;

+      invariant (forall j :: 0 <= j && j < i ==> a[j] > 0);

    {

      i := 0;

    }

    assert a[1] != a[1]; // ...for then this would incorrectly verify

 }

 

-method M<T>(a: array3<T>, b: array<T>, m: int, n: int)

+method ManyIndices<T>(a: array3<T>, b: array<T>, m: int, n: int)

 {

   // the following invalid expressions were once incorrectly resolved:

   var x := a[m, n];        // error

   var y := a[m];           // error

   var z := b[m, n, m, n];  // error

 }

+

+// -------- name resolution

+

+class Global {

+  var X: int;

+  function method F(x: int): int { x }

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

+  method M(x: int) returns (r: int)

+  {

+    r := x + X;

+  }

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

+  {

+    r := x + X;  // error: cannot access instance field X from static method

+  }

+}

+

+method TestNameResolution0() {

+  var z: int;

+  z := Global.X;  // error: X is an instance field

+  z := F(2);  // error: cannot resolve F

+  z := Global.F(2);  // error: invocation of instance function requires an instance

+  z := G(2);  // error: cannot resolve G

+  z := Global.G(2);

+  call z := M(2);  // error: cannot resolve M

+//  call z := Global.M(2);  // error: call to instance method requires an instance

+  call z := N(1);  // error: cannot resolve N

+//  call z := Global.N(1);

+

+  z := z(5);  // error: using local as if it were a function

+  z := Global.z;  // error: class Global does not have a member z

+

+  var Global: Global;  // a local variable with the name 'Global'

+  z := Global.X;  // this means the instance field X of the object stored in the local variable 'Global'

+  var gg: Global := null;

+  var y := gg.G(5);

+  call y := gg.N(5);

+}

+

+datatype Abc = Abel | Benny | Cecilia(y: int) | David(x: int) | Eleanor;

+datatype Xyz = Alberta | Benny | Constantine(y: int) | David(x: int);

+datatype Rst = David(x: int, y: int);

+

+function Tuv(arg0: Abc, arg1: bool): int { 10 }

+var Eleanor: bool;

+

+method TestNameResolution1() {

+  var a0 := Abel;

+  var a1 := Alberta;

+  var b0 := Benny;  // error: there's more than one constructor with the name Benny; needs qualification

+  var b1 := Abc.Benny;

+  var b2 := Xyz.Benny;

+  var Benny := 15;  // introduce a local variable with the name 'Benny'

+  var b3 := Benny;

+  var d0 := David(20);  // error: constructor name David is ambiguous

+  var d1 := David;  // error: constructor name David is ambiguous (never mind that the signature does

+                    // not match either of them)

+  var d2 := David(20, 40);  // error: constructor name Davis is ambiguous (never mind that the given

+                            // parameters match the signature of only one of those constructors)

+  var d3 := Abc.David(20, 40);  // error: wrong number of parameters

+  var d4 := Rst.David(20, 40);

+  var e := Eleanor;

+  assert Tuv(e, this.Eleanor) == 10;

+}

diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index 16bc0e2b..22221a15 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -15,7 +15,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy
             FunctionSpecifications.dfy ResolutionErrors.dfy

             Array.dfy MultiDimArray.dfy NonGhostQuantifiers.dfy AdvancedLHS.dfy

             Modules0.dfy Modules1.dfy BadFunction.dfy

-            Comprehensions.dfy ControlStructures.dfy

+            Comprehensions.dfy Basics.dfy ControlStructures.dfy

             Termination.dfy Use.dfy DTypes.dfy

             TypeParameters.dfy Datatypes.dfy TypeAntecedents.dfy SplitExpr.dfy

             Refinement.dfy RefinementErrors.dfy) do (