How to get Loop invariants to prove program is correct in Hoare logic
By definition, an invariant of while guard do c is a property I for which {I &amp;&amp; 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 &amp;&amp; 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 &amp;&amp; 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 &amp;&amp; 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 &amp;&amp; i != N)
   ==&gt;
(x*A == A^(i+1))


which trivially follows by arithmetic.