Selection Sort / 选择排序

English

Given an integer array a of length n, prove that the supplied function selection_sort(a, n) sorts it in place in nondecreasing order. The resulting array must be a permutation of the original array.

The input satisfies the following constraints:

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

Negative values and duplicates are allowed. The function returns void; its result is the updated array. Empty and one-element arrays remain unchanged, and neither case reads an element. For n = 0, the pointer may be null.

For each position i with i + 1 < n, the implementation scans the remaining suffix to find its minimum. It starts with min_index = i and updates that index only on finding a strictly smaller value. If the selected index differs from i, it swaps the two elements. The C* version expresses the two for loops as equivalent while loops and caches the compared and selected values in local variables. The algorithm uses constant runtime extra space and takes O(n^2) time in the worst case.

The fixed header supplies the following mathematical model:

• increasing(output) means that for every pair of valid indices p < q, output[p] <= output[q].
• occurrences(x, values) counts occurrences of the integer x.
• Permutation(input, output) means that every integer has the same occurrence count in both lists, including duplicate multiplicities.

The contract records the original array as the ghost list input. It requires an output list of length n that is nondecreasing and a permutation of input, together with ownership of the array containing that output.

Define any auxiliary predicates and prove the lemmas needed for your invariants in starter.c; the header supplies only the contract model and its dependencies.

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.

中文

给定长度为 n 的整数数组 a，请证明给定函数 selection_sort(a, n) 使用选择排序将其原地按非降序排列。排序后的数组必须为原数组的一个排列。

输入满足以下约束：

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

允许负数和重复元素。函数返回类型为 void，排序结果保存在原数组中。空数组和单元素数组保持不变，这两种情况均不会读取数组元素。n = 0 时，数组指针可以为空指针。

对于每个满足 i + 1 < n 的位置 i，给定实现扫描剩余后缀以找到最小值。先令 min_index = i，只有发现严格更小的值时才更新该下标。如果最终选中的下标与 i 不同，就交换这两个位置的元素。C* 实现将两个 for 循环改写为等价的 while 循环，并使用局部变量缓存比较和交换所需的值。算法运行时额外空间为常数，最坏时间复杂度为 O(n^2)。

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

• increasing(output) 表示任意合法下标 p < q 均满足 output[p] <= output[q]，即非降序。
• occurrences(x, values) 统计整数 x 在列表中出现的次数。
• Permutation(input, output) 表示每个整数在两个列表中的出现次数均相同，包括重复元素的个数。

契约使用幽灵列表 input 记录原始数组内容，并要求存在长度为 n 的输出列表，该列表非降序且为 input 的一个排列，同时保留存放输出列表的数组内存所有权。

请在 starter.c 中自行定义不变式所需的辅助谓词并证明所需引理；头文件仅提供规约模型及其依赖定义。

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

Examples / 示例