Given the following pre and post conditions identify as many loop invariants as you can:

Pre-Condition: x > 0 y > 0 x = x₀y = y₀

Post-Condition: z = x₀ + y₀

method add(int x, int y) return int z

{

z := x

while(y != 0)

{

z:= z + 1;

y:= y - 1;

}

return z;

}