diff options
Diffstat (limited to 'Test/dafny0/ResolutionErrors.dfy')
| -rw-r--r-- | Test/dafny0/ResolutionErrors.dfy | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index 60314836..92b4aa80 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -642,3 +642,14 @@ module UnderspecifiedTypes { var T4 :| T4 <= S;
}
}
+
+// ------------------------- lemmas ------------------------------
+
+// a lemma is allowed to have out-parameters, but not a modifies clause
+lemma MyLemma(x: int) returns (y: int)
+ requires 0 <= x;
+ modifies this;
+ ensures 0 <= y;
+{
+ y := x;
+}
|