Sum an Array in Reverse / 逆序数组求和

English

Problem

Given an integer array a of length n, the supplied function array_sum_reverse(a, n) uses a for loop to add its elements in the order a[n - 1], a[n - 2], ..., a[0].

Verify that it returns the sum of all elements and leaves the array unchanged. An empty array has sum zero.

Preconditions

• 0 <= n <= 100000.
• The array has exactly n elements.
• -100000 <= a[i] <= 100000 for every valid index i.
• For every 0 <= k <= n, the sum of the suffix a[k..n) lies in [-2147483648, 2147483647].

The last condition bounds every intermediate sum in the reverse traversal. Bounding only the final total would not be sufficient. All sums in the specification use mathematical integers; the executable program uses signed 32-bit int arithmetic.

C* specification

The ghost parameter input records the original array as a list of mathematical integers; it is not an executable argument. The header defines its sum by

list_sum([]) = 0
list_sum(x :: xs) = x + list_sum(xs)

ilength input is the array length, inth j input is element j, and sublist k n input is the half-open suffix input[k..n). The specification uses slices only with nonnegative endpoints. store_int_array a n input describes ownership of all n array elements with these contents. Requiring the same assertion in the postcondition preserves the array unchanged.

Verification task

Complete starter.c by adding loop invariants and any necessary internal annotations or proof code. You may add proof-only auxiliary definitions and lemmas in that file. Prove that every array access is valid, that signed integer operations do not overflow, and that the function satisfies its postcondition. This includes the empty-array case.

Do not change the executable C code, function signature, ghost parameter, or supplied precondition and postcondition. Keep #include "problem.h" and do not edit the supplied header or its mathematical definitions. The judge compares the fixed program and specification after removing proof annotations.

Submit the completed starter.c. No main function or input/output handling is needed. The verification task is memory safety, absence of signed integer overflow, and partial correctness; it does not request a separate formal termination proof.

中文

题目描述

给定长度为 n 的整数数组 a，给定函数 array_sum_reverse(a, n) 使用 for 循环，按照 a[n - 1], a[n - 2], ..., a[0] 的顺序累加数组元素。

请验证该函数返回所有元素的和，并保持数组内容不变。空数组的和为零。

前置条件

• 0 <= n <= 100000。
• 数组长度恰好为 n。
• 对每个有效下标 i，有 -100000 <= a[i] <= 100000。
• 对所有 0 <= k <= n，后缀 a[k..n) 的元素之和均在 [-2147483648, 2147483647] 范围内。

最后一个条件约束了逆序遍历过程中的每个中间和。仅约束最终总和是不够的。规约中的所有求和均使用数学整数；可执行程序使用 32 位有符号 int 运算。

C* 规约

幽灵参数 input 用数学整数列表记录原始数组内容，它不是实际运行时的函数参数。头文件按如下方式定义列表的和：

list_sum([]) = 0
list_sum(x :: xs) = x + list_sum(xs)

ilength input 表示数组长度，inth j input 表示下标为 j 的元素， sublist k n input 表示半开区间后缀 input[k..n)。规约仅使用端点非负的切片。store_int_array a n input 描述全部 n 个数组元素的内存所有权及其内容。后置条件要求保留同一断言，从而保证数组内容不变。

验证任务

请在 starter.c 中添加循环不变式以及必要的内部标注或证明代码。你可以在该文件中添加仅用于证明的辅助定义和引理。请证明每次数组访问均合法、有符号整数运算不会溢出，且函数满足后置条件。证明必须覆盖空数组的情况。

不得修改可执行 C 代码、函数签名、幽灵参数或给定的前置条件与后置条件。请保留 #include "problem.h"，不得修改给定头文件或其中的数学定义。评测机会在移除证明标注后比较固定程序及规约。

提交完成后的 starter.c 即可，不需要编写 main 函数或输入输出代码。本题要求验证内存安全性、无有符号整数溢出以及部分正确性，不要求单独给出形式化的终止性证明。

Examples / 示例