P009 · NIT Destroys the Universe / NIT 摧毁宇宙

English

For a collection of nonnegative integers, its mex is the smallest nonnegative integer missing from the collection. An operation chooses a nonempty contiguous segment of an array, computes that segment's mex, and replaces every element in the segment with that value.

Given a of length n, prove that nit_destroys_universe(a, n) returns the minimum number of these operations needed to make every element zero. The function computes this number and preserves the input array.

• 1 <= n <= 100000; a contains exactly n integers.
• For every 0 <= i < n, 0 <= a[i] <= 1000000000.
• This function handles one test case. No main, input parser, or output routine is needed.

A nonzero run is a maximal contiguous segment containing only nonzero values. If there are no runs, the answer is 0. One run can be replaced with zeros in one operation because its mex is zero. If at least two runs exist, any segment covering every nonzero element also contains a zero, so one operation cannot suffice. In this case, two operations on the entire array suffice: the first removes all zeros, and the second replaces all elements with zero. Thus the answer is the run count capped at 2.

The supplied implementation scans the array once, counting a new run whenever it enters a nonzero region. It takes O(n) time and O(1) extra runtime space. The scan uses a while loop with an explicit index, a cached array read, and zero/nonzero branches.

The fixed header supplies these mathematical definitions:

• RunCount(xs, before) counts run starts in xs, where before is 1 if the preceding element is nonzero and 0 otherwise. At the beginning of an array, before is 0. The empty list contributes zero; each head contributes one exactly when it is nonzero and before is zero.
• NonzeroRunCount(input, runs) requires runs == RunCount(input, 0). This recursive definition counts each nonzero-run start exactly once.
• Spec(input, out) requires an exact run count with out = 0 for zero runs, out = 1 for one run, and out = 2 for at least two runs.

The ghost list input records the original array. The same store_int_array a n input assertion occurs in both contracts, requiring all elements and their ownership to be preserved. This per-test-case interface requires no storage beyond the n input elements. Mathematical counts use unbounded integers; executable variables use signed C int.

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.

中文

非负整数集合的 mex 是其中未出现的最小非负整数。一次操作选择数组中一个非空连续区间，计算该区间的 mex，并将区间内的所有元素替换为这个值。

给定长度为 n 的数组 a，请证明 nit_destroys_universe(a, n) 返回将所有元素变为零所需的最少操作次数。函数只计算次数，保持输入数组不变。

• 1 <= n <= 100000，数组长度恰好为 n。
• 对所有 0 <= i < n，有 0 <= a[i] <= 1000000000。
• 函数每次处理一个测试用例，无须编写 main、输入解析或输出代码。

一个非零段是只含非零元素的极大连续区间。没有非零段时答案为 0；只有一个非零段时，其 mex 为零，一次操作即可。若至少有两个非零段，覆盖所有非零元素的区间必然含零，其 mex 不为零，因此一次操作不够。此时对整个数组操作两次一定可行：第一次使所有元素非零，第二次使所有元素为零。因此答案等于非零段数量与 2 的较小值。

给定实现只扫描一次数组，每次进入一个非零段时计数加一，时间复杂度为 O(n)，额外运行时空间为 O(1)。扫描使用显式下标的 while 循环，缓存当前元素，并使用零值与非零值分支。

给定头文件定义了以下数学概念：

• RunCount(xs, before) 计算列表 xs 中的非零段起点数。若前一个元素非零，before 为 1，否则为 0；数组开头取 0。空列表贡献零；当前元素非零且 before 为零时，当前元素贡献一个起点。
• NonzeroRunCount(input, runs) 要求 runs == RunCount(input, 0)。该递归定义对每个非零段起点恰好计数一次。
• Spec(input, out) 要求存在精确的非零段数量：零段时返回 0，一段时返回 1，至少两段时返回 2。

幽灵列表 input 记录原始数组，前后置条件中的 store_int_array a n input 要求保持所有元素及其所有权。这个单用例接口只需提供 n 个元素的存储空间。数学计数使用无界整数，运行时变量使用有符号 C int。

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

Examples / 示例