Array Sum / 数组求和

English

Given an integer array a of length n, prove that the supplied function array_sum(a, n) returns the sum of all its elements and leaves the array unchanged. The sum of an empty array is 0.

The input satisfies all of the following conditions:

• 0 <= n <= 100000, and the array has exactly n elements.
• For every 0 <= i < n, -100000 <= a[i] <= 100000.
• For every 0 <= k <= n, the sum of the first k elements is between -2147483648 and 2147483647, inclusive.

All sums in the specification are mathematical integers. The prefix-sum bound guarantees that every addition in the supplied left-to-right implementation fits in a signed 32-bit int. A bound on the final sum alone would not be sufficient.

The C* contract uses two ghost parameters, which are not executable arguments: input records the original array, and prefix records its prefix sums. The contract requires

prefix(0) = 0
prefix(j + 1) = prefix(j) + input[j]    for 0 <= j < n

These equations uniquely determine prefix(k) for every 0 <= k <= n. Thus the required result prefix(n) is exactly the sum of the array. store_int_array a n input describes ownership of the array and its contents; the same assertion in the postcondition requires every element to be preserved.

The implementation and contract are fixed. Add loop invariants and proof code only inside starter.c; changing the implementation or specification is rejected by the judge and consumes an attempt. Keep the supplied model registration code. Submit the completed starter.c; no main function or standard input/output handling is needed.

中文

给定长度为 n 的整数数组 a，请证明给定函数 array_sum(a, n) 返回数组中所有元素的和，并保持数组内容不变。空数组的和为 0。

输入满足以下全部条件：

• 0 <= n <= 100000，数组长度恰好为 n。
• 对所有 0 <= i < n，有 -100000 <= a[i] <= 100000。
• 对所有 0 <= k <= n，前 k 个元素的和满足 -2147483648 <= sum(a[0..k)) <= 2147483647。

规约中的求和使用数学整数。前缀和约束保证给定实现从左到右累加时，每次加法的结果均在 32 位有符号 int 的范围内。仅保证最终总和不溢出是不够的。

C* 契约使用两个幽灵参数，它们不是实际运行时的函数参数：input 记录原始数组内容，prefix 记录前缀和。契约要求：

prefix(0) = 0
prefix(j + 1) = prefix(j) + input[j]    对所有 0 <= j < n

这些等式唯一确定了所有 0 <= k <= n 对应的 prefix(k)，因此返回值 prefix(n) 就是数组中所有元素的和。store_int_array a n input 描述数组的内存所有权及内容；后置条件保留同一断言，要求数组中的每个元素保持不变。

实现和契约均为固定内容。你只能在 starter.c 中添加循环不变式和证明代码；修改实现或规约将被判定为失败，并消耗一次提交机会。请保留给定的模型注册代码。提交完成后的 starter.c 即可，不需要编写 main 函数或标准输入输出代码。

Examples / 示例