Come cambiare le implicazioni dell'algoritmo cambiando l'invariante?

Question

Ho questa specifica in GCL:

$ [Ctx c: n geqslant 0 wedge b: [0..n-1] text {di int} $

$ {Q: text {true} } $

$ Sum, i: = 0,0; $

$ { text {invariant} p: 0 leqslant i leqslant n wedge sum = sum_ {j = 0}^{i-1} b [j] } $

$ {T: ni } $

$ do i neq n destrorrow sum, i: = sum+b [i], i+1; od $

$ {R: sum = sum_ {j = 0}^{n-1} b [j] } $

$]$

Ma poi mi è stato chiesto di sviluppare la stessa somma dei numeri situati in $ b $ ma con la seguente funzione invariante e dimensionale ($ t $):

$ { text {invariant} p: 0 leqslant i leqslant n wedge sum = sum_ {j = i}^{n-1} b [j] } $

e

$ {T: i } $

Ma non ho come procedere. Quello che in primo luogo ho supposto è che la somma deve essere fatta in ordine inverso.

Qualche suggerimento, idee?