method TerminationExample0(a: nat) returns ()
{
    var x := a;

    while x > 1  
        decreases x 
    {
        x := x - 1;
    }
}

method TerminationExample1(a: nat, b: nat) returns ()
{
    var x,y := a,b;

    while x > 1 && y > 1  
        decreases y,x    
    {
        if * {
            x := x - 1;
        } else {            
            y := y - 1;
            x := a;
        }
    }
}


method TerminationExample2(a: nat, b: nat, c: nat) returns ()
{
    var x,y,z := a,b,c;

    while x > 1 && y > 1 && z > 1 
        decreases x + y + z
    {
        if * {
            x := x - 2;
            y := y + 1;
        } else if * {            
            y := y - 2;
            z := z + 1;
        } else {
            z := z - 2;
            x := x + 1;
        }
    }
}



method TerminationExample3(a: nat, b: nat) {
  var x, y := a, b;
  while x > 0 && y > 3
    //decreases x + y, x
    decreases 2 * x + y 
  {
    if * { x := x - 1; y := y + 1; }   
    else { y := y - 3; x := x + 1; }   
  }
}




method Nested(m: nat, n: nat) {
  var i, j := 0, 0;
  while i < m
    decreases m - i, n - j 
  {
    if j < n { j := j + 1; }
    else     { i := i + 1; j := 0; }
  }
}



// I corrected the example before so that it requires the 
// measure I had in mind. You can check that x,y no longer works.

method ModCounting(a: nat, b: nat) {
  var x, y := a, b;
  while x > 0
    decreases x, y % 4
  {
    if y % 4 == 0 { x, y := x - 1, y + 1; }
    else          { y := y + 3; }
  }
}





method PhaseRank(a: nat, b: nat)
{
  var phase: nat := 1;
  var work := a;

  while phase == 0 || work > 0
    decreases 1 - phase, work 
  {
    if phase == 0 {
      phase := 1;
      work := a + b;
    } else {
      work := work - 1;
    }
  }
}






method EuclidGCD(a: nat, b: nat) returns (g: nat)
    requires a >= b > 0
{
  var x, y := a, b;

  while x != y
    invariant x >= y > 0
    decreases x,y  
  {
    x,y := if x - y >= y then x - y else y, if x - y >= y then y else x - y;
  }

  g := x;
}