Design and Analysis of Algorithms

178 Design and Analysis of Algorithms

(k) {?} if x < 0 then y ← – x else y ← x endif

{2 ≤ y ≤ 4}

(l) {?} if x < 0 then y ← x else y ← x – 2

endif {–1 ≤ y ≤ 4}

(m) {?} i ← i + 1 sum ← sum + x(i) {i ∈

Z and n ∈ Z and i ≤ n and sum =

1

i

j

=

∑

x( j)}

7.2 Prove the following propositions, using the

relevant proof rules.

(a) {V1 ∧ B} S1 {P} ∧ {¬ B} S2 {P}⇒

{V1} if B then S1 else S2 endif {P}

(b) {B} S1 {P} ∧ {V2 ∧ ¬ B} S2 {P}⇒

{V2} if B then S1 else S2 endif {P}

(c) {V1} S1 {P} ∧ {V2} S2 {P} ⇒ {V1

∧V2} if B then S1 else S2 endif {P}

7.3 Verify the following correctness proposition,

by applying the proof rule for the

While and

other proof rules ...