Question

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?

No correct solution

Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange
scroll top