README.md

示例:first_index_ge —— icontract + CrossHair 的真实闭环

对应 C 那边的 examples/abs-int/,但换成 Python 的契约工具链,验证 ../../references/python-contracts.md 里的结论和命令是否准确。

文件

• first_index_buggy.py —— 有 bug 的版本
• first_index_fixed.py —— 修复后的版本

代码

from typing import List
import icontract


@icontract.ensure(lambda result, numbers, threshold:
                   (result == -1 and all(n < threshold for n in numbers))
                   or (result != -1 and numbers[result] >= threshold))
def first_index_ge(numbers: List[int], threshold: int) -> int:
    """Return the first index i such that numbers[i] >= threshold, or -1 if none exists."""
    for i in range(len(numbers) - 1):   # bug: 应该是 range(len(numbers))
        if numbers[i] >= threshold:
            return i
    return -1

range(len(numbers) - 1) 少扫了最后一个元素,导致"唯一满足条件的元素恰好是最后一个"时漏报。

第一步:CrossHair 找反例(实测)

python3 -m crosshair check first_index_buggy.py

实测输出:

first_index_buggy.py:6: error: false when calling first_index_ge([-1, 400], 0) (which returns -1)

first_index_ge([-1, 400], 0) 期望返回 1(因为 400 >= 0),实际返回 -1——off-by-one 被症状化地找出来了,而且是一个干净、可读的具体反例(前提是给参数加了类型标注,否则 CrossHair 可能给出字符串之类语义混乱的反例)。

第二步:修复

for i in range(len(numbers)):   # 修复:去掉 -1
    ...

第三步:CrossHair 确认修复(实测)

python3 -m crosshair check first_index_fixed.py

实测输出:无(退出码 0)——在 CrossHair 的搜索预算内没找到反例。这不是数学证明,只是没搜到,和 WP 的"证明通过"性质不同。

第四步:icontract 运行时检查作对照(实测)

>>> from first_index_buggy import first_index_ge as buggy
>>> buggy([-1, 400], 0)

实测输出(真实抛出的异常,包含具体触发值):

icontract runtime violation: ... 
all(n < threshold for n in numbers) was False, e.g., with
  n = 400
numbers was [-1, 400]
numbers[result] was 400
result was -1
threshold was 0

修复后的版本对同样的输入正常返回 1,无异常。