diff options
| author |  leino <unknown> | 2014-11-01 13:59:06 -0700 |
|---|---|---|
| committer | leino <unknown> | 2014-11-01 13:59:06 -0700 |
| commit | e200c1f9a8b5e7873b17abc71e4a8c1f953ed31c (patch) | |
| tree | 084f3b080f42bf90e3ce15c19a91c72737b65a64 /Test/dafny0 | |
| parent | f21cde811e9194934eb30f196ad19c2cfbeb8ff9 (diff) | |
| parent | 02e2b99ab18659ea2626e2be5fa369b7f1795334 (diff) | |
Merge
Diffstat (limited to 'Test/dafny0')
| -rw-r--r-- | Test/dafny0/DirtyLoops.dfy | 17 | ||||
| -rw-r--r-- | Test/dafny0/DirtyLoops.dfy.expect | 2 |
2 files changed, 17 insertions, 2 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;
+}
diff --git a/Test/dafny0/DirtyLoops.dfy.expect b/Test/dafny0/DirtyLoops.dfy.expect index 5c12e1ef..060f3287 100644 --- a/Test/dafny0/DirtyLoops.dfy.expect +++ b/Test/dafny0/DirtyLoops.dfy.expect @@ -1,4 +1,4 @@ -Dafny program verifier finished with 2 verified, 0 errors
+Dafny program verifier finished with 6 verified, 0 errors
Dafny program verifier finished with 0 verified, 0 errors
|