Subarrays with Sum Less Than k / 和小于 k 的子数组

English

Problem

Count the nonempty contiguous subarrays of a positive integer array whose sum is strictly less than k. Subarrays at different positions count separately, even when they have the same elements or sum. The input array must remain unchanged.

int subarray_sum_less_than_k(int *a, int n, int k);

The supplied program uses a sliding window. It returns 0 immediately when k <= 1; otherwise it extends the right end and removes elements from the left until the window sum is below k.

Constraints

• 0 <= n <= 50000; the array contains exactly n elements.
• 0 <= k <= 1000000.
• 1 <= a[i] <= 1000 for every 0 <= i < n.

An empty array has no nonempty subarrays, so its answer is 0. A sum equal to k is excluded. The largest possible answer is 50000 * 50001 / 2 = 1250025000, which fits in a signed 32-bit int.

Mathematical model and verification task

The ghost parameter xs records the original array; it is not an executable argument. prefix_sums(xs) lists the sums of all nonempty prefixes, in order of increasing length:

prefix_sums([]) = []
prefix_sums(x :: tail) = x :: map(s ↦ x + s, prefix_sums(tail))
subarray_sum_count([], k) = 0
subarray_sum_count(x :: tail, k) =
    length(filter(s ↦ s < k, prefix_sums(x :: tail)))
    + subarray_sum_count(tail, k)

These definitions use mathematical integers. Filtering preserves multiplicity, and recursion over the starting positions counts every qualifying nonempty contiguous subarray once. The definitions also apply to arbitrary integer lists and thresholds; the function contract restricts executable inputs to the constraints above.

Prove the return value equals subarray_sum_count(xs, k). The identical store_int_array a n xs assertion in the precondition and postcondition requires ownership of the whole array and preservation of every element. Verification must justify valid memory accesses and the absence of signed integer overflow. Loop verification establishes partial correctness: the postcondition holds whenever the function returns.

Submission

Complete starter.c by adding proof helpers, proof blocks, and loop invariants. The executable program, function signature, ghost parameter, contracts, and mathematical definitions in problem.h are fixed. Do not modify them. Submit the completed starter.c; no main function or input/output handling is needed.

中文

题目

给定一个正整数数组，统计元素和严格小于 k 的非空连续子数组个数。不同位置的子数组分别计数，即使它们的元素或元素和相同。输入数组必须保持不变。

int subarray_sum_less_than_k(int *a, int n, int k);

给定程序采用滑动窗口。当 k <= 1 时直接返回 0；否则扩展窗口右端，并从左端移除元素，直到窗口内的元素和小于 k。

约束

• 0 <= n <= 50000，数组长度恰好为 n。
• 0 <= k <= 1000000。
• 对每个 0 <= i < n，有 1 <= a[i] <= 1000。

空数组没有非空子数组，因此答案为 0。元素和恰好等于 k 的子数组不计入答案。答案最大为 50000 * 50001 / 2 = 1250025000，可用 32 位有符号 int 表示。

数学模型与验证任务

幽灵参数 xs 记录原始数组内容，不是运行时的函数参数。 prefix_sums(xs) 按前缀长度递增的顺序列出所有非空前缀的元素和：

prefix_sums([]) = []
prefix_sums(x :: tail) = x :: map(s ↦ x + s, prefix_sums(tail))
subarray_sum_count([], k) = 0
subarray_sum_count(x :: tail, k) =
    length(filter(s ↦ s < k, prefix_sums(x :: tail)))
    + subarray_sum_count(tail, k)

这些定义使用数学整数。筛选操作保留重复值，按起点递归恰好将每个满足条件的非空连续子数组计数一次。定义本身也适用于任意整数列表和阈值；函数契约将实际输入限制在上述约束范围内。

请证明返回值等于 subarray_sum_count(xs, k)。前置条件与后置条件中相同的 store_int_array a n xs 断言要求拥有整个数组的内存，并保持每个元素不变。验证必须证明内存访问有效，且有符号整数运算不溢出。循环验证建立部分正确性：当函数返回时，后置条件成立。

提交方式

在 starter.c 中添加证明辅助定义、证明块和循环不变式，完成验证。可执行程序、函数签名、幽灵参数、契约以及 problem.h 中的数学定义均为固定内容，不得修改。提交完成后的 starter.c 即可，无须编写 main 函数或输入输出代码。

Examples / 示例

In the first example, the qualifying subarrays are [5], [2], [6], [5, 2], and [2, 6]. The singleton [10] is excluded.

第一个示例中，满足条件的子数组为 [5]、[2]、[6]、[5, 2] 和 [2, 6]。单元素子数组 [10] 不计入答案。