{n:nat}
float dotprod (n:int(n), a[n]: float, b[n]: float) {
  var: nat k; float sum;;

  sum = 0.0;
  for (k = 0; k < n; k = k + 1) {
    sum = sum +. a[k] *. b[k];
  }
  return sum;
}

unit main () {
  var: nat size, i; a[]: float;;

  size = 100;
  a = alloc (size, 0.0);

  for (i = 0; i < size; i = i+1) {
    a[i] = float_of_int (size - i);
  }
  print_int (size * (size - 1) * (2 * size - 1) / 6);
  print_newline ();
  print_float (dotprod (size, a, a));
  print_newline ();
}