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

No correct solution

Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange
scroll top