Minimize the Largest Segment Sum / 最小化最大分段和

English

Given a nonnegative integer array a of length n and an integer k, partition it into exactly k nonempty contiguous segments. The cost is the largest segment sum. Return the minimum possible cost, preserving element order and leaving the array unchanged.

Preconditions

• 1 <= n <= 100000 and 1 <= k <= n.
• The array has exactly n elements, each between 0 and 10000, inclusive.

Thus the total sum and the optimal answer are at most 1000000000.

Verification task

Complete starter.c. The fixed program searches for the smallest feasible capacity. Its helper fits_in_k greedily packs consecutive elements into segments, tracking the unused capacity in the current segment. The helper also requires 0 <= cap <= 1000000000 and returns either zero or one.

Add loop invariants and necessary internal proof annotations for both fits_in_k and split_min_largest_sum, including the ownership reasoning needed for array reads. Prove both function contracts, memory safety, absence of signed integer overflow, preservation of the array, and optimality of the returned answer.

problem.h supplies the mathematical definitions used by the contracts. PrefixSplitState describes the greedy prefix transitions; CanSplit and CannotSplit describe their completed states. SegmentPartition requires nonempty contiguous segments, MaxSegmentSum gives their attained maximum sum, and MinimizedMaxSegmentSum requires an attained minimum over partitions into exactly k segments.

The feasibility check uses at most k segments. Your proof must connect it to exactly k nonempty segments: because elements are nonnegative and k <= n, further splitting can reach k without increasing the largest sum. Merely showing minimality among successful greedy checks does not establish the required postcondition.

You may add proved helper lemmas, private mathematical definitions, proof-only helpers and internal annotations. Preserve the supplied definitions, both function signatures and contracts, and all executable C code. Do not introduce axioms, admissions or unproved strategies. Submit the completed starter.c; the judge uses the fixed problem.h. No main or input/output code is needed.

C* checks the annotated program's partial correctness and safety. A separate measure-decrease lemma alone does not constitute a total-correctness judgment.

中文

给定长度为 n 的非负整数数组 a 和整数 k，将数组划分为恰好 k 个非空连续段。一次划分的代价为各段元素之和的最大值。请返回所有划分中最小的代价，保持元素顺序，并保持数组内容不变。

前置条件

• 1 <= n <= 100000，且 1 <= k <= n。
• 数组长度恰好为 n，每个元素均在 [0, 10000] 范围内。

因此，数组总和与最优答案均不超过 1000000000。

验证任务

请补全 starter.c。给定程序搜索最小的可行容量。辅助函数 fits_in_k 以贪心方式将连续元素装入各段，并记录当前段的剩余容量。该辅助函数还要求 0 <= cap <= 1000000000，返回值为零或一。

请为 fits_in_k 和 split_min_largest_sum 两个函数添加循环不变式及必要的内部证明标注，包括数组读取所需的所有权推理。你需要证明两个函数的契约、内存安全性、无有符号整数溢出、数组内容不变，以及返回答案的最优性。

problem.h 提供了契约使用的数学定义。PrefixSplitState 描述贪心算法处理数组前缀时的状态转移，CanSplit 和 CannotSplit 描述其完成状态。SegmentPartition 要求各段非空且连续，MaxSegmentSum 给出各段元素之和中实际取得的最大值，MinimizedMaxSegmentSum 则要求返回值是所有恰好分为 k 段的划分中实际取得的最小代价。

可行性检查使用至多 k 段。你的证明必须将这一条件与恰好 k 个非空段联系起来：由于元素非负且 k <= n，可以继续拆分，直到段数达到 k，而不增加最大分段和。仅证明答案在贪心检查成功的容量中最小，并不足以证明要求的后置条件。

你可以添加经过证明的辅助引理、私有数学定义、仅用于证明的辅助函数及内部标注。请保留给定定义、两个函数的签名与契约，以及全部可执行 C 代码。不得引入公理、跳过证明或使用未经证明的策略。提交完成后的 starter.c；评测机使用固定的 problem.h。不需要编写 main 函数或输入输出代码。

C* 检查带标注程序的部分正确性和安全性。单独证明一个度量递减引理，并不构成对程序完全正确性的验证。

Examples / 示例