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

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
• By the way, AND is conventionally written as && or /\ in ASCII. The notation || is usually used for OR.
– chi
Dec 28, 2017 at 10:57

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}