class C {
 var id: int;
}


method test(x: C?, y: C?) returns (b: bool)
 // requires x !=null && y != null;
{
  if (x != null && y != null) {
    b := x.id == y.id;
    return b;
  }
  return false;

}

/*
method Abs(x: int) returns (y: int)
ensures x < 0 ==> y == -x;
ensures x >= 0 ==> y == x;
{
   if (x < 0)
     { y := -x;}
   else
     { y := x;}
}

method a(x:int) returns (abs:int)
ensures abs >= x;
{
  abs := Abs(x);
}

method Test1(x:int)
{
   var v := Abs(x);
   assert 0 <= v;
}

function abs(x: int): int
{
   if x < 0 then -x else x
}

method Test2()
{
   var v1 := Abs(3);
   assert v1 = 3;

   var v2 := abs(3);
   assert v2 = 3;
}


method MultipleReturns(x: int, y: int)
returns (more: int, less: int)
requires x > 0 && y > 0;
ensures more >= less;
{
   more := x + y;
   less := x - y;
}

method c(x:int) returns (z1:int, z2:int)
{
  if (x > 0)
  { z1, z2 := MultipleReturns(x, x);}
  else
  { z1 := 0; z2 := 0; }
}



method m(n: nat)
{
   var i: int := 0;
   while (i < n)
     invariant 0 <= i < n;
   {
      i := i + 1;
   }
   assert i = n;
}


method m(n: nat)
{
   var i: int := 0;
   while (i < n+2)
      //invariant 0 <= i < n;
   decreases n + 2 - i;
   {
      i := i + 1;
   }
}




method m(n: nat)
{
   var i: int := n;
   while (0 < i)
   decreases i;
   {
      i := i - 1;
   }
}

*/



function fib(n: nat): nat
decreases n;
{
   if n == 0 then 0 else
   if n == 1 then 1 else
      fib(n - 1) + fib(n - 2)
}


//      n = 0, 1, 2, 3, 4, 5, 6,  7,  8, ...
// fib(n) = 0, 1, 1, 2, 3, 5, 8, 13, 21, ...
method ComputeFib(n: nat) returns (f: nat)
{
  if (n ==0)
   { f := 0; }
  else
  {
    var i, f_1, f_2: int;

    i := 1;
    f := 1;    f_1 := 0;    f_2 := 0;

    while (i < n)
    {
      f_2 := f_1;
      f_1 := f;
      f  := f_1 + f_2;

      i := i + 1;
    }
  }
}

/*
method ComputeFib(n: nat) returns (f: nat)
   requires n > 0;
   ensures f == fib(n);
{
  var i, f1, f2: int;

  i := 1;

  f := 1;    f1 := 0;    f2 := 0;

  while (i < n)
  //invariant 0 < i ;
  invariant i <= n;
  invariant f1 == fib(i-1);
  invariant f == fib(i);
  {
  f2 := f1;
  f1 := f;
  f := f1 + f2;

    i := i + 1;
  }
}



method Find(a: array<int>, key: int) returns (index: int)
{
   index := 0;
   while (index < a.Length)
   {
      if (a[index] == key) { return; }
      index := index + 1;
   }
   index := -1;
}




method Find(a: array<int>, key: int) returns (index: int)
   requires a != null;
   ensures 0 <= index ==> (index < a.Length && a[index] == key &&
                           forall k :: 0 <= k < index ==> a[k] != key);

   ensures index < 0 ==> forall k :: 0 <= k < a.Length ==> a[k] != key;
{
   index := 0;
   while (index < a.Length)
   invariant 0 <= index <= a.Length;
   //invariant index < a.Length ==> a[index] != key;
   invariant forall k:int :: 0 <= k < index ==> a[k] != key;
   {
      if (a[index] == key) { return; }
      index := index + 1;
   }
   index := -1;
}


*/