diff options
| author |  rustanleino <unknown> | 2011-02-02 23:23:14 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2011-02-02 23:23:14 +0000 |
| commit | 9f2be05e55c8fcb8e753afb965ff242d79327691 (patch) | |
| tree | e5418c4c1217e763542dfdf36c0f26a059b5393f /Test/dafny0/DTypes.dfy | |
| parent | 9d24f5281d326d92b3cc738bcc6e870ee43f1653 (diff) | |
Dafny: added ensures clauses to functions
Diffstat (limited to 'Test/dafny0/DTypes.dfy')
| -rw-r--r-- | Test/dafny0/DTypes.dfy | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/Test/dafny0/DTypes.dfy b/Test/dafny0/DTypes.dfy index c6f0737c..d925587b 100644 --- a/Test/dafny0/DTypes.dfy +++ b/Test/dafny0/DTypes.dfy @@ -74,3 +74,16 @@ class Node { } class CP<T,U> {
}
+
+datatype Data {
+ Lemon;
+ Kiwi(int);
+}
+
+function G(d: Data): int
+ requires d != #Data.Lemon;
+{
+ match d
+ case Lemon => G(d)
+ case Kiwi(x) => 7
+}
|