diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-06-05 17:15:05 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-06-05 17:15:05 -0700 |
| commit | 629da95c2623b66d2d39c198e714df2b0147e511 (patch) | |
| tree | 523fc711421135d47228d08cdc509eff5636fe00 /Test/dafny0/Datatypes.dfy | |
| parent | b2757720d71257434e70a1dbdc3f0d425e0e283c (diff) | |
Dafny: added implicit datatype query fields and datatype destructor fields
Diffstat (limited to 'Test/dafny0/Datatypes.dfy')
| -rw-r--r-- | Test/dafny0/Datatypes.dfy | 59 |
1 files changed, 59 insertions, 0 deletions
diff --git a/Test/dafny0/Datatypes.dfy b/Test/dafny0/Datatypes.dfy index 99e5e920..31b3860a 100644 --- a/Test/dafny0/Datatypes.dfy +++ b/Test/dafny0/Datatypes.dfy @@ -134,3 +134,62 @@ class NestedMatchExpr { }
}
}
+
+// ------------------- datatype destructors ---------------------------------------
+
+datatype XList = XNil | XCons(Car: int, Cdr: XList);
+
+method Destructors0(d: XList) {
+ Lemma_AllCases(d);
+ if {
+ case d.XNil? =>
+ assert d == XNil;
+ case d.XCons? =>
+ var hd := d.Car;
+ var tl := d.Cdr;
+ assert d == XCons(hd, tl);
+ }
+}
+
+method Destructors1(d: XList) {
+ match (d) {
+ case XNil =>
+ assert d.XNil?;
+ case XCons(hd,tl) =>
+ assert d.XCons?;
+ }
+}
+
+method Destructors2(d: XList) {
+ // this method gets it backwards
+ match (d) {
+ case XNil =>
+ assert d.XCons?; // error
+ case XCons(hd,tl) =>
+ assert d.XNil?; // error
+ }
+}
+
+ghost method Lemma_AllCases(d: XList)
+ ensures d.XNil? || d.XCons?;
+{
+ match (d) {
+ case XNil =>
+ case XCons(hd,tl) =>
+ }
+}
+
+method InjectivityTests(d: XList)
+ requires d != XNil;
+{
+ match (d) {
+ case XCons(a,b) =>
+ match (d) {
+ case XCons(x,y) =>
+ assert a == x && b == y;
+ }
+ assert a == d.Car;
+ assert b == d.Cdr;
+ assert d == XCons(d.Car, d.Cdr);
+ }
+}
|