method Swap(x: int, y: int) returns (a: int, b: int)
  ensures a == y && b == x
{
  a, b := x, y;
  var tmp := a;
  a := b;
  b := tmp;
}



method Swap_forward_incorrect(x: int, y: int) returns (a: int, b: int)
  ensures a == y && b == x
{
  a, b := x, y;

  assert a == x && b == y;

  var tmp := a;

  assert a == x && b == y && tmp == a;

  a := b;

  assert a == x && b == y && tmp == a && a == b; // oops, we can't prove that!

  b := tmp;
}



method Swap_backward(x: int, y: int) returns (a: int, b: int)
  ensures a == y && b == x
{
  // (6): what can we simplify that to?
  assert true;

  // (5): same rule works for parallel assignment:
  assert true;

  a, b := x, y;

  // (4):
  assert true;

  var tmp := a;

  // (3):
  assert true;

  a := b;

  // (2) the rule for assignment may be surprising... replace all mentions of
  // the variable being assigned with copies of the expression being assigned:
  assert true;

  b := tmp;

  // (1) easy starting point... copy in the postcondition:
  assert true;
}