SE 504
Development of a program to compute prefix sums

Let b be an integer array. Suppose that we want to develop a program that establishes, for all i satisfying 0≤i<#b,

b.i = B.0 + B.1 + ... + B.i

where (rigid/ghost variable) B refers to the original contents of b. Intuitively, this means that we want to replace the value in each element of b by the sum of all the values (originally) occupying the prefix of b up to and including that element. For example:

Before: 
    0   1   2   3   4   5   6   7
  +---+---+---+---+---+---+---+---+
B | 3 | 9 |-4 | 6 |-1 | 9 | 0 |-5 |
  +---+---+---+---+---+---+---+---+
After: 
    0   1   2   3   4   5   6   7
  +---+---+---+---+---+---+---+---+
b | 3 |12 | 8 |14 |13 |22 |22 |17 |
  +---+---+---+---+---+---+---+---+

A formal specification is as follows: 

|[var b : array of int;  { b=B }

  b := ?

  {Q: (∀i | 0≤i<#b : b.i = prefixSum.i) }
]|
where prefixSum.m = (+j | 0≤j≤m : B.j).

Clearly, to solve this we should use a loop. As a first step in developing the program, we employ the heuristic of replacing a constant (in the postcondition Q) by a fresh variable and adding a new conjunct stating that the fresh variable is equal to that constant. (This yields Q', a slightly strengthened form of the postcondition.) Choosing to replace constant #b by (fresh variable) n, we get

Q' : (∀i | 0≤i<n : b.i = prefixSum.i)   ∧   n = #b

We take the modified postcondition (not including the new conjunct) to be a candidate for a loop invariant and the negation of the new conjunct (n ≠ #b) to be the loop guard. The loop body should involve changes to n and b. We get: 

|[var b : array of int;  { b=B }
  var n : int;

  n := E;
  {loop invariant I: (∀i | 0≤i<n : b.i = prefixSum.i) }
  do n ≠ #b  --->  n, b := F, G;
  od
  {Q': (∀i | 0≤i<n : b.i = prefixSum.i) ∧ n = #b }
  {Q: (∀i | 0≤i<#b : b.i = prefixSum.i) }
]|

The obvious initialization for n is to make it zero, as that truthifies I (by Gries & Schneider's (8.13)). Considering this, together with the loop guard, the obvious modification to n inside the loop is to increment it. This suggests that 0≤n≤#b is also an invariant of the loop, which could turn out to be important (especially in showing item (iv) on the loop checklist). It also suggests that G be of the form b(n:E). That is, it would seem likely that each iteration of the loop should modify b.n. Our proposed program is then 

|[var b : array of int;  { b=B }
  var n : int;

  n := 0;
  {loop invariant I: I1 ∧ I2, where
     I1: (∀i | 0≤i<n : b.i = prefixSum.i),
     I2: 0≤n≤#b
  }
  {bound: #b - n}
  do n ≠ #b  --->  n, b := n+1, b(n:E);
  od
  {Q': (∀i | 0≤i<n : b.i = prefixSum.i) ∧ n = #b }
  {Q: (∀i | 0≤i<#b : b.i = prefixSum.i) }
]|

To calculate E, we attempt to prove item (ii) of the loop checklist. (Note the use of the Irrelevant Array Element Axiom.)

To be proved: 
{I ∧ B} n, b := n+1, b(n:E) {I}  (i.e., [I ∧ B  ⇒ wp.(n,b:=n+1,b(n:E)).I])

Assume I (I1 and I2) and B.

    wp.(n,b := n+1,b(n:E)).I

 =    < wp law, defn. of I, text. sub >

    (∀i | 0≤i<n+1 : b(n:E).i = prefixSum.i)

 =    < (8.23) split off term (note importance here of assumption 0≤n) >

    (∀i | 0≤i<n : b(n:E).i = prefixSum.i)  ∧  b(n:E).n = prefixSum.n

 =    < b(n:E).n = E by defn of b(n:E) >

    (∀i | 0≤i<n : b(n:E).i = prefixSum.i)  ∧  E = prefixSum.n

 =    < b(n:E).i = b.i for all i<n; hence, it follows from the
        Irrelevant Array Element Axiom (instantiated by
        R := 0≤i<n, b := b, i := i, P := b.i = prefixSum.i,
        k := n, E := E, and * := ∧) that "b(n:E)" in the body 
        of the quantification can be replaced by "b"            >

    (∀i | 0≤i<n : b.i = prefixSum.i)  ∧  E = prefixSum.n

 =    < 1st conjunct above is assumption I1; (3.39) >

    E = prefixSum.n

 =    < defn of function prefixSum >

    E = (+j | 0≤j≤n : B.j)
   
 =    < (8.23) Split Off Term (note importance of assumption n≥0) >

    E = (+j | 0≤j<n : B.j)  +  B.n

 =    < j<n = j≤n-1 (due to j and n being integers) >

    E = (+j | 0≤j≤n-1 : B.j)  +  B.n

 =    < defn of prefixSum >

    E = prefixSum.(n-1)  +  B.n

 =    < by assumption I1, b.(n-1) = prefixSum.(n-1) >

    E = b.(n-1) + B.n

As B is only a rigid variable (or what some authors call a ghost variable or specification constant), and not a variable (or constant) that can be referred to in the (executable code within the) program, we are not done. Yet we realize that the loop invariant must say something about B.n, or else there is no way to proceed. Examining the program, we notice that, as any given iteration of the loop begins, the only elements of b that have been modified (during previous iterations) are those in b[0..n). Thus, it is clear that B.n = b.n is an invariant of the loop. Indeed, we can make the stronger statement that B[n..#b) = b[n..#b) (which, of course, is an abbreviation for (∀j | n≤j<#b : B.j = b.j)) is an invariant of the loop. (It turns out that we must make this stronger statement in order to be able to prove (ii) on the loop checklist (i.e., that I is a loop invariant). This is an example, not infrequently observed in proofs by mathematical induction, of where it is easier to prove a stronger statement than to prove a weaker one. This is not really a paradox; rather, it arises because by choosing to prove a stronger statement, you have the advantage of exploiting a stronger induction hypothesis.) Using this, we continue as follows: 

    E = b.(n-1) + B.n

 =    < assume I has been augmented to include
        B[n..#b) = b[n..#b) as a new conjunct  >

    E = b.(n-1) + b.n

Thus, we have calculated an expression for E. The resulting program is 

|[var b : array of int;  { b=B }
  var n : int;

  n := 0;
  {loop invariant I: I1 ∧ I2 ∧ I3, where
     I1: (∀i | 0≤i<n : b.i = prefixSum.i),
     I2: 0≤n≤#b,
     I3: b[n..#b) = B[n..#b)
  }
  {bound: #b - n}
  do n ≠ #b ---> n, b := n+1, b(n : b.(n-1) + b.n);
  od
  {Q': (∀i | 0≤i<n : b.i = prefixSum.i) ∧ n = #b }
  {Q: (∀i | 0≤i<#b : b.i = prefixSum.i) }
]|

However, this program is faulty because during the loop's first iteration an access will be made to b[-1], which does not exist. To repair this, we can initialize n to 1 rather than to 0. The value in location zero ought to remain there anyway (because prefixSum.0 = B.0), so there is no need for a loop iteration in which an assignment is made to b.0.

Oh, but initializing n to 1 fails to establish loop invariant I2 in the case #b = 0, and so the precondition needs to be strengthened slightly to #b > 0. If we insist on our program handling the case #b = 0, we can nest our program inside a selection command (i.e. if-else statement) so that it executes only in the case that #b>0. The opposite branch will do nothing.

Choosing the option of strengthening the pre-condition (which also allows I2 to be strengthened to say 0<n), the final program is 

|[var b : array of int;  { b=B ∧ #b > 0 }
  var n : int;
  n := 1;
  {loop invariant I: I1 ∧ I2 ∧ I3, where
     I1: (∀i | 0≤i<n : b.i = prefixSum.i),
     I2: 0<n≤#b,
     I3: b[n..#b) = B[n..#b)
  }
  {bound: #b - n}
  do n ≠ #b ---> n, b := n+1, b(n : b.(n-1) + b.n);
  od
  {Q: (∀i | 0≤i<#b : b.i = prefixSum.i) }
]|

Of course, the more usual way of writing the assignment to b is

b.n := b.(n-1) + b.n

There is yet another issue to address. In calculating the right-hand side of the assignment to b, we strengthened the loop invariant to include the new conjunct b[n..#b) = B[n..#b). Having done so, we are responsible for showing that execution of the loop body preserves this new conjunct. Now, intuitively it is obvious that if we modify b.n but also increment n, then the truth of b[n..#b) = B[n..#b) is preserved. (Note that the modified array element is now b.(n-1), on which this condition does not depend.) But let's prove it formally, so as to illustrate, once again, the use of the Irrelevant Array Element Axiom. What we want to show is

{I ∧ B} n, b := n+1, b(n : b.(n-1) + b.n) {I}

Our previous work has demonstrated that

{I ∧ B} n, b := n+1, b(n : b.(n-1) + b.n) {I1 ∧ I2}

Hence, it remains to show

{I ∧ B} n, b := n+1, b(n : b.(n-1) + b.n) {I3}

By the relationship between Hoare Triples and wp, this is equivalent to

[I ∧ B  ⟹  wp.(n, b := n+1, b(n : b.(n-1) + b.n)).I3]

We assume the antecedent, I ∧ B, and show the consequent: 

Assume I (i.e., I1, I2, and I3) and B.

     wp.(n, b := n+1, b(n : b.(n-1) + b.n)).I3]

  =    < wp assignment law >

     I3(n, b := n+1, b(n : b.(n-1) + b.n))

  =    < defn of I3 >

     (∀i | n≤i<#b : b.i = B.i)(n, b := n+1, b(n : b.(n-1) + b.n))

  =    < textual substitution >

     (∀i | n+1≤i<#(b(n:b.(n-1)+b.n)) : b(n : b.(n-1) + b.n).i = B.i)

  =    < length of array b is same as length of array b(n:E) (no matter what E is) >

     (∀i | n+1≤i<#b : b(n : b.(n-1) + b.n).i = B.i)

  =    < Irrelevant Array Element Axiom, with instantiation 
         R := n+1≤i<#b, b := b, i := i, P := b.i = B.i,
         k := n, E := b.(n-1) + b.n, and * := ∧  
         That is, because i iterates over a range that does not
         include n, b(n:E).i is equivalent to b.i                >

     (∀i | n+1≤i<#b : b.i = B.i)

 <==   < (3.76b) >

     b.n = B.n ∧ (∀i | n+1≤i<#b : b.i = B.i)

  =    < split off term (8.23) (assumptions I2 and B yield n<#b) >

     (∀i | n≤i<#b : b.i = B.i)

  =    < assumption I3 >

     true

Returning to our claim that I3 needed to be b[n..#b) = B[n..#b) rather than the weaker b.n = B.n, suppose that I3 had been the latter. Then the proof above would have led to the expression b.(n+1) = B.(n+1), which could not be resolved, because the assumption b.n = B.n could not be applied to argue for its being true.