Question

What is the relationship between loop invariant, loop condition, and the input-output recursively?

Answer 1

A loop invariant is a condition [among program variables] that is necessarily true immediately before and immediately after, each iteration of a loop. A loop invariant is some condition that holds for every iteration of the loop.