diff options
| author |  Unknown <t-jasonk@A3479856.redmond.corp.microsoft.com> | 2011-05-13 10:43:58 -0700 |
|---|---|---|
| committer | Unknown <t-jasonk@A3479856.redmond.corp.microsoft.com> | 2011-05-13 10:43:58 -0700 |
| commit | 2178536246cab25a4564a15c05a6d2fcb4ac54ca (patch) | |
| tree | 681725d51412180fe699f62e17cffb42a99f3526 /Test/dafny0 | |
| parent | 01ef4de837c37c98edc7ba10241867873190b008 (diff) | |
Cleaner version of ghost loop termination example.
Diffstat (limited to 'Test/dafny0')
| -rw-r--r-- | Test/dafny0/Answer | 6 | ||||
| -rw-r--r-- | Test/dafny0/ResolutionErrors.dfy | 17 |
2 files changed, 11 insertions, 12 deletions
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)
|