Does the Array Contain Zero? / 判断数组中是否有零

English

Given an integer array a of length n, prove that the supplied function array_has_zero(a, n) returns 1 if at least one element equals 0, and returns 0 otherwise. The array must remain unchanged.

The input satisfies both of the following constraints:

• 0 <= n <= 100000, and the array has exactly n elements.
• For every 0 <= i < n, -100000 <= a[i] <= 100000.

The implementation scans from left to right and returns 1 immediately on finding a zero. If it reaches the end, it returns 0. In particular, an empty array produces 0 without reading any element.

The C* contract uses the ghost list input to record the original array. An existentially quantified index expresses that a zero exists:

there exists j such that 0 <= j < n and input[j] = 0

The result is restricted to 0 or 1. A result of 1 requires such an index; a result of 0 requires every in-range element to be nonzero. These conditions are equivalent to membership or non-membership of zero in the original list. store_int_array a n input in both the precondition and the postcondition requires the array contents to be preserved, including on an early return.

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_has_zero(a, n) 在数组中存在元素等于 0 时返回 1，否则返回 0，并保持数组内容不变。

输入满足以下约束：

• 0 <= n <= 100000，数组长度恰好为 n。
• 对所有 0 <= i < n，有 -100000 <= a[i] <= 100000。

给定实现从左到右扫描数组，遇到零时立即返回 1；如果扫描到末尾仍未找到零，则返回 0。特别地，空数组返回 0，不会读取任何元素。

C* 契约使用幽灵列表 input 记录原始数组内容，并用存在量词描述“存在零”：

存在下标 j，满足 0 <= j < n 且 input[j] = 0

契约将返回值限制为 0 或 1。返回 1 时必须存在上述下标；返回 0 时必须保证所有合法下标处的元素均非零。这与零属于或不属于原始列表的条件等价。前置条件和后置条件中的 store_int_array a n input 要求保留数组的内存所有权及原始内容，提前返回时也必须满足这一要求。

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

Examples / 示例