diff options
author | chmaria <unknown> | 2014-11-01 13:59:31 +0100 |
---|---|---|
committer | chmaria <unknown> | 2014-11-01 13:59:31 +0100 |
commit | 6e5fb70941531435489c1dc533d7caea9120a3d5 (patch) | |
tree | 4b575de9ef5c17bdf61c805233adbdb2360d0f4c /Test/dafny0/DirtyLoops.dfy | |
parent | 9f41b35b514eba87a037cbada83f0c294eafb936 (diff) |
Added initial support for dirty while statements.
Diffstat (limited to 'Test/dafny0/DirtyLoops.dfy')
-rw-r--r-- | Test/dafny0/DirtyLoops.dfy | 17 |
1 files changed, 16 insertions, 1 deletions
diff --git a/Test/dafny0/DirtyLoops.dfy b/Test/dafny0/DirtyLoops.dfy index 6a49e733..5d356f0a 100644 --- a/Test/dafny0/DirtyLoops.dfy +++ b/Test/dafny0/DirtyLoops.dfy @@ -1,6 +1,21 @@ // RUN: %dafny /compile:0 /dprint:"%t.dprint.dfy" "%s" > "%t"; %dafny /noVerify /compile:0 "%t.dprint.dfy" >> "%t"
// RUN: %diff "%s.expect" "%t"
-method M(S: set<int>) {
+method M0(S: set<int>) {
forall s | s in S ensures s < 0;
}
+
+method M1(x: int)
+{
+ var i := x;
+ while (0 < i)
+ invariant i <= x;
+}
+
+method M2(x: int)
+{
+ var i := x;
+ while (0 < i)
+ invariant i <= x;
+ decreases i;
+}
|