Bonsoir,
 
Etant un noob ça va sembler idiot comme question mais comment fait-on des preuves de programme (avec boucle)?
Par exemple, j'ai ça à faire et je sais pas comment m'y prendre:
 
"Prouver que ce programme calcule la somme des n premiers entiers. L'invariant d'itération est s=0+...+(i-1) et i<=n+1.
 
n=sc.nextInt(); s=0; i=1;
while (i <= n){
 s=s+i;
 i=i+1;
}
 
j'imagine qu'il faut noter à coté ce qu'il se passe, mais avec n en lecture interactive je vois pas quand on sait qu'on sort ou quoi. Quelqu'un a une idée?
 
Merci d'avance.
 
edit: personne?? :[