# 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.

• thanks. It is what I have supposed by simple inspection: the summation starts in the last index of the array and ends in the first position (0). So in this, can we say that the $T$ function 'ends' when $i$ reaches the $0$ value? – InfZero Oct 4 '16 at 1:08
• @InfZero Yes, that's what happens. – chi Oct 4 '16 at 7:25

We wish to establish

R : sum = ∑ j : 0..n-1 • b[j]


using invariant

P : 0 ≤ i ≤ n ∧ sum = ∑ j : i..n-1 • b[j]


Well we clearly have P ⇒ R if we know i = 0, so let's use a loop with its negation as guard.

Now this loop will terminate if we reduce i, so let's place i ≔ i -1 in the loop body while also attempting to maintain P; i.e., solve for X in P ∧ i ≠ 0 ⇒ P [sum, i ≔ X , i - 1 ].

Indeed, let us assume P and i ≠ 0 and solve for X:

  P [sum, i ≔ X , i - 1 ]
≡⟪ definition of P and substitution ⟫
0 ≤ i - 1 ≤ n ∧ X = ∑ j : i-1..n-1 • b[j]
≡⟪ arithmetic ⟫
1 ≤ i ≤ n + 1 ∧ X = ∑ j : i-1..n-1 • b[j]
≡⟪ Assumptions i ≠ 0 and P ensure 1 ≤ i ≤ n + 1 ⟫
X = ∑ j : i-1..n-1 • b[j]
≡⟪ quantifiers: term split off rule ⟫
X = b[i - 1] + ∑ j : i..n-1 • b[j]
≡⟪ assumption P yields sum = ∑ j : i..n-1 • b[j] ⟫
X = b[i - 1] + sum


Hence, we have arrived at the appropriate loop-body by mere calculation: sum, i ≔ b[i - 1] + sum, i - 1.

Of course our loop will not begin if our variables are not initialized correctly, and indeed P, that is 0 ≤ i ≤ n ∧ sum = ∑ j : i..n-1 • b[j] is easily truthified by setting i ≔ 0, since 0 ≤ n, resulting in an empty sum and thus sum ≔ 0.

In summary, we have calculated

{ 0 ≤ n }
sum, i ≔ 0, n
{ Invaraint: 0 ≤ i ≤ n ∧ sum = ∑ j : i..n-1 • b[j]
bound: i }
do i ≠ 0 → sum, i ≔ b[i - 1] + sum, i - 1 od
{ sum = ∑ j : 0..n-1 • b[j] }