diff options
author | 2011-03-01 02:53:16 +0000 | |
---|---|---|
committer | 2011-03-01 02:53:16 +0000 | |
commit | 9d3dc37ca301c2f310dc10929d6c6fe317b54757 (patch) | |
tree | 74993055f0f2ca7383bd04497dc16710b8f86fd0 /Test/dafny0/Datatypes.dfy | |
parent | f9cb8c7c79c2c4a6eb921a58b56d7d207bf09b50 (diff) |
Dafny: support for nested match expressions
Diffstat (limited to 'Test/dafny0/Datatypes.dfy')
-rw-r--r-- | Test/dafny0/Datatypes.dfy | 44 |
1 files changed, 44 insertions, 0 deletions
diff --git a/Test/dafny0/Datatypes.dfy b/Test/dafny0/Datatypes.dfy index a7ac03d9..998b20bc 100644 --- a/Test/dafny0/Datatypes.dfy +++ b/Test/dafny0/Datatypes.dfy @@ -93,3 +93,47 @@ method TestAllocatednessAxioms(a: List<Node>, b: List<Node>, c: List<AnotherNode }
}
}
+
+class NestedMatchExpr {
+ function Cadr<T>(a: List<T>, default: T): T
+ {
+ match a
+ case Nil => default
+ case Cons(x,t) =>
+ match t
+ case Nil => default
+ case Cons(y,tail) => y
+ }
+ // CadrAlt is the same as Cadr, but it writes its two outer cases in the opposite order
+ function CadrAlt<T>(a: List<T>, default: T): T
+ {
+ match a
+ case Cons(x,t) => (
+ match t
+ case Nil => default
+ case Cons(y,tail) => y)
+ case Nil => default
+ }
+ method TestNesting0()
+ {
+ var x := 5;
+ var list := #List.Cons(3, #List.Cons(6, #List.Nil));
+ assert Cadr(list, x) == 6;
+ match (list) {
+ case Nil => assert false;
+ case Cons(h,t) => assert Cadr(t, x) == 5;
+ }
+ }
+ method TestNesting1(a: List<NestedMatchExpr>)
+ ensures Cadr(a, this) == CadrAlt(a, this);
+ {
+ match (a) {
+ case Nil =>
+ case Cons(x,t) =>
+ match (t) {
+ case Nil =>
+ case Cons(y,tail) =>
+ }
+ }
+ }
+}
|