Loop Invariant

Kompleksitas menjawab “seberapa cepat”, tetapi tidak menjawab “apakah benar”. Untuk pertanyaan terakhir, kita memerlukan teknik formal pembuktian kebenaran. Loop invariant adalah alat utama untuk membuktikan algoritma iteratif: sebuah properti yang dipertahankan sepanjang eksekusi loop. Pada Chapter ini kita akan mempelajari tiga langkah pembuktian loop invariant — initialization, maintenance, termination — dan menerapkannya pada algoritma klasik seperti linear search dan insertion sort.

Apa itu Loop Invariant #

Loop invariant adalah properti P yang:

1. Initialization — benar sebelum iterasi pertama.
2. Maintenance — bila P benar sebelum iterasi ke-k, maka P tetap benar sebelum iterasi ke-k+1.
3. Termination — saat loop berhenti, P memberikan properti yang berguna untuk menyimpulkan kebenaran algoritma.

Loop invariant mirip dengan induksi matematis: initialization adalah kasus dasar, maintenance adalah langkah induksi, dan termination memberi konklusi praktis.

Memilih Loop Invariant yang Tepat #

Loop invariant yang baik harus:

• Menggambarkan kemajuan algoritma (apa yang sudah dicapai di iterasi k).
• Cukup kuat untuk menyimpulkan kebenaran saat loop berhenti.
• Cukup lemah sehingga maintenance bisa dibuktikan tanpa kesulitan.

Contoh 1: Linear Search #

Misalkan kita ingin membuktikan kebenaran algoritma linear search berikut:

// Mencari indeks target pada array v.
// Mengembalikan indeks jika ketemu, atau -1 jika tidak.
int linearSearch(const std::vector<int>& v, int target) {
    for (std::size_t i = 0; i < v.size(); ++i) {
        if (v[i] == target) return static_cast<int>(i);
    }
    return -1;
}

Loop Invariant #

Pada awal setiap iterasi i, properti berikut benar:

P(i): target tidak ditemukan pada v[0], v[1], ..., v[i-1].

Pembuktian #

Initialization (sebelum i = 0): rentang v[0..-1] kosong, sehingga pernyataan “target tidak ditemukan pada rentang kosong” benar secara trivial. ✓

Maintenance: asumsikan P(i) benar sebelum iterasi ke-i. Iterasi memeriksa v[i]. Bila v[i] == target, algoritma kembali (return). Bila tidak, iterasi berlanjut ke i + 1, dan P(i+1) kini menyatakan target tidak ditemukan pada v[0..i] — yang benar karena P(i) benar dan v[i] != target. ✓

Termination: loop berhenti saat i == v.size(). Pada titik ini, P(v.size()) menyatakan target tidak ditemukan pada v[0..v.size()-1], yaitu seluruh array. Algoritma mengembalikan -1 dengan benar. Bila loop keluar lebih awal karena v[i] == target, algoritma mengembalikan i dengan benar. ∎

Contoh 2: Insertion Sort #

Insertion sort sedikit lebih kompleks karena mempertahankan dua properti sekaligus: array awal tetap utuh sebagai prefix, dan prefix tersebut terurut.

Loop Invariant #

Pada awal setiap iterasi i (mulai dari 1), properti berikut benar:

P(i): sub-array v[0..i-1] berisi elemen-elemen yang sama dengan sub-array asli v[0..i-1] (sebelum sorting), tetapi sudah terurut menaik.

Pembuktian #

Initialization (sebelum i = 1): v[0..0] berisi satu elemen, yang sudah terurut secara trivial. Elemen-elemennya sama dengan array asli karena belum ada perubahan. ✓

Maintenance: asumsikan P(i) benar. Iterasi i mengambil key = v[i], lalu menggeser elemen v[0..i-1] yang lebih besar dari key ke kanan satu posisi, sampai menemukan posisi yang tepat. Setelah iterasi, v[0..i] terurut dan berisi elemen yang sama dengan array asli v[0..i]. Maka P(i+1) benar. ✓

Termination: loop berhenti saat i == v.size(). Pada titik ini, P(v.size()) menyatakan v[0..v.size()-1] (yaitu seluruh array) berisi elemen yang sama dengan array asli dan sudah terurut menaik. Inilah spesifikasi insertion sort. ∎

Kode: Verifikasi Loop Invariant Insertion Sort #

#include <iostream>
#include <vector>

void insertionSort(std::vector<int>& v) {
    for (std::size_t i = 1; i < v.size(); ++i) {
        int key = v[i];
        int j = static_cast<int>(i) - 1;
        while (j >= 0 && v[j] > key) {
            v[j + 1] = v[j];
            --j;
        }
        v[j + 1] = key;

        // Pemeriksaan invariant: v[0..i] harus terurut
        bool terurut = true;
        for (std::size_t k = 1; k <= i; ++k) {
            if (v[k - 1] > v[k]) { terurut = false; break; }
        }
        std::cout << "Setelah iterasi i=" << i
                  << " | v[0..i] terurut? "
                  << (terurut ? "YA" : "TIDAK") << '\n';
    }
}

