Chalice/tests/examples/swap.chalice


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20

class C {
  method m(a, b) returns (x, y)
    ensures x == a && y == b;
  {
    x := a;
    y := b;
  }

  var F;
  var G;
  method n()
    requires acc(F) && acc(this.G);
    ensures acc(F) && acc(G);
    ensures F == old(G) && G == old(F);
  {
    var tmp := F;
    F := G;
    G := tmp;
  }
}