Minor clean-up in a couple of test files.

2 files changed, 7 insertions, 10 deletions

diff --git a/Test/dafny1/pow2.dfy b/Test/dafny1/pow2.dfy
index c7e4bc63..bc23fb0b 100644
--- a/Test/dafny1/pow2.dfy
+++ b/Test/dafny1/pow2.dfy
@@ -31,20 +31,20 @@ function pow2_slow(n: int): int
     2*pow2_slow(n-1)

 }

 

-ghost method Lemma(n: int)

+lemma Lemma(n: int)

   requires 0 <= n && IsEven(n);

   ensures pow2_slow(n) == Square(pow2_slow(n/2));

 {

-  if (n != 0) {

+  if n != 0 {

     Lemma(n-2);

   }

 }

 

-ghost method Theorem(n: int)

+lemma Theorem(n: int)

   requires 0 <= n;

   ensures pow2(n) == pow2_slow(n);

 {

-  if (n == 0) {

+  if n == 0 {

   } else if (IsEven(n)) {

     Lemma(n);

     Theorem(n/2);

diff --git a/Test/dafny4/SoftwareFoundations-Basics.dfy b/Test/dafny4/SoftwareFoundations-Basics.dfy
index 25adce4c..0b695aef 100644
--- a/Test/dafny4/SoftwareFoundations-Basics.dfy
+++ b/Test/dafny4/SoftwareFoundations-Basics.dfy
@@ -53,8 +53,8 @@ method test_next_weekday()
   // "function method" in the declaration of next_weekday.)  To try this

   // out on rise4fun.com/dafny:  (0) comment out (or fix!) the assert above

   // so that the program will verify, (1) fill in a body of the uninterpreted

-  // function f on line 412 below (any body will do; for example, uncomment

-  // line 416), and (2) change the name of this method to Main().

+  // function f on line 396 below (any body will do; for example, uncomment

+  // line 400), and (2) change the name of this method to Main().

   print next_weekday(wednesday);

 }

 

@@ -134,10 +134,7 @@ datatype Nat =
     O

   | S(Nat)

 

-// Note, in order to refer to the function pred as Playground1.pred outside the current

-// module, the function must be declared "static".  This will change in a near-future

-// release of Dafny.

-static function pred (n : Nat) : Nat

+function pred (n : Nat) : Nat

 {

   match n

   case O => O