Chapter 10 exercise:

7.6 (just as an illustration of assertions and loop invariants.)

a) After the loop, prod should be 7*lastInt. At the beginning of every iteration, prod should 7*k.

This is the case if k is initialized to any integer value k_init between 0 and lastInt-1, and prod is initialized to 7*k_init. The loop executes lastInt-k_init times. Thus at the end of the loop, prod=7*k_init + 7*(lastInt-k_init)=7*lastInt. If at the beginning of an iteration k=k₁ and prod=7*k=7*k₁, then at the beginning of the next iteration, k=k₁+1 and prod=prod + 7 = 7*(k₁+1)=7*k.
One possible choice is k=0 and prod=0.

b) prod=prod+7 is the primary work, k=k+1 is the make progress part.

c) The loop is infinite if lastInt<k_init, which won't happen if we choose k_init=0,or1, or2, or..., or lastInt-1

d) The assertion doesn't change since the two statements k=k+1 and prod=prod+7 are independent.

e) No change in the loop invariant either: prod=7*k at the start of every iteration.

f)
int k=lastInt;
int prod=0;
while(k!=0){

prod=prod+7;
k=k-1;

}

g)
int k=0; // assume lastInt is >0
int prod=0;
do{

prod=prod+7;
k=k+1;

}while(k!=lastInt);