How to change the algorithm implication by changing the invariant? I have this specification in GCL:

$[Ctx C: n\geqslant 0\ \wedge\ b:[0..n-1]\ \text{of 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:n-i\}$

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

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

$]$

But then I have been requested to develop the same summation of the numbers located in $b$ but with the following invariant and dimension function ($T$):

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

and

$\{T:i\}$

But I don't how to proceed. What I firstly supposed is that the summation must be done in reverse order.

Some suggestion, ideas?
Well, the new invariant does not hold in the code you posted, so I guess you are asked to change the code accordingly.


  What I firstly supposed is that the summation must be done in reverse order.


That might be a wise choice. You could try something like this:

$$
\begin{array}{l}
sum,i:=0,n;
\\
\{\text{Invariant}\ P: 0\leqslant i \leqslant n\ \wedge sum=\sum_{j=i}^{n-1} b[j]\}
\\
\{T:i\}
\\
do\ i\neq 0 \rightarrow\ sum, i:=sum+b[i-1],i-1;\ od
\\
\{R: sum=\sum_{j=0}^{n-1} b[j]\}
\end{array}
$$

I have not checked that this Hoare triple is valid, but it should be, possibly with some minor changes.