int main() {
    std::vector<int> data = {5, 2, 8, 1, 4};
    insertionSort(data);
    std::cout << "Hasil akhir: ";
    for (int x : data) std::cout << x << ' ';
    std::cout << '\n';
    return 0;
}

Output yang Dihasilkan:

Setelah iterasi i=1 | v[0..i] terurut? YA
Setelah iterasi i=2 | v[0..i] terurut? YA
Setelah iterasi i=3 | v[0..i] terurut? YA
Setelah iterasi i=4 | v[0..i] terurut? YA
Hasil akhir: 1 2 4 5 8

Bedah Kode Baris-per-Baris #

1. Baris int key = v[i];: menyimpan elemen yang akan disisipkan ke variabel sementara. Pada titik ini, v[i] akan ditimpa, sehingga key menjadi satu-satunya tempat menyimpan nilai asli.
2. Baris while (j >= 0 && v[j] > key): menggeser elemen yang lebih besar dari key ke kanan. Loop berhenti saat j < 0 atau v[j] <= key.
3. Baris v[j + 1] = key;: menempatkan key pada posisi yang tepat. Pada titik ini, sub-array v[0..i] harus terurut.
4. Pemeriksaan invariant: loop for (std::size_t k = 1; k <= i; ++k) memeriksa bahwa v[0..i] terurut menaik. Pemeriksaan ini hanya untuk demonstrasi, tidak diperlukan di algoritma sebenarnya.
5. Output: setelah setiap iterasi, prefix v[0..i] memang terurut. Pada akhir, seluruh array 1 2 4 5 8 terurut. Inilah validasi numerik terhadap loop invariant.

Contoh 3: Binary Search #

Binary search memiliki loop invariant yang menarik karena melibatkan rentang aktif pencarian.

Loop Invariant #

Pada awal setiap iterasi, properti berikut benar:

P: bila target ada pada array v, maka target berada dalam rentang v[lo..hi].

Pembuktian #

Initialization (sebelum iterasi pertama): lo = 0 dan hi = v.size() - 1, sehingga rentang v[lo..hi] mencakup seluruh array. Bila target ada pada v, target pasti berada dalam rentang tersebut. ✓

Maintenance: asumsikan P benar. Iterasi menghitung mid = (lo + hi) / 2. Bila v[mid] == target, algoritma kembal. Bila v[mid] < target, target (jika ada) harus berada pada v[mid+1..hi], sehingga lo = mid + 1 mempertahankan invariant. Bila v[mid] > target, target (jika ada) harus berada pada v[lo..mid-1], sehingga hi = mid - 1 mempertahankan invariant. ✓

Termination: loop berhenti saat lo > hi. Pada titik ini, rentang v[lo..hi] kosong. Menurut P, bila target ada, target ada dalam rentang kosong — yang berarti target tidak ada. Algoritma mengembalikan -1 dengan benar. ∎

Kapan Loop Invariant Sulit Diterapkan #

Loop invariant cocok untuk loop yang terstruktur, tetapi sulit diterapkan pada:

• Loop dengan efek samping global: variabel yang dimodifikasi di banyak tempat.
• Loop dengan kondisi kompleks: while loop yang bergantung pada banyak variabel.
• Loop yang dimodifikasi dari banyak tempat (continue, break, return di tengah).
• Loop dengan iterasi non-deterministik: yang bergantung pada input user atau I/O.

Pada kasus ini, kita biasanya memecah loop menjadi bagian-bagian kecil yang masing-masing memiliki invariant sederhana, atau menggunakan teknik lain seperti axiomatic semantics atau program derivation.

Loop Invariant vs Induksi Matematis #

Loop invariant adalah induksi matematis terapan pada iterasi loop. Inisialisasi adalah kasus dasar, dan maintenance adalah langkah induksi. Pembagian tiga langkah ini akan kita pakai lagi di Chapter Induksi Matematis.

Ringkasan #

• Loop invariant adalah properti yang dipertahankan sepanjang eksekusi loop.
• Tiga langkah pembuktian: initialization (kasus dasar), maintenance (langkah induksi), termination (konklusi).
• Linear search: target tidak ditemukan pada prefix yang sudah diperiksa.
• Insertion sort: prefix v[0..i-1] terurut dan berisi elemen yang sama dengan array asli.
• Binary search: bila target ada, target berada dalam rentang v[lo..hi] aktif.
• Loop invariant adalah induksi matematis terapan pada iterasi.

Pada Chapter berikutnya kita akan mempelajari induksi matematis secara umum, sebagai fondasi untuk pembuktian algoritma yang lebih kompleks.