Median of Two Sorted Arrays / 两个有序数组的中位数

English

Problem

Given two nondecreasing integer arrays, prove that the supplied function returns twice the median of their combined elements and leaves both arrays unchanged. For an odd total length, the result is twice the middle element; for an even total length, it is the sum of the two middle elements.

int median_two_sorted_arrays(int *a, int m, int *b, int n);

The fixed implementation uses binary partitioning on the shorter array. Its helper median_partition(int *a, int m, int *b, int n) additionally requires m <= n. Verify both functions. The wrapper exchanges the arrays when needed.

Constraints and ownership

• 0 <= m, n <= 100000 and m + n >= 1.
• Each array is sorted in nondecreasing order; duplicates are allowed.
• Each element is in [-1000000, 1000000].
• The arrays occupy disjoint memory resources. Their lengths and contents must be preserved. Either array may be empty, but they cannot both be empty.

The ghost lists xs and ys record the original contents. They are not executable arguments. The separated assertions store_int_array a m xs ** store_int_array b n ys describe ownership of both arrays. The same assertions in the postcondition require both arrays to remain unchanged.

Mathematical specification

Nondecreasing compares every pair of valid indices in a list. MedianTwice xs ys result uses the concatenation s = xs ++ ys and its length L. There must be values lower and upper occurring in s such that

count(x in s where x < lower) <= (L - 1) div 2
(L - 1) div 2 < count(x in s where x <= lower)
count(x in s where x < upper) <= L div 2
L div 2 < count(x in s where x <= upper)
result = lower + upper

Counts include every occurrence, including duplicates. Thus lower and upper are the elements at zero-based ranks (L - 1) div 2 and L div 2 of the sorted combined elements. They coincide when L is odd. Model arithmetic uses mathematical integers; div denotes floor division. This relation is false for two empty lists because neither membership witness exists.

Verification and submission

Complete starter.c by adding proof declarations, proof blocks, and loop invariants. Prove memory safety, absence of signed integer overflow, and the stated postconditions whenever the functions return. The verification task uses partial correctness; it does not request a separate total-correctness judgment.

The executable statements, function signatures, ghost parameters, contracts, and problem.h are fixed. Do not change them or add axioms, admissions, or unproved strategies. Submit the completed starter.c. No main function or input/output handling is needed.

中文

题目

给定两个非递减整数数组，请证明给定函数返回它们合并后所有元素的中位数的两倍，并保持两个数组不变。总长度为奇数时，返回中间元素的两倍；总长度为偶数时，返回中间两个元素之和。

int median_two_sorted_arrays(int *a, int m, int *b, int n);

给定实现通过在较短的数组上二分查找划分位置来求解。辅助函数 median_partition(int *a, int m, int *b, int n) 额外要求 m <= n。两个函数都需要验证；外层函数在需要时交换两个数组的参数。

约束与所有权

• 0 <= m, n <= 100000，且 m + n >= 1。
• 每个数组按非递减顺序排列，允许重复元素。
• 每个元素均在 [-1000000, 1000000] 内。
• 两个数组占有互不重叠的内存资源，必须保持其长度与内容不变。其中一个数组可以为空，但不能同时为空。

幽灵列表 xs 和 ys 记录两个数组的原始内容，不是运行时参数。分离断言 store_int_array a m xs ** store_int_array b n ys 描述两个数组的所有权。后置条件保留相同断言，要求两个数组的内容均保持不变。

数学规约

Nondecreasing 比较列表中任意一对有效下标对应的元素。 MedianTwice xs ys result 使用拼接列表 s = xs ++ ys 及其长度 L。它要求存在均出现在 s 中的值 lower 和 upper，使得：

s 中严格小于 lower 的元素个数 <= (L - 1) div 2
(L - 1) div 2 < s 中小于或等于 lower 的元素个数
s 中严格小于 upper 的元素个数 <= L div 2
L div 2 < s 中小于或等于 upper 的元素个数
result = lower + upper

计数包含每次出现，重复元素按出现次数计算。因此，lower 和 upper 分别是合并排序后下标为 (L - 1) div 2 和 L div 2 的元素，下标从零开始。 L 为奇数时，两者相同。模型中的算术使用数学整数，div 表示向下取整的除法。两个列表均为空时，该关系为假，因为无法找到属于列表的见证值。

验证与提交

请在 starter.c 中添加证明声明、证明块和循环不变式，完成验证。你需要证明内存访问安全、不发生有符号整数溢出，并证明函数返回时满足后置条件。本题采用部分正确性验证，不要求另行给出总正确性判定。

可执行语句、函数签名、幽灵参数、契约以及 problem.h 均为固定内容，不得修改，也不得引入公理、未完成的证明占位或未经证明的策略。提交完成后的 starter.c 即可，无需编写 main 函数或输入输出代码。

Examples / 示例

The return value is twice the median, so it is always an integer, including when the median itself is a half-integer.

返回值是中位数的两倍，因此即使中位数是半整数，返回值也仍是整数。