如何找到這個小代碼體的循環不變式？

Question

前提條件：len（list）> = 2的整數列表

後置條件：返回第二小的值。如果列表中存在兩個最小值，則返回最小值。

def SecondSmallest(list): 
1 smallest = min(list[0], list[1]) 
2 second_smallest = max(list[0], list[1]) 
3 i = 2 
4 while i < len(list): 
5  item = list[i] 
6  if item < second_smallest: 
7   if item < smallest: 
8    second_smallest = smallest 
9    smallest = item 
10   else: 
11    second_smallest = item 
12  i += 1 
13 return second_smallest 

很多謝謝。

Answer 1

循環不變是一個謂詞，適用於循環的每一次迭代。 有關更多詳細信息，請參閱What is a loop invariant?。

在您的具體情況下，每次迭代都有1 < i < len(list)。

有關更正式的定義，請參閱：https://en.wikipedia.org/wiki/Loop_invariant