From 8a332057c2c9fc76e5fb112d430404d1aa47ea0d Mon Sep 17 00:00:00 2001
From: leino <unknown>
Date: Tue, 31 Mar 2015 17:57:52 -0700
Subject: Reflect cleaner syntax in some test programs

---
 Test/dafny3/Dijkstra.dfy | 41 ++++++++++++++++++++++-------------------
 1 file changed, 22 insertions(+), 19 deletions(-)

(limited to 'Test/dafny3')

diff --git a/Test/dafny3/Dijkstra.dfy b/Test/dafny3/Dijkstra.dfy
index acc29ccd..1fbd9b7c 100644
--- a/Test/dafny3/Dijkstra.dfy
+++ b/Test/dafny3/Dijkstra.dfy
@@ -17,11 +17,13 @@ predicate P()
 // The following theorem says that if f satisfies the peculiar property,
 // then f is the identity function.  The body of the method, and the methods
 // that follow, give the proof.
-ghost method theorem()
-  requires P();
-  ensures forall n: nat :: f(n) == n;
+lemma theorem()
+  requires P()
+  ensures forall n: nat :: f(n) == n
 {
-  forall (n: nat) {
+  forall n: nat
+    ensures f(n) == n
+  {
     calc {
       f(n);
     ==  { lemma_ping(n, n); lemma_pong(n); }
@@ -31,12 +33,13 @@ ghost method theorem()
 }
 
 // Aiming at n <= f(n), but strengthening it for induction
-ghost method lemma_ping(j: nat, n: nat)
-  requires P();
-  ensures j <= n ==> j <= f(n);
+lemma lemma_ping(j: nat, n: nat)
+  requires P()
+  ensures j <= n ==> j <= f(n)
 {
   // The case for j == 0 is trivial
-  if 0 < j {
+  if 0 < j 
+  {
     calc {
       j <= f(n);
     ==
@@ -54,9 +57,9 @@ ghost method lemma_ping(j: nat, n: nat)
 }
 
 // The other directorion: f(n) <= n
-ghost method lemma_pong(n: nat)
-  requires P();
-  ensures f(n) <= n;
+lemma lemma_pong(n: nat)
+  requires P()
+  ensures f(n) <= n
 {
   calc {
     f(n) <= n;
@@ -69,13 +72,13 @@ ghost method lemma_pong(n: nat)
   }
 }
 
-ghost method lemma_monotonicity_0(a: nat, b: nat)
-  requires P();
-  ensures a <= b ==> f(a) <= f(b);  // or, equivalently:  f(b) < f(a) ==> b < a
-  decreases b - a;
+lemma lemma_monotonicity_0(a: nat, b: nat)
+  requires P()
+  ensures a <= b ==> f(a) <= f(b)  // or, equivalently:  f(b) < f(a) ==> b < a
+  decreases b - a
 {
   // The case for a == b is trivial
-  if (a < b) {
+  if a < b {
     calc {
       f(a);
     <=  { lemma_monotonicity_1(a); }
@@ -86,9 +89,9 @@ ghost method lemma_monotonicity_0(a: nat, b: nat)
   }
 }
 
-ghost method lemma_monotonicity_1(n: nat)
-  requires P();
-  ensures f(n) <= f(n + 1);
+lemma lemma_monotonicity_1(n: nat)
+  requires P()
+  ensures f(n) <= f(n + 1)
 {
   calc {
     f(n);
-- 
cgit v1.2.3