// a[0] + a[1] + ... a[k-1]
function sumTo(a:array<int>, k:nat):int
reads a;
requires k <= a.Length;
decreases  k
{
  if (k == 0) then 0
  else a[k-1] + sumTo(a, k-1)
}

// compute a[0] + a[1] + ...
method sum(a:array<int>) returns (s:int)
  ensures s == sumTo(a, a.Length)
{
  var i:nat := 0 ;
  s := 0 ;
  while (i < a.Length)
    decreases a.Length - i;
    invariant i <= a.Length;
    invariant s == sumTo(a, i)
  {
    s := s + a[i] ;
    i := i + 1 ;
  }
}