ループ変化条件とループ不変条件
出典: フリー百科事典『ウィキペディア(Wikipedia)』 (2020/07/23 09:22 UTC 版)
「制御構造」の記事における「ループ変化条件とループ不変条件」の解説
ループ変化条件(英語版)とループ不変条件は、ループの正しさを表すのに使われる。 現実的には、ループ変化条件とは非負の初期値を持つ整数式である。変化条件はループを回るたびに減少しなければならないが、正しいループ実行の間は負の値になってはならない。ループ変化条件はループが終了するであろうことを保証するのに使われる。 ループ不変条件は、ループを回る前と各反復において真でなければならない表明である。すなわち、ループが正しく終了するには終了条件とループ不変条件が共に真でなければならない。ループ不変条件は、ループ実行中にループの具体的属性を監視するのに使われる。 Eiffelなどのプログラミング言語でループ変化条件とループ不変条件がサポートされている。Javaではアドオンである Java Modeling Language (JML) という仕様で同様のものをサポートしている。
※この「ループ変化条件とループ不変条件」の解説は、「制御構造」の解説の一部です。
「ループ変化条件とループ不変条件」を含む「制御構造」の記事については、「制御構造」の概要を参照ください。
- ループ変化条件とループ不変条件のページへのリンク