Section 1.6 Proof of Correctness
93
2. According to the assignment rule, what is the precondition in the following program segment?
{precondition}
x = 2 * x
{x > y}
3. According to the assignment rule, what is the precondition in the following program segment?
{precondition}
x = 3 * x − 1
{x = 2 * y − 1}
4. According to the assignment rule, what is the precondition in the following program segment?
{precondition}
y = 3x + 7
{y = x + 1}
5. Verify the correctness of the following program segment with the precondition and postcondition shown.
{x = 1}
y = x + 3
y = 2 * y
{y = 8}
6. Verify the correctness of the following program segment with the precondition and postcondition shown.
{x > 0}
y = x + 2
z = y + 1
{z > 3}
7. Verify the correctness of the following program segment with the precondition and postcondition shown.
{x = 0}
z = 2 * x + 1
y = z − 1
{y = 0}
8. Verify the correctness of the following program segment with the precondition and postcondition shown.
{x < 8}
z = x − 1
y = z – 5
{y < 2}
9. Verify the correctness of the following program segment to compute y = x(x − 1).
y = x − 1
y = x * y
10. Verify the correctness of the following program segment to compute y = 2x + 1.
y = x
y = y + y
y = y + 1
11. Verify the correctness of the following program segment with the precondition and postcondition shown.
{y = 0}
if y < 5 then
y = y + 1
else
y = 5
end if
{y = 1}