diff options
Diffstat (limited to 'Test/dafny0/Datatypes.dfy')
| -rw-r--r-- | Test/dafny0/Datatypes.dfy | 249 |
1 files changed, 0 insertions, 249 deletions
diff --git a/Test/dafny0/Datatypes.dfy b/Test/dafny0/Datatypes.dfy deleted file mode 100644 index 70177ef4..00000000 --- a/Test/dafny0/Datatypes.dfy +++ /dev/null @@ -1,249 +0,0 @@ -datatype List<T> = Nil | Cons(T, List<T>);
-
-class Node {
- var data: int;
- var next: Node;
-
- function Repr(list: List<int>): 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<int>) 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<int>): 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<int>) 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<Node>, b: List<Node>, c: List<AnotherNode>)
-{
- 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<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 := 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<NestedMatchExpr>)
- 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);
|