Test/dafny1/ListReverse.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

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

class Node {
  var nxt: Node;

  method ReverseInPlace(x: Node, r: set<Node>) returns (reverse: Node)
    requires null !in r;
    requires x == null || x in r;
    requires (forall y :: y in r ==> y.nxt == null || y.nxt in r);  // region closure
    modifies r;
    ensures reverse == null || reverse in r;
    ensures (forall y :: y in r ==> y.nxt == null || y.nxt in r);  // region closure
    decreases *;
  {
    var current := x;
    reverse := null;
    while (current != null)
      invariant current == null || current in r;
      invariant reverse == null || reverse in r;
      invariant (forall y :: y in r ==> y.nxt == null || y.nxt in r);  // region closure
      decreases *;  // omit loop termination check
    {
      var tmp := current.nxt;
      current.nxt := reverse;
      reverse := current;
      current := tmp;
    }
  }
}