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 结束，则算法产生正确的结果
• 证明如果循环正常结束，算法也会产生正确的结果