この小さなコード体系では、どのようにループ不変式を見つけることができますか？

Question

前提条件：intのリストlen（リスト）> = 2

後条件：2番目に小さい値を返します。リストに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