Question

Verify that the program segment

x : = 2

z : = x + y

if y > 0 then

z : z + 1

else

z : = 0

is correct with respect to the initial assertion x = 3and the final assertion z = 6.

Short answer

Thus, our final assertion z = 6 is satisfied.

Step-by-step solution

Given

In the given question program segment,

x : = 2

z : = x + y

if y > 0 then

z : z + 1

else

z : = 0

We need to satisfy it.

Verify program segment.

In the given question y = 3 is an initial acceleration. Now here assign the first program will x = 2 .

Here we know that x + z is computed and assigned to z.

Then x + y is 2 + 3, the result is z = 5.

Now, here the program will check the condition statement for if else block 3 > 0, so z : = z + 1 is executed and else ignored.

Therefore,

z = 5 + 1 = 6

Hence, our final acceleration is satisfied.