/*@
  axiomatic AccumulateAxiomatic 
  {
    logic int Accumulate{L}(int* a, integer n, int init) reads a[0..n-1]; 

    axiom
      AccumulateEmpty{L}:
        \forall int *a, init, integer n;
          n <= 0 ==> Accumulate(a, n, init) == init;

    axiom
      AccumulateNext{L}:
        \forall int *a, init, integer n;
          0 < n ==> Accumulate(a, n, init) == Accumulate(a, n-1, init) + a[n-1];
  }


  lemma
    Accumulate1{L}:
      \forall int *a, init; Accumulate{L}(a, 1, init) == init + a[0];
*/


int foo()
{
  //@ assert danger: \false;
  return 1;
}