VeryFastSorting / 极速排序

English

Task

Complete the proof of the supplied function:

void VeryFastSorting(int *a, int n);

It sorts the array in place into nondecreasing order, preserving every element and its multiplicity. Stability is not required. The input satisfies 0 <= n <= 100000; each element may be any signed 32-bit integer, including -2147483648 and 2147483647. Duplicates and the empty array are allowed.

Fixed implementation

The program uses bubble sort for subarrays of length at most 16. For larger subarrays, it uses heap sort when the remaining depth is zero; otherwise it partitions around the last element and recursively sorts both sides. The initial depth is 2 * floor(log2(n)) for n >= 1, and zero for n = 0. Each partition consumes one unit. Heap sort constructs a max heap bottom up and uses hole-based sift-down: save the root value, move larger children upward, and write the saved value into the final hole.

Verification and mathematical model

Prove the contracts of all seven supplied functions. In addition to the final sorting result, these contracts specify the partition boundaries, heap construction, and the ordering and unchanged prefix guaranteed by sift-down. xs is a ghost parameter recording the array before each call. store_int_array describes ownership of the complete array and its contents. The postconditions retain that ownership. Permutation means equality of occurrence counts for every mathematical integer; increasing means nondecreasing order. These definitions cover duplicates and empty arrays.

Heap indices are zero based. heap_parent(child) is (child - 1) / 2, with division toward zero. heap_ordered(xs, n) requires each child with 0 < child < n to be no larger than its parent. nth_zero returns zero for negative or out-of-range indices. A multiset contains a list representative; store_heap owns a concrete array of the specified length that is a permutation of the representative and satisfies heap order. The header gives the exact contracts and definitions. Their arithmetic uses mathematical integers; executable arithmetic must also stay within signed 32-bit bounds.

The verification task establishes memory safety and partial correctness: whenever a function returns, its postcondition holds. It does not ask for a separate total-correctness judgment or a proof of running-time complexity.

Submission

Complete starter.c by adding proof declarations, proof blocks, ghost arguments, and loop invariants. Keep the executable code, function signatures, contracts, and problem.h fixed. Auxiliary proof definitions and checked lemmas belong in starter.c; do not introduce axioms or unproved strategies. Submit the completed starter.c. No main or input/output handling is needed.

中文

任务

请补全给定函数的证明：

void VeryFastSorting(int *a, int n);

该函数原地将数组排为非递减序，并保留每个元素及其出现次数。不要求排序稳定。输入满足 0 <= n <= 100000；元素可以是任意 32 位有符号整数，包括 -2147483648 和 2147483647。允许重复元素和空数组。

固定实现

长度不超过 16 的子数组使用冒泡排序。对于更长的子数组，若剩余深度为零，则使用堆排序；否则，以最后一个元素为基准进行划分，再递归排序两侧。当 n >= 1 时，初始深度为 2 * floor(log2(n))；当 n = 0 时为零。每次划分消耗一个单位的深度。堆排序自底向上构造大顶堆，下沉操作采用空位法：先保存根元素，将较大的孩子依次上移，最后将保存的值写入空位。

验证要求与数学模型

请证明给定的全部七个函数的契约。除最终排序结果外，契约还规定了划分后的边界关系、建堆结果，以及下沉操作所保证的有序关系和不变前缀。幽灵参数 xs 记录每次调用前的数组内容。store_int_array 描述完整数组的内存所有权及内容，后置条件保留其所有权。Permutation 表示每个数学整数的出现次数相同，increasing 表示非递减序。这些定义也适用于重复元素和空数组。

堆下标从零开始。heap_parent(child) 为 (child - 1) / 2，除法向零取整。 heap_ordered(xs, n) 要求每个满足 0 < child < n 的孩子均不大于其父节点。 nth_zero 对负下标或越界下标返回零。多重集保存一个代表列表；store_heap 拥有指定长度的具体数组，要求其为代表列表的一个排列，且满足堆序。精确契约与定义见头文件。规约中的运算使用数学整数；可执行代码中的运算还必须满足 32 位有符号整数的范围约束。

本题验证内存安全性和部分正确性：函数返回时，后置条件成立。不要求另行给出完全正确性判定或运行时间复杂度证明。

提交方式

在 starter.c 中添加证明声明、证明块、幽灵实参和循环不变式，补全证明。可执行代码、函数签名、契约以及 problem.h 均为固定内容。辅助证明定义和经过检查的引理应放在 starter.c 中，不得引入公理或未经证明的策略。提交完成后的 starter.c 即可，无需编写 main 函数或输入输出代码。

Examples / 示例

The output column shows the contents of the same array after the call. 输出列表示调用后原数组中的内容。