私はデータ構造とアルゴリズムの初歩的なコースを取っています。私たちが使用する本は、CLRS による独創的な作品です。章 2.1: 挿入ソートで説明されているように、ループ不変式を理解するのに苦労しています。
その本は次のように述べています。
行 1 ～ 8 の for ループの各反復の開始時に、部分配列 A[1..j -1] は、元は A[1..j-1] の要素で構成されますが、並べ替えられた順序になっています。
今、これは私を困惑させます。最初の反復が開始されたときにこれが保持されるのはなぜですか? ソートされる配列が { 5, 2, 4, 6, 1, 3 } のように見えるとします。for ループの最初の繰り返しが開始されると、 A[1.. j-1] は並べ替えられた順序ではありませんが、繰り返しが終了すると並べ替えられます。
ここで何が欠けていますか？