2
$\begingroup$

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?

$\endgroup$
2
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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? $\endgroup$ – InfZero Oct 4 '16 at 1:08
  • $\begingroup$ @InfZero Yes, that's what happens. $\endgroup$ – chi Oct 4 '16 at 7:25
2
$\begingroup$

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] }
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.