// Add enough annotations so this method verifies.
method LoopUp(lo: int, hi: int) returns (s: int)
  requires lo <= hi
  ensures s == SumUp(lo, hi)
/*{
  s := 0;
  var i := lo;
  while i != hi
  {
    s := s + F(i);
    i := i + 1;
  }
}*/

function F(x: int): int

ghost function SumUp(lo: int, hi: int): int
  requires lo <= hi
  decreases hi - lo
{
  if lo == hi then 0 else F(lo) + SumUp(lo + 1, hi)
}

ghost function SumDown(lo: int, hi: int): int
  requires lo <= hi
  decreases hi - lo
{
  if lo == hi then 0 else SumDown(lo, hi - 1) + F(hi - 1)
}