// RUN: %dafny /compile:3 "%s" > "%t" // RUN: %diff "%s.expect" "%t" class Node { ghost var List: seq; ghost var Repr: set>; var data: T; var next: Node; 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) 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) 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(); }