Correct Answer.
We consider the body of the program's only while-statement
z = z + a;
a = a + 1;
To see whether
2z = (a - 1)a 
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
2z = (a - 1)a
to hold after the execution of the loop's body:
2(z + a) = ((a + 1) - 1)(a + 1) Weakest Precondition
z = z + a;
2z = ((a + 1) - 1)(a + 1) Assignment
a = a + 1;
2z = (a - 1)a Assignment
- The weakest precondition we determined is
2(z + a) = ((a + 1) - 1)(a + 1) , which we may simplify to
2(z + a) = a(a + 1) .
- With that at hand, the postcondition 2z = (a -1)a is an invariant for the
program's only while-statement if, and only if,
the weakest precondition is implied by the invariant candidate
2z = (a - 1)a
in conjunction with the condition of the while-statement's boolean
guard a != y+1.
- Indeed, the implication
(a = y + 1) 
(2z = (a - 1)a)
(2(z + a) = a(a + 1)) is true in general.
Back to Question.
Next Question.