Big Integer Comparison / 大整数大小比较

English

Two nonnegative big integers are represented by decimal digit arrays a and b, both of length n. The most significant digit is at index 0. Prove that the supplied function bigint_compare(a, b, n) returns:

• -1 if the value represented by a is smaller;
• 0 if the two values are equal;
• 1 if the value represented by a is larger.

The input satisfies the following constraints:

• 1 <= n <= 100000; both arrays have exactly n elements.
• Every element of both arrays is a decimal digit: 0 <= digit <= 9.

Leading zeros are allowed. Both arrays must remain unchanged. The contract provides separate ownership of the two arrays, so their storage does not overlap.

The supplied implementation scans from left to right. It returns as soon as it finds a differing pair of digits, and returns 0 after an equal scan. It performs at most n iterations and uses constant runtime extra space. No conversion to a machine integer is required.

The fixed header supplies the mathematical model:

digits_value([]) = 0
digits_value(d :: ds) = d * 10^(length(ds)) + digits_value(ds)

This definition uses unbounded mathematical integers. The ghost lists digits_a and digits_b record the original arrays. The recursive predicate decimal_digits means that every list element lies in [0, 9]; it expresses the element constraint above. The postcondition compares the actual digits_value results and preserves both arrays, including on early returns.

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 header and contract annotations. Submit the completed starter.c; no main function or standard input/output handling is needed.

中文

两个非负大整数用等长十进制数字数组 a、b 表示，长度均为 n，最高位在数组下标 0。请证明给定函数 bigint_compare(a, b, n) 满足：

• 若 a 表示的数小于 b 表示的数，返回 -1；
• 若两个数相等，返回 0；
• 若 a 表示的数大于 b 表示的数，返回 1。

输入满足以下约束：

• 1 <= n <= 100000，两个数组的长度均恰好为 n。
• 两个数组的每个元素都是十进制数字，即 0 <= digit <= 9。

允许前导零。函数必须保持两个数组的内容不变。契约分别提供两个数组的内存所有权，因此它们的存储区域互不重叠。

给定实现从左到右扫描，在遇到第一对不相等的数字时立即返回比较结果；如果所有数字均相等，则返回 0。最多执行 n 次循环，运行时额外空间为常数，不需要将大整数转换为机器整数。

给定头文件提供以下数学模型：

digits_value([]) = 0
digits_value(d :: ds) = d * 10^(length(ds)) + digits_value(ds)

该定义使用无界数学整数。幽灵列表 digits_a、digits_b 记录原始数组内容。递归谓词 decimal_digits 表示列表中每个元素都在 [0, 9] 范围内，与上述元素约束等价。后置条件比较两个列表的实际 digits_value，并要求保留两个数组的原始内容，提前返回时也必须满足这一要求。

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

Examples / 示例