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/Answer | |
| parent | 01ef4de837c37c98edc7ba10241867873190b008 (diff) | |
Cleaner version of ghost loop termination example.
Diffstat (limited to 'Test/dafny0/Answer')
| -rw-r--r-- | Test/dafny0/Answer | 6 |
1 files changed, 3 insertions, 3 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 --------------------
|