Question

Prove that the program segment

y: = 1

z : = x + y

is correct with respect to the initial assertion x = 0 and the final assertion z = 1.

Short answer

Thus, the final acceleration is satisfied.

Step-by-step solution

Segment of a program

A program or segment of a program S is said to be partially correct with respect to the initial statement p and final statement q if p holds for input values S and S then terminates q applies to the output values of S.

The notation p{S}qindicates that the program or program segment, S is partially correct with respect to the initial statement p and the final statement q.

Explanation

Given, y : = 1 , z : = x + y and x = 0 .

The initial assertion p : x = 0 and the final assertion q : z = 0 .

Solution

Suppose that p : x = 0 as per our initial assertion. Here we need to assign p : y = 1 .

Therefore, the x + y is computed and assigned to.

Since x + y is 0 + 1 , the result is z = 1.

Hence, z = 1, the final assertion is satisfied.