Incorrect Answer.
We consider the body of the program's only while-statement
z = z + a;
a = a + 1;
To see whether
z = a(a + y) 
is an invariant for the while-statement,
we place it as a postcondition at the bottom of the loop-body and
push it upwards through that body to determine the weakest
precondition that guarantees
z = a(a + y)
to hold after the execution of the loop's body:
(z + a) = (a + 1)((a+1) + y) Weakest Precondition
z = z + a;
z = (a + 1)((a+1) + y) Assignment
a = a + 1;
z = a(a + y) Assignment
- The weakest precondition we determined is
(z + a) = (a + 1)((a+1) + y) .
- With that at hand, the postcondition z = a(a + y) is an invariant for the
program's only while-statement if, and only if,
the weakest precondition is implied by the invariant candidate
z = a(a + y)
in conjunction with the condition of the while-statement's boolean
guard a != y+1.
- However, the implication
(a = y + 1) 
(z = a(a + y))
((z + a) = (a + 1)((a+1) + y)) is not true in general.
(Please find values for a, x, y, and z for which this implication is false.)
Back to Question.
Next Question.