Hoare Logic, en boucle avec '<='

Question

Je travaille sur une logique Hoare et je me demande si mon approche est la bonne.

je le programme P suivant:

s = 0 
i = 1 
while (i <= n) { 
    s = s + i 
    i = i + 1 
} 

Il devrait satisfaire le triple Hoare {n> = 0} P {s = n * (n + 1)/2} (donc il faut juste la somme). Maintenant, initialement j'avais | s = i * (i-1)/2 | comme mon invariant, ce qui fonctionne bien. Cependant, j'ai eu un problème d'aller à la fin de ma boucle, à mon postcondition désiré. Parce que pour la impliciation

|s = i*(i-1)/2 & i > n| 
=> 
| s = n * (n+1)/2 | 

à tenir, je dois prouver que i est n + 1, et non pas seulement Importe plus grand que n. Alors ce que je pensais est d'ajouter un (i < = n + 1) à l'invariant, de sorte qu'il devient:

|s = i * (i-1)/2 & i <= n+1| 

Ensuite, je peux prouver le programme que je pense qu'il devrait être correct. Néanmoins, je trouve l'invariant un peu moins "invariant" :). Et pas comme tout ce que j'ai vu dans le cours ou dans les exercices jusqu'à présent, alors je me demandais s'il y avait une solution plus élégante ici?

Answer 1

Alors ce que je pensais est d'ajouter un (i < = n + 1) à l'invariant, de sorte qu'il devient:

|s = i * (i-1)/2 & i <= n+1| 

Néanmoins, je trouve l'invariant être un peu, moins "invariant" :). Et pas comme tout ce que j'ai vu dans le cours ou dans les exercices jusqu'à présent, alors je me demandais s'il y avait une solution plus élégante ici?

Non, étant donné la façon dont le code est écrit, c'est exactement le chemin à parcourir. (Je peux dire d'expérience depuis que j'ai enseigné la logique Hoare pendant plusieurs semestres dans deux cours différents et puisque cela fait partie de mes études supérieures.)

L'utilisation de i <= n est considérée comme une bonne pratique lors de la programmation. Dans votre programme particulier cependant, vous pourriez tout aussi bien écrit i != n+1 à la place, dans ce cas, votre premier invariant (qui semble en effet plus propre) aurait suffi puisque vous obtenez

| s=i*(i-1)/2 & i=n+1 | 
=> 
| s=n*(n+1)/2 | 

qui tient évidemment.