How to demonstrate the correctness of a program with a while cycle using Hoare's logic?

Question

How can I demonstrate through Hoare logic the correctness of a program that has a while cycle. It would be fascinating that some one develop it with any example, due to as my problem to solve is:

Precondition={n>0}

cont := n;
sum := 0;
while cont <> 0 do:
    sum := sum + cont;
    cont := cont-1;
endwhile

Postcondition={sum=1+2+...+n}

It is not necessary to develop this example. I just need to understand the procedure because I don't have a practical example. Thanks for your time.

Answer 1

Hoare logic's "while" rule must be applied here:

If a command S satisfies a Hoare triple of the form {P ∧ B} S {P}, then the command while B do S satisfies {P} while B do S {P ∧ ¬B}.

This is the only technique for proving the postcondition of a while loop in Hoare logic, so you must apply it. The condition B and the loop body S are given in the code, but P can be any condition you choose so long as {P ∧ B} S {P} holds.

This Hoare triple asserts that if P is true before an iteration of the loop then it will still be true afterwards, so such a condition P is known as a loop invariant. To prove the postcondition of the loop you need to establish (1) that P is true before the first iteration of the loop, and (2) that P is preserved by the loop body.

The necessary invariant for the loop in your example is sum = n + (n-1) + ... + (cont+1), i.e. the sum of the numbers from cont+1 to n. In general, there is no systematic way to find the right loop invariant to use; you have to use your understanding of the algorithm, and your intuition/experience to come up with one yourself.

---

This is sufficient to show that if the loop terminates then its postcondition will be satisfied; you also need to establish that the loop does terminate. The technique you should apply here is to find a loop variant; this is usually some integer quantity which (1) decreases on each iteration of the loop, and (2) causes the loop to terminate when the quantity reaches zero.

In your example, cont is a loop variant, because the loop decrements cont := cont-1, and the loop condition terminates the loop when cont reaches zero. In general, like finding a useful invariant, there is no systematic procedure which finds a variant in all cases, but you can start by looking at the loop condition to see which variable(s) determine when the loop terminates.