In simple words, a loop invariant is some predicate (condition) that holds for every iteration of the loop. For example, let's look at a simple for
loop that looks like this:
int j = 9;
for(int i=0; i<10; i++)
j--;
In this example it is true (for every iteration) that i + j == 9
. A weaker invariant that is also true is that
i >= 0 && i <= 10
.
与恶龙缠斗过久,自身亦成为恶龙;凝视深渊过久,深渊将回以凝视…