diff options
| author |  rustanleino <unknown> | 2011-02-19 04:19:05 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2011-02-19 04:19:05 +0000 |
| commit | 030a31968ee7b949b14c6aeed8e550385bca92d8 (patch) | |
| tree | 8b69e6a2b9c18632d6561eec958e20266fa64d5e /Test/dafny0/TypeParameters.dfy | |
| parent | 320a0392daf9cbb9d4d2b0d0c0ee66c0392f858f (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> {
|