ループ不変条件

ループの実行前にも、反復するたびにも成立する条件。