Integer Square Root by Binary Search / 二分计算根号 n 的整数部分

English

Given an integer n with 0 <= n <= 2147395600, prove that the supplied function integer_sqrt(n) returns the integer r satisfying

0 <= r
r * r <= n < (r + 1) * (r + 1)

The fixed implementation returns 0 immediately when n = 0. Otherwise, it uses binary search over the inclusive interval [1, 46340]. At each step, it computes mid = lo + (hi - lo) / 2. If mid * mid <= n, it records mid in ans and searches above it; otherwise, it searches below it. When the interval is empty, it returns ans.

The implementation and contract are fixed. Add loop invariants and proof code only inside starter.c; changing the implementation or specification is rejected by the judge and consumes an attempt. Submit the completed starter.c. No main function or standard input/output handling is needed.

The inequalities in the contract use mathematical integers. In particular, when r = 46340, (r + 1) * (r + 1) = 2147488281; this specification expression is not evaluated as a C int. The executable multiplication mid * mid must remain within the signed 32-bit integer range.

中文

给定一个整数 n，其中 0 <= n <= 2147395600，请证明给定函数 integer_sqrt(n) 返回满足下列条件的整数 r，即根号 n 的整数部分：

0 <= r
r * r <= n < (r + 1) * (r + 1)

给定实现使用二分查找。当 n = 0 时，直接返回 0；其余情况在闭区间 [1, 46340] 内查找。每次计算 mid = lo + (hi - lo) / 2：若 mid * mid <= n，则将 ans 更新为 mid，并继续查找更大的值；否则继续查找更小的值。当查找区间为空时，返回 ans。

实现和契约均为固定内容。你只能在 starter.c 中添加循环不变式和证明代码；修改实现或规约将被判定为失败，并消耗一次提交机会。提交完成后的 starter.c 即可，不需要编写 main 函数或标准输入输出代码。

契约中的不等式使用数学整数。特别地，当 r = 46340 时， (r + 1) * (r + 1) = 2147488281；该规约表达式不会作为 C 的 int 表达式执行。实际程序中的乘法 mid * mid 则必须保持在 32 位有符号整数范围内。

Examples / 示例