diff options
| author |  rustanleino <unknown> | 2011-02-19 04:19:05 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2011-02-19 04:19:05 +0000 |
| commit | d4fa0b13799c9639b106b909e6d4b5cb36841b9e (patch) | |
| tree | 103f74b5216530ba430290dcab9fde1ae9acb6d2 /Test/dafny0/TypeParameters.dfy | |
| parent | b841cb8090c47b0807292c76f591bf38d0bbe9df (diff) | |
Dafny: Improved scheme for splitting expressions. Also, report each split in error messages.
Diffstat (limited to 'Test/dafny0/TypeParameters.dfy')
| -rw-r--r-- | Test/dafny0/TypeParameters.dfy | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/Test/dafny0/TypeParameters.dfy b/Test/dafny0/TypeParameters.dfy index 7aaf5ad3..a044341e 100644 --- a/Test/dafny0/TypeParameters.dfy +++ b/Test/dafny0/TypeParameters.dfy @@ -133,6 +133,22 @@ method IsRogerCool(n: int) }
}
+method LoopyRoger(n: int)
+{
+ var i := 0;
+ while (i < n)
+ invariant RogerThat(0 <= n ==> i <= n);
+ {
+ i := i + 1;
+ }
+ i := 0;
+ while (i < n)
+ invariant RogerThat(0 <= n ==> i <= n); // error: failure to maintain loop invariant
+ {
+ i := i + 2;
+ }
+}
+
// ----------------------
class TyKn_C<T> {
|