How to get Loop invariants to prove program is correct in Hoare logic

Question

start off stating the definition of a loop invariant. It is a condition that must be true at the start of the loop and must be true after each iteration of the loop. I understand what it is but i have trouble trying to come up with one.

Here below is a program which i know is correct and I have stated the loop invariant. Could someone please go through explaining simply why this is the loop invariant. I've been looking at it for awhile now but cannot see why the loop invariant is what it is. I am very new to Hoare logic.

{N >=0}//Pre condition

x = 1;

i = 0;

{x == A^i}//Invariant

while (i != N)

{x == A^i || i != N}//Invariant and Guard

x = x * A;

i = i + 1;

{x == A^i} //invariant

{x == A^i    ||    i==N}// Invariant and !Guard

{x == A^N}//Post condition

Answer 1

By definition, an invariant of while guard do c is a property I for which {I && guard} c {I} is a valid Hoare triple.

In your case, it is enough to prove the validity of what you wrote in the body, namely

{x == A^i && i != N}//Invariant and Guard
x = x * A;
i = i + 1;
{x == A^i} //invariant

This can be done using the rules for assignment and composition. Usually, it's best to proceed backwards, from the bottom of the code block, recovering the (weakest) precondition in the process.

{x == A^i && i != N}
{x*A == A^(i+1)}
x = x * A;
{x == A^(i+1)}
i = i + 1;
{x == A^i}

We now get two Hoare assertions one after the other at the top. This means that we proved the validity of

{x*A == A^(i+1)}
x = x * A;
i = i + 1;
{x == A^i}

when we actually need instead

{x == A^i && i != N}
x = x * A;
i = i + 1;
{x == A^i}

For that, we can exploit the weakening rule (AKA "Pre-" or "PrePost" rule). Such rules simply states that we need to prove the implication between the topmost assertion and the other one. Concretely, we need to prove the implication

(x == A^i && i != N)
   ==>
(x*A == A^(i+1))

which trivially follows by arithmetic.