class Global {
  static function G(x: int): int { x+x }
  static method N(ghost x: int) returns (ghost r: int)
    ensures r == Global.G(x);
  {
    if {
      case true =>  r := G(x+0);
      case true =>
        var g: Global;
        r := g.G(x);
      case true =>
        var g: Global := null;
        r := g.G(x);
      case true =>
        r := Global.G(x);
    }
  }
}

method TestCalls(k: nat) {
  var g: Global, h: Global;
  assume g != h;
  ghost var r: int;
  ghost var s := Global.G(k);

  r := Global.N(k);
  assert r == s;

  r := g.N(k);
  assert r == s;
  r := h.N(k);
  assert r == s;

  g := null;
  r := g.N(k);
  assert r == s;

  r := Global.N(r);
  if (k == 0) {
    assert r == s;
  } else {
    assert r == s;  // error: G(k) and G(k+k) are different
  }
}

// ---------- chaining operators ------------------------------------

function UpTruth(j: int, k: int): bool
  requires 10 <= j < 180 < 220 <= k;
{
  0 < 2 <= 2 < j != 200 < k < k + 1
}

function DownTruth(j: int, k: int): bool
  requires k >= 220 > 180 > j >= 10;
{
  k + 1 > k > 200 != j > 2 >= 2 > 0
}

method ChallengeTruth(j: int, k: int)
  requires 80 <= j < 150 && 250 <= k < 1000;
{
  assert UpTruth(j, k);
  assert DownTruth(j, k);
  // but this is not equally true:
  assert j <= j + k != k + j + 1 < k+k+j <=/*this is the error*/ j+j+k < k+k+j+j == 2*k + 2*j == 2*(k+j);
}

// ---------- reverse implication ------------------------------------

method Explies(s: seq<int>, i: nat)
  requires forall x :: x in s ==> x > 0;
{
  var a, b, c: bool;
  assert a <== b <== c <== false;   // OK, because <== is left-associative
  assert s[i] > 0 <== i < |s|;      // OK, because <== is short-circuiting from the right
}

// --------- multi assignments --------------------------------

class Multi {
  var x: int;
  var y: int;
  var next: Multi;
  method Mutate(z: int) returns (m: Multi)
    requires 0 <= z;
    modifies this;
    ensures y == old(y);
  {
    x := x + z;
  }
  method IncX() returns (oldX: int)
    modifies this;
    ensures x == old(x) + 1 && oldX == old(x);
  {
    x, oldX := x + 1, x;
  }
}

method TestMulti(m: Multi, p: Multi)
  requires m != null && p != null;
  modifies m, p;
{
  m.x := 10;
  m.y := 12;
  p.x := 20;
  p.y := 22;
  if (*) {
    assert p.x == 20;
    assert m.x == 10;  // error: m and p may be the same
  }
  var t, u;
  u, m.x, t := 100, u + t + m.x, 200;
  m.x := 0;
  u, m.x, t := 200, u + t + m.x, 400;
  assert m.x == 300;
  if (p.x != 300) {
    p.x, m.x := m.x, p.x;
  }
  assert p.x == 300;
  if (*) {
    p.x, m.y := 10, 10;
    p.x, m.x := 8, 8;
  }

  var a, b := new int[20], new int[30];
  a[4], b[10], a[0], a[3], b[18] := 0, 1, 2, 3, 4;
  a[4], b[b[18]] := 271, 272;
  a[4], a[b[18]] := 273, 274;  // error: duplicate assignment (since b[18] is 4)
}

class MyBoxyClass<T> {
  var f: T;
}

method TestBoxAssignment<T>(x: MyBoxyClass<int>, y: MyBoxyClass<T>, t: T)
  requires x != null && y != null;
  modifies x, y;
{
  y.f := t;
  x.f := 15;
  // all together now:
  y.f, x.f := t, 15;  // error: duplicate assignment (if T==int and x==y)
  var k: int := x.f;
}

method TestCallsWithFancyLhss(m: Multi)
  requires m != null && m.next != null;
  modifies m, m.next;
{
  m.x := 10;
  var p := m.next;
  m.next.next := m.Mutate(m.x);  // fine
  if (*) {
    assert m.next == old(m.next);  // error: the call to Mutate may have changed m.next
  }
  m.next.next := m.Mutate(20);  // error: LHS may not be well defined (m.next may be null)
  m.x, m.next := 12, p;
  m.x, m.y := SwapEm(m.x, m.y);
  assert m.y == 12;
  if (*) {
    m.x, m.x := SwapEm(m.x, m.y);  // error: duplicate among LHSs
  }
  m.x := 30;
  var xx := m.IncX();
  assert xx == 30;
  m.y := m.IncX();
  assert m.y == 31 && m.x == 32;
  m.x := m.IncX();
  assert m.x == 32;
  xx := m.IncX();
  if (*) {
    assert xx == 33;  // error: xx will in fact be 32
  } else {
    assert xx == 32;  // see!
  }
}

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

function method abs(a:int): int
{
   if a <= 0 then -a else a
}
// test of verifier using euclidean division.
method EuclideanTest(a: int, b: int)
   requires b != 0;
{
   var q, r := a / b, a % b;
   assert 0 <= r < abs(b);
   assert a == b * q + r;
   assert (a/b) * b + a % b == a;
}

method havocInMultiassignment()
{
   var i: nat, j: nat;
   i, j := *, 3;
   assert 0 <= i;
}

method m()
{
  var i: int, j: int;
  i, j := 3, 6;
}

method swap(a: array<int>, i: nat, j: nat)
  requires a != null && 0 <= i < a.Length && 0 <= j < a.Length;
  modifies a;
{
  a[i], a[j] := a[j], a[i];
}

class CC {
  var x : int;
  var y : int;
}

method notQuiteSwap(c: CC, d: CC)
  requires c != null && d != null;
  modifies c,d;
{
  c.x, d.x := c.x, c.x;
}

method notQuiteSwap2(c: CC, d: CC)
  requires c != null && d != null;
  modifies c,d;
{
  c.x, d.x := d.x, c.y; // BAD: c and d could be the same.
}

method OKNowIt'sSwapAgain(c: CC, d: CC)
  requires c != null && d != null;
  modifies c,d;
{
  c.x, d.x := d.x, c.x;
}

method notQuiteSwap3(c: CC, d: CC)
  requires c != null && d != null && c != d;
  modifies c,d;
{
  c.x, d.x := 4, c.y;
  c.x, c.y := 3, c.y;
}

// ---------------------------
// regression tests of things that were once errors

method InlineMultisetFormingExpr(s: seq<int>)
  ensures MSFE(s);
predicate MSFE(s: seq<int>)
{
  multiset(s) == multiset(s)
}

copredicate CoPredTypeCheck(n: int)
  requires n != 0;