Insertion Sort / 插入排序

English

Given an integer array a of length n, prove that the supplied function insertion_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:

• 1 <= 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.

The implementation extends a sorted prefix one element at a time. It saves a[i] as key, shifts strictly larger preceding elements one position to the right, then writes key into the remaining position. In the supplied C* version, the short-circuit test j >= 0 && a[j] > key is expressed by a loop on j >= 0, a cached value previous = a[j], and a break when previous <= key. Thus a[j] is never read when j is negative. The algorithm uses constant runtime extra space and takes O(n^2) time in the worst case.

The fixed header supplies these mathematical definitions:

• 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. This preserves duplicate multiplicities, not just the set of distinct values.

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，请证明给定函数 insertion_sort(a, n) 使用插入排序将其原地按非降序排列。排序后的数组必须为原数组的一个排列。

输入满足以下约束：

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

允许负数和重复元素。函数返回类型为 void，排序结果保存在原数组中。

给定实现逐步扩展有序前缀：先将 a[i] 保存为 key，再把前面严格大于 key 的元素依次右移一位，最后将 key 写入空出的位置。在给定的 C* 实现中，短路条件 j >= 0 && a[j] > key 被展开为条件为 j >= 0 的循环：先缓存 previous = a[j]，当 previous <= key 时退出。因此，j 为负数时不会读取 a[j]。算法运行时额外空间为常数，最坏时间复杂度为 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 / 示例