Hoare logic rules

Question

using repeated addition, where a and b are any two arbitrary numbers. Prove the program is correct using Hoare logic inference rules (precondition and postcondition have been given).

{b>=0}

x:= b;

z := 0;

WHILE (x!=0) {

z := z+a;

x := x-1;

}

{z=a*b}

please start by identifying the loop invariant, then apply the Hoare logic inference rules(Specify which rule you are using )

Answer 1

Here is Mira's problem

{b>=0}

w := b;

z := 0;

WHILE (w!=0) {

z := z+a;

w := w-1;

}

{z=a*b}

Here is my solution to her problem. You can adjust it to yours.

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.