Comment trouver la boucle invariante pour ce petit corpus de code?

Question

Pré-condition: liste des entrées où len (liste)> = 2

Post-condition: retourne la deuxième plus petite valeur. S'il existe deux plus petites valeurs dans la liste, retournez le plus petit.

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 

Merci beaucoup.

Answer 1

Un invariant de boucle est un prédicat qui s'applique à chaque itération de la boucle. Voir What is a loop invariant? pour plus de détails.

Dans votre cas spécifique, pour chaque itération, 1 < i < len(list) tient.

Pour une définition plus formelle, voir: https://en.wikipedia.org/wiki/Loop_invariant