算法正确性证明：循环不变量

找一个在循环中始终成立的性质，证明初始成立、每轮保持、结束时能推出结论。