我想找到一个反转数组的程序的完整性，即如果我的前提是arr = [a_1,a_2,...,a_n]，其中n> = 1，那么我的后置条件就是arr' = [a_n,a_n-1,a_1]。

算法如下：

i <- 1
j <- n
while i < n
    swap(arr[i],arr[j])
    i <- i + 1
    j <- j - 1
endwhile

return arr

我选择的循环不变式是：[i，j]范围内的arr元素保持不变，而[i，j]范围外的元素相互交换。

现在我没有在循环的不变式中指定交换的数学定义，因为我假设在每次迭代中，元素arr [i]和arr [j]都会根据算法相互交换。

我已经验证了初始步骤和归纳步骤的循环不变性，但是当涉及到循环终止时的状态时，我不确定，因为循环终止于n / 2次迭代，其中i = 1 + n/2和j = n - n/2 = n/2（i！i = n/2和j = n - (n/2 - 1) = n/2 + 1中，因此范围为[n / 2，n / 2 + 1]，这与循环终止。我认为这是错误的，因为它断言在循环终止后两个最中间的元素没有相互交换，但实际上，当循环结束时，满足了后置条件。

我认为我对此太过古怪，但是尽管我认为我的循环不变式是正确的，但是我无法说出我的循环终止时是否为真。也许我在思考为什么数学不适合最终情况时犯了一些错误的数学直觉，所以请帮助我了解为什么我错了，或者如果我错了，我缺少的关键因素是什么。