最小值算法的正确性

如何解决最小值算法的正确性

我的任务是证明寻找数组中最小元素的索引所用算法的正确性。我想知道我的过程是否正确。任何反馈都很好，因为这是我第一次学习算法，但是我仍然在寻找解决方法。

前提条件：arr[a_1,a_2,a_3,...,a_n]，其中a_i是实数，n> = 1。

后置条件：smallestIndex = m，对于[1，n]中的所有i，为1 arr[m] <= arr[i]。

我的算法：

smallestIndex <- 1
i <- 2
while i <= n
    if arr[i] < arr[smallestIndex]
        smallestIndex <- i
    i <- i + 1
endwhile
return smallestIndex

我的循环不变性：arr[smallestIndex] <= arr[m]对于[1，i-1]范围内的m。

基本步骤：由于smallestIndex <- 1和i <- 2在while循环开始之前，因此对于[1，1]范围内的m，循环不变性“ arr [1]

归纳步骤：假设循环不变性在第k次迭代后为真，然后为smallestIndex <- r，其中1 arr[k+1] < arr[r]，则{ {1}}或其他smallestIndex <- k+1仍为r。在这两种情况下，自smallestIndex开始，对于范围[1，k + 1]中的m，循环不变式仍然成立。这样就解决了归纳步骤。

循环后终止步骤：由于arr[smallestIndex] <= arr[m]在每次迭代后增加1，因此，当i时，循环条件为false，因此循环终止。自i <- n+1起，对于范围[1，n]中的m，循环不变性仍然成立。由于范围[1，n]是数组arr[smallestIndex] <= arr[m]的全长，因此可以说arr是smallestIndex中最小元素的索引。