diff options
| author |  Rustan Leino <unknown> | 2013-08-02 21:44:37 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2013-08-02 21:44:37 -0700 |
| commit | 8af0f2d97ab5ca1a212c7f4901c43059ccb08e36 (patch) | |
| tree | f412217ac7bb4e348669f9b34d121349c187e294 /Test/dafny0/Simple.dfy | |
| parent | 0487bbe1d95c08a458e496240547127f03a7be3b (diff) | |
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)
Diffstat (limited to 'Test/dafny0/Simple.dfy')
| -rw-r--r-- | Test/dafny0/Simple.dfy | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/Test/dafny0/Simple.dfy b/Test/dafny0/Simple.dfy index ac3a4792..35740520 100644 --- a/Test/dafny0/Simple.dfy +++ b/Test/dafny0/Simple.dfy @@ -50,3 +50,13 @@ class C { var w: WildData;
var list: List<bool>;
}
+
+lemma M(x: int)
+ ensures x < 8;
+{
+ // proof would go here
+}
+colemma M'(x': int)
+ ensures true;
+{
+}
|