Hoare Logic inference

Question

which corresponds to the series 0+1+2+3+ … +n with 0 being the 0th triangular number, 1 being the 1st, 3 being the 2nd, 6 being the 4th and so on. Prove the program is correct using Hoare logic inference rules (precondition and postcondition have been given).

{n>=0}

x := n;

z := 0;

WHILE (x!=0) {

z := z+x;

x := x-1;

}

{z*2=n*(n+1)}

note Start by identifying the loop invariant then apply Hoare logic inference rules

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 n >= 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 the

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}

x := n;

B: {0 = (n-x)(n+x+1)}

z := 0;

I: {2z = (n-x)(n+x+1)}

WHILE (x != 0) {

C: {2(z+x) = (n-x+1)(n+x)}

z := z + x;

D: {2z = (n-x+1)(n+x)}

x = x - 1;

I: {2z = (n-x)(n+x+1)}

}

E: {2z = n(n+1)}

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 & x=0 ==> E (2)

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

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

{A} x := n {B} (3)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

From (8) by the Rule of While loop

{I} z := z + x; x := x - 1 {I}

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

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

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

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

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

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

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

{A} x := n {B}, {B} z := 0 {I}, {I} WHILE (x != 0) {z := z + x; x := x - 1} {E}

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

{A} x := n; z := 0; WHILE (x != 0) {z := z + x; x := x - 1} {E}

That completes the proof.