The First Element Greater Than x: Binary Search / 第一个大于 x 的元素：二分搜索

English

Problem

Given a strictly increasing integer array a of length n and an integer x, find the smallest index i such that a[i] > x using binary search.

Indices are zero-based. Return n if no such index exists. In particular, return zero when the array is empty. The array must remain unchanged.

The supplied function is:

int binary_search_upper_bound(int *a, int n, int x);

Preconditions

• 0 <= n <= 100000.
• The array has exactly n elements.
• Every array element and x is a signed 32-bit integer.
• For every 0 <= i < j < n, a[i] < a[j].

Verification Task

Complete starter.c by adding loop invariants and any necessary internal proof annotations. Prove memory safety, absence of signed integer overflow, and the following properties of the result r:

• 0 <= r <= n;
• every element with index less than r is at most x;
• every element with index at least r and less than n is greater than x;
• the array is unchanged.

Here element indices range from 0 to n - 1. The C* ghost parameter input records the original array as a list of mathematical integers. ilength input is its length, and inth j input is its element at integer index j. store_int_array a n input describes ownership and contents of the whole array; preserving this assertion with the same input requires the array to remain unchanged. Arithmetic in contracts is mathematical integer arithmetic; the executable program uses signed 32-bit C integers.

Do not change the executable C code, function signature, ghost parameter, or supplied function specification. Keep problem.h unchanged. You may add proof-only definitions, lemmas, helper functions, and annotations in starter.c. Submit the completed starter.c; no main function or input/output handling is needed. The judge checks that the fixed program and specification are preserved. The verification task is safety and partial correctness.

中文

题目描述

给定长度为 n 的严格递增整数数组 a 和整数 x，使用二分搜索，查找满足 a[i] > x 的最小下标 i。

下标从零开始。如果不存在这样的下标，则返回 n。特别地，空数组的返回值为零。数组内容必须保持不变。

给定函数如下：

int binary_search_upper_bound(int *a, int n, int x);

前置条件

• 0 <= n <= 100000。
• 数组长度恰好为 n。
• 数组中的每个元素以及 x 均为 32 位有符号整数。
• 对所有 0 <= i < j < n，有 a[i] < a[j]。

验证任务

请在 starter.c 中添加循环不变式及必要的内部证明标注。你需要证明内存安全性、无有符号整数溢出，以及返回值 r 的以下性质：

• 0 <= r <= n；
• 下标小于 r 的每个元素均不大于 x；
• 下标不小于 r 且小于 n 的每个元素均大于 x；
• 数组内容保持不变。

这里的元素下标范围为 0 到 n - 1。C* 幽灵参数 input 用数学整数列表记录原始数组内容。ilength input 表示其长度，inth j input 表示整数下标 j 处的元素。store_int_array a n input 描述整个数组的内存所有权及内容；保留使用同一 input 的断言，要求数组内容保持不变。契约中的运算使用数学整数，可执行程序则使用 32 位有符号 C 整数。

不得修改可执行 C 代码、函数签名、幽灵参数或给定的函数规约。请保持 problem.h 不变。你可以在 starter.c 中添加仅用于证明的定义、引理、辅助函数和标注。提交完成后的 starter.c 即可，不需要编写 main 函数或输入输出代码。评测机会检查固定程序及规约是否得到保留。本题要求验证安全性和部分正确性。

Examples / 示例

For a = [1, 3, 5, 7] / 当 a = [1, 3, 5, 7] 时：

For a = [], the return value is 0 for every allowed x.

当 a = [] 时，对任意满足前置条件的 x，返回值均为 0。