90
Formal Logic
Conditional rule
A conditional statement is a program statement of the form
if condition B then
P 1
else
P 2
end if
When this statement is executed, a condition B that is either true or false is
evaluated. If B is true, program segment P 1 is executed, but if B is false, program
segment P 2 is executed.
A conditional rule of inference, shown in Table 1.19, determines when a
Hoare triple
{Q}s i {R}
can be inserted in a proof sequence if s i is a conditional statement. The Hoare
triple is inferred from two other Hoare triples. One of these says that if Q is true
and B is true and program segment P 1 is executed, then R holds; the other says that
if Q is true and B is false and program segment P 2 is executed, then R holds. This
simply says that each branch of the conditional statement must be proved correct.
tAbLe 1.19
from
can derive
name of Rule
Restrictions on use
{Q ` B} P 1 {R},
{Q ` B9} P 2 {R}
{Q}s i {R }
conditional
s i has the form
if condition B then
P 1
else
P 2
end if
eXAMPLe 45
Verify the correctness of the following program segment with the precondition and
postcondition shown.
{n = 5}
if n >= 10 then
y = 100
else
y = n + 1
end if
{y = 6}
Here the precondition is n = 5, and the condition B to be evaluated is n >= 10. In
order to apply the conditional rule, we must first prove that
{Q ` B} P 1 {R}