Preuve d'invariant de boucle/somme d'une liste/python

[invite01356ec6]

Bonjour,

j'ai un petit soucis de compréhension, j'espère que vous pourrez m'éclairer.

En pyhton, on me donne ce code (qui somme tous les éléments d'une liste):

1 def sum_all(liste):
2     res = 0
3     for item in liste:
4         res += item
5     return res

Dans ce petit code on me dit que l'invariant de boucle est l'assertion suivante:

Ensuite, pour prouver cette assertion, il faut la prouver pour le cas de base, soit S(0)
Or, on me dit que :

et que ceci est bien égale à

Si je ne me trompe pas, faire revient à faire liste[0]+liste[-1] non ? Donc, on additionne le premier élément avec le dernier ce qui est loin de donner 0 dans beaucoup de cas !

Je suis perdu !! Merci d'avance en tout cas...
-----

[imoca]

Bonjour,

il s'agit de la somme sur l'ensemble des j entier supérieur ou égal à zéro et inférieur ou égale à -1, l'ensemble est vide, donc la somme est nulle.

[invite01356ec6]

Ok merci... Juste que le liste[j] me déstabilisait...