datatype List = Nil | Cons(T, List); class Node { var data: int; var next: Node; function Repr(list: List): bool reads *; decreases list; { match list case Nil => next == null case Cons(d,cdr) => data == d && next != null && next.Repr(cdr) } method Init() modifies this; ensures Repr(Nil); { next := null; } method Add(d: int, L: List) returns (r: Node) requires Repr(L); ensures r != null && r.Repr(Cons(d, L)); { r := new Node; r.data := d; r.next := this; } } class AnotherNode { var data: int; var next: AnotherNode; function Repr(n: AnotherNode, list: List): bool reads *; decreases list; { match list case Nil => n == null case Cons(d,cdr) => n != null && n.data == d && Repr(n.next, cdr) } method Create() returns (n: AnotherNode) ensures Repr(n, Nil); { n := null; } method Add(n: AnotherNode, d: int, L: List) returns (r: AnotherNode) requires Repr(n, L); ensures Repr(r, Cons(d, L)); { r := new AnotherNode; r.data := d; r.next := n; } } method TestAllocatednessAxioms(a: List, b: List, c: List) { var n := new Node; var p := n; match a { case Nil => case Cons(x, tail) => assert x != n; p := x; } match b { case Nil => case Cons(x, tail) => match tail { case Nil => case Cons(y, more) => assert y != n; assert y != p; // error: if p is car(a), then it and y may very well be equal } } match c { case Nil => case Cons(x, tail) => match tail { case Nil => case Cons(y, more) => var o: object := y; assert p != null ==> p != o; // follows from well-typedness } } } class NestedMatchExpr { function Cadr(a: List, 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(a: List, 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 := Cons(3, Cons(6, 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) ensures Cadr(a, this) == CadrAlt(a, this); { match (a) { case Nil => case Cons(x,t) => match (t) { case Nil => case Cons(y,tail) => } } } } // ------------------- 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); } } method MatchingDestructor(d: XList) returns (r: XList) ensures r.Car == 5; // error: specification is not well-formed (since r might not be an XCons) { if (*) { var x0 := d.Car; // error: d might not be an XCons } else if (d.XCons?) { var x1 := d.Car; } r := XCons(5, XNil); } datatype Triple = T(a: int, b: int, c: int); // just one constructor datatype TripleAndMore = T'(a: int, b: int, c: int) | NotATriple; method Rotate0(t: Triple) returns (u: Triple) { u := T(t.c, t.a, t.b); } method Rotate1(t: TripleAndMore) returns (u: TripleAndMore) { if { case t.T'? => u := T'(t.c, t.a, t.b); case true => u := T'(t.c, t.a, t.b); // error: t may be NotATriple } } // ------------- method FwdBug(f: Fwd, initialized: bool) requires !f.FwdCons?; { match (f) { case FwdNil => // Syntactically, there is a missing case here, but the verifier checks that this is still cool. // There was once a bug in Dafny, where this had caused an ill-defined Boogie program. } if (!initialized) { // There was once a Dafny parsing bug with this line } } function FwdBugFunction(f: Fwd): bool requires !f.FwdCons?; { match f case FwdNil => true // Syntactically, there is a missing case here, but the verifier checks that this is still cool. // There was once a bug in Dafny, where this had caused an ill-defined Boogie program. } datatype Fwd = FwdNil | FwdCons(int, Fwd);