SE 504
Solution to Array Decomposition Problem

Develop a program to satisfy the following specification. 

|[ con N : int; { N > 0 }
   con F : array [0..N) of int;
   var h : array [0..N) of int;

   h := ?

   {Q: (∀k | 0≤k<N : F.k = (+i | 0≤i≤k : h.i)) |
]|

In words, the goal is to place values into array h so that, for each k, the sum of the elements in h[0..k] is equal to F.k.

As an example, the arrays F and h shown here are consistent with the postcondition: 

  +----+----+----+----+----+----+----+----+
F |  3 | 12 | -5 |  6 |  0 | 13 | -2 |  7 |
  +----+----+----+----+----+----+----+----+

  +----+----+----+----+----+----+----+----+
h |  3 |  9 |-17 | 11 | -6 | 13 |-15 |  9 |
  +----+----+----+----+----+----+----+----+

We strengthen the postcondition Q by replacing the constant N by the fresh variable n and adding the conjunct n=N. Then we take the first conjunct as a possible loop invariant and the negation of the second as the guard of the loop. It would appear that, as is often the case, the variable n should be incremented during each loop iteration. In addition, we probably need to modify h on each iteration. This gives rise to 

|[ con N : int; { N > 0 }
   con F : array [0..N) of int;
   var h : array [0..N) of int;
   var n : int;

   n,h := D, E;
   {invariant I: I1 ∧ I2, where 
      I1: (∀k | 0≤k<n : F.k = (+i | 0≤i≤k : h.i)),
      I2: 0≤n≤N
   }
   {bound: N - n}
   do n ≠ N ⟶ n,h := n+1,G;
   od
   {Q: (∀k | 0≤k<N : F.k = (+i | 0≤i≤k : h.i)) }
]|

To make initialization easy, we could take D to be 0. That would truthify I (by G&S's Theorem (8.13)) and make initialization of h unnecessary. If we were to take D to be 1, then (applying G&S's Theorem (8.14) would lead us to conclude that) to truthify I we would have to initialize h to h(0:F.0). (That is, we would have to assign to h.0 the value of F.0.)

As for G, let us attempt to derive it by showing (ii) of the loop checklist:

{I ∧ B} n,h := n+1,G {I} (i.e., [I ∧ B ⇒ wp.(n,h := n+1,G).I] ) 

Assume I and B.

    wp.(n,h := n+1,G).I

 =     < defn of I, wp assignment law, textual sub >

    (∀k | 0≤k<n+1 : F.k = (+i | 0≤i≤k : G.i))  ∧  0≤n+1≤N 
    
 =     < 2nd conjunct is implied by conjunction of I2 (0≤n≤N) and loop guard (n≠N); (3.39) >

    (∀k | 0≤k<n+1 : F.k = (+i | 0≤i≤k : G.i))

 =     < split off term (8.23) >

    (∀k | 0≤k<n : F.k = (+i | 0≤i≤k : G.i))  ∧  F.n = (+i | 0≤i≤n : G.i)

 =     < assume that G[0..n) =  h[0..n) >

    (∀k | 0≤k<n : F.k = (+i | 0≤i≤k : h.i))  ∧  F.n = (+i | 0≤i≤n : G.i)

 =     < assumption I, (3.39) >

    F.n = (+i | 0≤i≤n : G.i)

 =     < (8.23) split off term (the range is nonempty by assumption n≥0) >

    F.n = (+i | 0≤i<n : G.i) + G.n

 =     < assume (again) that G satisfies G.i = h.i for i satisfying 0≤i<n >

    F.n = (+i | 0≤i<n : h.i) + G.n

At this point, we notice that the first term on the right-hand side looks very much like a subexpression of the first conjunct of our loop invariant. It would look even more similar if we rewrote the inequality i<n as i≤n-1, so we do that now: 

    F.n = (+i | 0≤i<n : h.i) + G.n

 =     < rewrite inequality i<n as i≤n-1 >

    F.n = (+i | 0≤i≤n-1 : h.i) + G.n

The first conjunct of the loop invariant (which we have taken as an assumption, you will recall) says that F.k = (+i | 0≤i≤k : h.i) for every k from zero up to and including n-1. In particular, then, by plugging in n-1 for k we get F.(n-1) = (+i | 0≤i≤n-1 : h.i). Note that this makes sense only for n>0, so now we assume that condition. To justify this step technically, we use a slightly more general form of Gries's and Schneider's (9.13) Instantiation theorem, which we call (9.13') and can be found in the Appendix. Continuing the proof: 

    F.n = (+i | 0≤i≤n-1 : h.i) + G.n

 =     < assumptions I (the loop invariant) and n > 0, and application
         of (9.13') (see Appendix), instantiated by 
         x: k, 
         e: n-1,
         R: 0≤k<n, and
         P: F.k = (+i | 0≤i≤k : h.i)   >

    F.n = F.(n-1) + G.n

 =     < algebra >

    G.n = F.n - F.(n-1)

 =     < choose G to be h(n : F.n - F.(n-1)), so that G.n = F.n - F.(n-1)
         and so that earlier assumption that G.i = h.i for i satisfying
         0≤i<n also holds                                                >

    true

Recall that during the derivation above, we assumed that n>0. Hence, our pre-loop initialization of n should be n:=1 rather than n:=0. Earlier we figured that such an initialization of n requires that h.0 be initialized to F.0. The assignment h := h(n : F.n - F.(n-1)) is usually written h.n := F.n - F.(n-1). The resulting program is 

|[ con N : int; { N > 0 }
   con F : array [0..N) of int;
   var h : array [0..N) of int;
   var n : int;

   n,h.0 := 1,F.0;
   {invariant I: (∀k | 0≤k<n : F.k = (+i | 0≤i≤k : h.i))  ∧  1≤n≤N }
   do n ≠ N ⟶ n, h.n := n+1, F.n - F.(n-1);
   od
   {(∀k | 0≤k<N : F.k = (+i | 0≤i≤k : h.i)) }
]|

Had we recognized from the start that the only modification needing to be made to h on each iteration were to the element h.n, we would have started with our loop body being the assignment

n, h.n := n+1, G;

This would have made the calculation of G somewhat easier.

Appendix: Theorem (9.13')

In Gries & Schneider, Theorem 9.13 (Instantiation) says

(∀x |: P) ⟹ P(x:=e)

Informally, this says that, if every choice of x satisfies P, then e (any expression whose type is compatible with x's) satisfies P.

A somewhat more general form of this theorem is as follows:

Theorem 9.13': R(x:=e) ⟹ ((∀x | R : P) ⟹ P(x:=e))

It is readily seen that (9.13) is obtained from (9.13') by taking R to be true (and then applying (3.73)).

Informally, (9.13') says that, if e satisfies R and P is satisfied by every x satisfying R, then e satisfies P.

Here is a proof of (9.13'). 

 Assume R(x:=e).

    (∀x | R : P)

=      < (9.2) Trading >

    (∀x |: R ⇒ P)

⇒      < (9.13) Instantiation >

    (R ⇒ P)(x:=e)

=      < textual substitution distributes over operators >

    R(x:=e) ⇒ P(x:=e)

=      < assumption R(x:=e) >

    true ⇒ P(x:=e)

=      < (3.73) true is left identity of ⇒ >

    P(x:=e)