Introduced keywords "lemma" (like a "ghost method", but not allowed to have a "modifies" clause) and "colemma" (synonymous with "comethod"; perhaps "comethod" will go away at some point)

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;

+}