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;
  }
}