I need help with the following question

Question

Hi, I need help with the following question

Prove the program is correct using Hoare logic inference rules where a and b are any two arbitrary numbers.and it is using repeated addition

{b>=0}

w := b;

z := 0;

WHILE (w!=0) {

z := z+a;

w := w-1;

}

{z=a*b}

start by identifying the loop invariant then apply the rules

note: I have used another website to get the answer but they only said it is correct, without any steps or explanation

Answer 1

You are being asked to prove correctness, not total correctness (i.e. termination).

Therefore I will prove correctness only. For that I will ignore the precondition b >= 0,

as that is needed for termination only.

Below is the given program annotated with assertions named A, B, C, D, and specially I.

The assertion I is the loop invariant.

There is no general way to derive loop invariants; if you need help with generating

loop invariant for this particular problem, let me know.

In contrast, the assertions A, B, C, D are generated by mechanical application of the Rule of Assignment.

A: {0 = 0}

w := b;

B: {0 = a(b-w)}

z := 0;

I: {z = a(b-w)}

WHILE (w != 0) {

C: {z+a = a(b-w+1)}

z := z + a;

D: {z = a(b-w+1)}

w = w - 1;

I: {z = a(b-w)}

}

E: {z = ab}

I do not know in what format you present proofs, hope the format below helps.

By arithmetic manipulation we have the following two implications

I ==> C (1)

I & w=0 ==> E (2)

For the four assignments here are the consequences using the Rule of Assignment.

-------------------

{A} w := b {B} (3)

-------------------

{B} z := 0 {I} (4)

-------------------

{C} z := z + a {D} (5)

-------------------

{D} w := w - 1 {I} (6)

From (5) and (6) by the Rule of Composition

{C} z := z + a {D}, {D} w := w - 1 {I}

----------------------------------------

{C} z := z + a; w := w - 1 {I} (7)

From (1) and (7) by the Rule of Consequence

I ==> C, {C} z := z + a; w := w - 1 {I}

--------------------------------------------

{I} z := z + a; w := w - 1 {I} (8)

From (8) by the Rule of While loop

{I} z := z + a; w := w - 1 {I}

--------------------------------------

{I} WHILE (w != 0) {z := z + a; w := w - 1} {I & w=0} (9)

From (9) and (2) by the Rule of Consequence

{I} WHILE (w != 0) {z := z + a; w := w - 1} {I & w=0}

------------------------------------------------------

{I} WHILE (w != 0) {z := z + a; w := w - 1} {E} (10)

From (3), (4) and (10) by the Rule of Composition

{A} w := b {B}, {B} z := 0 {I}, {I} WHILE (w != 0) {z := z + a; w := w - 1} {E}

------------------------------------------------------------------------------------

{A} w := b; z := 0; WHILE (w != 0) {z := z + a; w := w - 1} {E}

That completes the proof.