How to get Loop invariants to prove program is correct in Hoare logic
-
05-11-2019 - |
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