不変条件

ループ開始前にも、反復を1回実行するたびにも成立する条件

形式的検証でループのアルゴリズムを証明するために使える

ループ不変条件はループ開始時と反復時の両方で真である必要がある

ループ終了時にループ不変条件とループ終了条件の両方が真であることが保証される