c - 我如何使用初始化-维护-终止技术证明算法正确？

Question

函数执行过程中必须满足的条件是什么？ (断言)

我想确保我的断言在运行第 i 个循环后描述我所知道的是真的。

int linearsearch(int arr[], int n, int target) {
    for (int i = 0; i < n; i++) {
        if (arr[i] == target) return i;
    }
    return -1;
}

这只是一个迭代线性搜索函数，如果找到目标则返回目标的索引，否则返回 -1。

Answer 1

线性搜索问题的循环不变式必须声明所有之前搜索过的数组元素，即没有一个等于target:

∀ j <i : arr_j ≠ 目标

关于它你需要证明几点:

• 在进入循环之前证明不变量成立
• 证明如果不变量在迭代前成立，那么它在迭代完成后也成立
• 表明如果循环在中间通过 return 结束，则算法产生正确的结果
• 证明如果循环正常结束，算法也会产生正确的结果