Test/dafny4/Bug140.dfy


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67

// RUN: %dafny /compile:3 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"

class Node<T> {
  ghost var List: seq<T>;
  ghost var Repr: set<Node<T>>;

  var data: T;
  var next: Node<T>;

  predicate Valid()
    reads this, Repr
  {
    this in Repr && null !in Repr &&
    (next == null ==> List == [data]) &&
    (next != null ==>
        next in Repr && next.Repr <= Repr &&
        this !in next.Repr &&
        List == [data] + next.List &&
        next.Valid())
  }

  constructor (d: T)
    modifies this
    ensures Valid() && fresh(Repr - {this})
    ensures List == [d]
  {
    data, next := d, null;
    List, Repr := [d], {this};
  }

  constructor InitAsPredecessor(d: T, succ: Node<T>)
    requires succ != null && succ.Valid() && this !in succ.Repr;
    modifies this;
    ensures Valid() && fresh(Repr - {this} - succ.Repr);
    ensures List == [d] + succ.List;
  {
    data, next := d, succ;
    List := [d] + succ.List;
    Repr := {this} + succ.Repr;
  }

  method Prepend(d: T) returns (r: Node<T>)
    requires Valid()
    ensures r != null && r.Valid() && fresh(r.Repr - old(Repr))
    ensures r.List == [d] + List
  {
    r := new Node.InitAsPredecessor(d, this);
  }
  
	method Print()
		requires Valid()
		decreases |List|
	{
		print data;
		if (next != null) {
			next.Print();
		}
	}
}

method Main() 
{
	var l2 := new Node(2);
  var l1 := l2.Prepend(1);
	l1.Print();
}