From 2178536246cab25a4564a15c05a6d2fcb4ac54ca Mon Sep 17 00:00:00 2001
From: Unknown <t-jasonk@A3479856.redmond.corp.microsoft.com>
Date: Fri, 13 May 2011 10:43:58 -0700
Subject: Cleaner version of ghost loop termination example.

---
 Test/dafny0/Answer               |  6 +++---
 Test/dafny0/ResolutionErrors.dfy | 17 ++++++++---------
 2 files changed, 11 insertions(+), 12 deletions(-)

(limited to 'Test')

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 8382a525..0ee81392 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -393,9 +393,9 @@ Dafny program verifier finished with 3 verified, 3 errors
 
 -------------------- ResolutionErrors.dfy --------------------
 ResolutionErrors.dfy(10,16): Error: 'decreases *' is not allowed on ghost loops
-ResolutionErrors.dfy(23,11): Error: array selection requires an array2 (got array3<T>)
-ResolutionErrors.dfy(24,12): Error: sequence/array selection requires a sequence or array (got array3<T>)
-ResolutionErrors.dfy(25,11): Error: array selection requires an array4 (got array<T>)
+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
 
 -------------------- Array.dfy --------------------
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 77a30102..5ec0cc4c 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -1,20 +1,19 @@
-method UmmThisIsntGoingToWork()
+
+//Should not verify, as ghost loops should not be allowed to diverge.
+method GhostDivergentLoop()
 {
    var a := new int [2];
-   var b := new int [1];
    a[0] := 1;
    a[1] := -1;
-
    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;
+      decreases *; // error: not allowed on a ghost loop
+	  invariant i <= 2;
+	  invariant (forall j :: 0 <= j && j < i ==> a[j] > 0);
    {
-      i := 0;
+     i := 0;
    }
-   assert a[1] == -1;  // ...for then this would incorrectly verify
-   b[a[1]] := 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)
-- 
cgit v1.2.3