Page 395 - Discrete Mathematics and Its Applications

374 5 / Induction and Recursion

Example 2 illustrates how this rule of inference is used.
EXAMPLE 2 Verify that the program segment

if x> y then
y := x

is correct with respect to the initial assertion T and the final assertion y ≥ x.

Solution: When the initial assertion is true and x> y, the assignment y := x is carried out.
Hence, the final assertion, which asserts that y ≥ x, is true in this case. Moreover, when the
initial assertion is true and x> y is false, so that x ≤ y, the final assertion is again true. Hence,
using the rule of inference for program segments of this type, this program is correct with respect
to the given initial and final assertions. ▲

Similarly, suppose that a program has a statement of the form

if condition then
S 1
else
S 2

If condition is true, then S 1 executes; if condition is false, then S 2 executes. To verify that this
program segment is correct with respect to the initial assertion p and the final assertion q,two
things must be done. First, it must be shown that when p is true and condition is true, then q
is true after S 1 terminates. Second, it must be shown that when p is true and condition is false,
then q is true after S 2 terminates. This leads to the following rule of inference:

(p ∧ condition){S 1 }q
(p ∧¬condition){S 2 }q

∴ p{if condition then S 1 else S 2 }q.

C. ANTHONY R. HOARE (BORN 1934) Tony Hoare was born in Colombo, Ceylon (now known as Sri
Lanka), where his father was a civil servant of the British Empire and his mother’s father owned a plantation.
He spent his early childhood in Ceylon, moving to England in 1945. Hoare studied philosophy, together with
the classics, at the University of Oxford, where he became interested in computing as a result of his fascination
with the power of mathematical logic and the certainty of mathematical truth. He received his bachelors degree
from Oxford in 1956.
Hoare learned Russian during his service in the Royal Navy, and latter studied the computer translation of
natural languages at Moscow State University. He returned to England in 1960, taking a job at a small computer manufacturer,
where he wrote a compiler for the programming language Algol. In 1968, he became Professor of Computing Science at the Queen’s
University, Belfast; in 1977, he moved to the University of Oxford as Professor of Computing; he is now Professor Emeritus. He is a
Fellow of the Royal Society and also holds a position at Microsoft Research in Cambridge.
Hoare has made many contributions to the theory of programming languages and to programming methodology. He was first
to define a programming language based on how programs could be proved correct with respect to their specifications. Hoare also
invented quick sort, one of the most commonly used sorting algorithms (see the preamble to Exercise 50 in Section 5.4). He received
the ACM Turing Award in 1980 and in 2000 he was knighted for services to education and computer science. Hoare is a noted writer
in the technical and social aspects of computer science.