
#include "accumulate.h"

value_type
accumulate(const value_type* a, size_type n, value_type init)
{
  /*@
    loop invariant index:    0 <= i <= n;
    loop invariant partial:  init == Accumulate(a, i, \at(init,Pre));
    loop assigns i, init;
    loop variant n-i;
  */
  for (size_type i = 0; i < n; ++i) {
    //@ assert \true;
    init = init + a[i];
  }

  return init;
}

