Dafny: updated test suite to new syntax

8 files changed, 30 insertions, 30 deletions

diff --git a/Test/dafny0/Compilation.dfy b/Test/dafny0/Compilation.dfy
index fe6eda47..c9545c93 100644
--- a/Test/dafny0/Compilation.dfy
+++ b/Test/dafny0/Compilation.dfy
@@ -73,9 +73,9 @@ module T refines S {
   }

 }

 module A {

-   module X as S = T;

-   module Y as S = T;

-   module Z = T;

+   import X as S default T;

+   import Y as S default T;

+   import Z = T;

    static method run() {

      var x := new X.C;

      x.m();

@@ -92,7 +92,7 @@ method NotMain() {
 

 

 ghost module S1 {

-  module B as S = T;

+  import B as S default T;

   static method do()

 }

 

@@ -102,7 +102,7 @@ module T1 refines S1 {
   }

 }

 module A1 {

-   module X as S1 = T1;

+   import X as S1 default T1;

    static method run() {

      X.do();

      var x := new X.B.C;

diff --git a/Test/dafny0/Datatypes.dfy b/Test/dafny0/Datatypes.dfy
index c4899f38..70177ef4 100644
--- a/Test/dafny0/Datatypes.dfy
+++ b/Test/dafny0/Datatypes.dfy
@@ -92,24 +92,24 @@ method TestAllocatednessAxioms(a: List<Node>, b: List<Node>, c: List<AnotherNode
 }

 

 class NestedMatchExpr {

-  function Cadr<T>(a: List<T>, default: T): T

+  function Cadr<T>(a: List<T>, Default: T): T

   {

     match a

-    case Nil => default

+    case Nil => Default

     case Cons(x,t) =>

       match t

-      case Nil => default

+      case Nil => Default

       case Cons(y,tail) => y

   }

   // CadrAlt is the same as Cadr, but it writes its two outer cases in the opposite order

-  function CadrAlt<T>(a: List<T>, default: T): T

+  function CadrAlt<T>(a: List<T>, Default: T): T

   {

     match a

     case Cons(x,t) => (

       match t

-      case Nil => default

+      case Nil => Default

       case Cons(y,tail) => y)

-    case Nil => default

+    case Nil => Default

   }

   method TestNesting0()

   {

diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy
index 273c88de..2bc3c4be 100644
--- a/Test/dafny0/Modules0.dfy
+++ b/Test/dafny0/Modules0.dfy
@@ -24,15 +24,15 @@ module N {
 }

 

 module U {

-  module NN = N;

+  import NN = N;

 }

 

 

 module A {  // Note, this has the effect of importing two different T's,

             // but that's okay as long as the module doesn't try to access

             // one of them

-  module MM = M;

-  module NN = N;

+  import MM = M;

+  import NN = N;

   class X {

     var t: MM.T;  // error: use of the ambiguous name T

     function F(x: MM.T):  // error: use of the ambiguous name T

@@ -57,7 +57,7 @@ module X0 {
 }

 

 module X1 {

-  module X0' = X0;

+  import X0' = X0;

   class MyClass1 {

     method Down(x0: X0'.MyClass0) {

       x0.Down();

@@ -213,7 +213,7 @@ module ATr {
 }

 

 module BTr {

-  module A = ATr;

+  import A = ATr;

   class Y {

     method N() returns (x: A.X)

       ensures x != null;

@@ -224,14 +224,14 @@ module BTr {
 }

 

 module CTr {

-  module B = BTr;

+  import B = BTr;

   class Z {

     var b: B.Y;  // fine

     var a: B.X;  // error: imports don't reach name X explicitly

   }

 }

 module CTs {

-  module B = BTr;

+  import B = BTr;

   method P() {

     var y := new B.Y;

     var x := y.N();  // this is allowed and will correctly infer the type of x to

@@ -270,8 +270,8 @@ module NonLocalB {
 }

 

 module Local {

-  module AA = NonLocalA;

-  module BB = NonLocalB;

+  import AA = NonLocalA;

+  import BB = NonLocalB;

   class MyClass {

     method MyMethod()

     {

diff --git a/Test/dafny0/Modules1.dfy b/Test/dafny0/Modules1.dfy
index 6fd8560e..1f47f3b1 100644
--- a/Test/dafny0/Modules1.dfy
+++ b/Test/dafny0/Modules1.dfy
@@ -1,5 +1,5 @@
 module A {

-  module B = Babble;

+  import B = Babble;

   class X {

     function Fx(z: B.Z): int

       requires z != null;

@@ -80,7 +80,7 @@ module A_Visibility {
 }

 

 module B_Visibility {

-  module A = A_Visibility;

+  import A = A_Visibility;

   method Main() {

     var y;

     if (A.C.P(y)) {

@@ -102,7 +102,7 @@ module Q_Imp {
 }

 

 module Q_M {

-  module Q = Q_Imp;

+  import Q = Q_Imp;

   method MyMethod(root: Q.Node, S: set<Q.Node>)

     requires root in S;

   {

diff --git a/Test/dafny0/ModulesCycle.dfy b/Test/dafny0/ModulesCycle.dfy
index 15cad8e8..72b7e6fb 100644
--- a/Test/dafny0/ModulesCycle.dfy
+++ b/Test/dafny0/ModulesCycle.dfy
@@ -1,12 +1,12 @@
 

 module V {

-  module t = T;  // error: T is not visible (and isn't even a module)

+  import t = T;  // error: T is not visible (and isn't even a module)

 }

 

 module A {

-  module B = C;

+  import B = C;

 }

 

 module C {

-  module D = A;

+  import D = A;

 }
\ No newline at end of file
diff --git a/Test/dafny0/Predicates.dfy b/Test/dafny0/Predicates.dfy
index 8857482f..19375ac2 100644
--- a/Test/dafny0/Predicates.dfy
+++ b/Test/dafny0/Predicates.dfy
@@ -79,7 +79,7 @@ module Tight refines Loose {
 }

 

 module UnawareClient {

-  module L = Loose;

+  import L = Loose;

   method Main0() {

     var n := new L.MyNumber.Init();

     assert n.N == 0;  // error: this is not known

@@ -91,7 +91,7 @@ module UnawareClient {
 }

 

 module AwareClient {

-  module T = Tight;

+  import T = Tight;

   method Main1() {

     var n := new T.MyNumber.Init();

     assert n.N == 0;

diff --git a/Test/dafny0/Refinement.dfy b/Test/dafny0/Refinement.dfy
index 2c2fc52b..e5c06a5e 100644
--- a/Test/dafny0/Refinement.dfy
+++ b/Test/dafny0/Refinement.dfy
@@ -156,7 +156,7 @@ module Concrete refines Abstract {
 }
 
 module Client {
-  module C = Concrete;
+  import C = Concrete;
   class TheClient {
     method Main() {
       var n := new C.MyNumber.Init();
diff --git a/Test/dafny2/StoreAndRetrieve.dfy b/Test/dafny2/StoreAndRetrieve.dfy
index dce9795b..da62f91c 100644
--- a/Test/dafny2/StoreAndRetrieve.dfy
+++ b/Test/dafny2/StoreAndRetrieve.dfy
@@ -1,5 +1,5 @@
 ghost module A {

-  module L = Library;

+  import L = Library;

   class {:autocontracts} StoreAndRetrieve<Thing> {

     ghost var Contents: set<Thing>;

     predicate Valid