94
Formal Logic
12. Verify the correctness of the following program segment with the precondition and postcondition shown.
{x = 7}
if x <= 0 then
y = x
else
y = 2 * x
end if
{y = 14}
13. Verify the correctness of the following program segment with the precondition and postcondition shown.
{x ≠ 0}
if x > 0 then
y = 2 * x
else
y = (−2) * x
end if
{y > 0}
14. Verify the correctness of the following program segment to compute min(x, y), the minimum of two distinct values x and y.
{x ≠ y}
if x <= y then
min = x
else
min = y
end if
15. Verify the correctness of the following program segment to compute |x|, the absolute value of x, for a
nonzero number x.
{x ≠ 0}
if x >= 0 then
abs = x
else
abs = −x
end if
16. Verify the correctness of the following program segment with the assertions shown.
{z = 3}
x = z + 1
y = x + 2
{y = 6}
if y > 0 then
z = y + 1
else
z = 2 * y
end if
{z = 7}