Correctness Algoritma

Setelah mempelajari loop invariant dan induksi matematis, kita siap menerapkan keduanya untuk membuktikan kebenaran algoritma secara formal. Pembuktian kebenaran bukan kemewahan akademis — algoritma yang salah dapat menyebabkan kerugian signifikan pada sistem produksi. Pada Chapter ini kita akan membuktikan kebenaran dua algoritma klasik: linear search (sebagai contoh sederhana) dan insertion sort (sebagai contoh lebih kompleks). Kita juga akan melihat bagaimana pembuktian membantu kita menemukan bug yang halus.

Apa itu Correctness #

Sebuah algoritma dikatakan correct (benar) jika untuk setiap input yang valid, algoritma tersebut:

Berhenti dalam waktu terbatas (termination).
Menghasilkan output yang benar sesuai spesifikasi (partial correctness).

Kombinasi keduanya disebut total correctness. Untuk algoritma yang sudah kita analisis kompleksitasnya (yang berarti pasti berhenti), fokus pembuktian adalah partial correctness.

flowchart LR A[Input valid] --> B[Algoritma] B --> C{Berhenti?} C -- TIDAK --> D[Tidak correct] C -- YA --> E{Output benar?} E -- TIDAK --> F[Partial correct gagal] E -- YA --> G[Total correct]

Membuktikan Linear Search #

Spesifikasi #

Diberikan array v berisi n elemen (boleh terurut atau tidak) dan nilai target. Algoritma linearSearch(v, target) harus mengembalikan:

Indeks i sehingga v[i] == target, bila target ada pada v.
-1 bila target tidak ada pada v.

Kode Program #

cpp
#include <iostream>
#include <vector>

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;
}

int main() {
    std::vector<int> data = {4, 2, 8, 1, 7, 3};
    std::cout << "cari 8  : " << linearSearch(data, 8) << '\n';
    std::cout << "cari 3  : " << linearSearch(data, 3) << '\n';
    std::cout << "cari 9  : " << linearSearch(data, 9) << '\n';
    return 0;
}

Output yang Dihasilkan:

text
cari 8  : 2
cari 3  : 5
cari 9  : -1

Pembuktian dengan Loop Invariant #

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

Initialization (i = 0): rentang v[0..-1] kosong, sehingga P(0) benar trivial.

Maintenance: asumsikan P(i) benar. Iterasi memeriksa v[i]:

Bila v[i] == target, algoritma return i. Loop berhenti. (Kasus sukses.)
Bila v[i] != target, iterasi berlanjut ke i+1. Sekarang P(i+1) menyatakan target tidak ditemukan pada v[0..i] — yang benar karena P(i) benar dan v[i] != target.

Termination: bila loop berhenti tanpa return, berarti i == v.size(). Maka P(v.size()) menyatakan target tidak ditemukan pada v[0..v.size()-1], yaitu seluruh array. Algoritma return -1 dengan benar.

Bedah Kode Baris-per-Baris #

Baris for (std::size_t i = 0; i < v.size(); ++i): loop dari indeks 0 hingga n-1. std::size_t digunakan agar kompatibel dengan tipe kembalian v.size().
Baris if (v[i] == target) return static_cast<int>(i);: bila ketemu, langsung kembalikan indeks. static_cast<int> diperlukan karena i bertipe std::size_t (unsigned), sedangkan spesifikasi meminta int agar bisa mengembalikan -1.
Baris return -1;: jika loop selesai tanpa return, target tidak ditemukan. Pembuktian termination menjamin kebenaran return ini.
Output: untuk target 8 ditemukan di indeks 2 (data[2] = 8); target 3 di indeks 5 (data[5] = 3); target 9 tidak ada, return -1.

Membuktikan Insertion Sort #

Spesifikasi #

Diberikan array v berisi n elemen. Algoritma insertionSort(v) harus mengurutkan v secara in-place secara menaik (non-decreasing), dengan tetap mempertahankan himpunan elemen yang sama (multi-set).

Kode Program #

cpp
#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;
    }
}

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

Output yang Dihasilkan:

text

1 2 4 5 7 8

Pembuktian dengan Loop Invariant #

Loop Invariant P(i): pada awal iterasi i, sub-array v[0..i-1] memenuhi dua properti:

Terurut menaik.
Berisi elemen yang sama dengan sub-array asli v[0..i-1] (multi-set sama).

Initialization (i = 1): v[0..0] berisi satu elemen, yang terurut secara trivial. Himpunan elemennya sama dengan aslinya karena belum ada modifikasi. P(1) benar.

Maintenance: asumsikan P(i) benar. Iterasi i mengambil key = v[i]. Inner loop menggeser elemen v[0..i-1] yang lebih besar dari key ke kanan satu posisi, sampai menemukan posisi tempat key seharusnya berada (v[j] <= key).

Setelah inner loop, semua elemen di v[j+2..i] adalah elemen yang sebelumnya di v[j+1..i-1] yang lebih besar dari key, digeser ke kanan.
v[j+1] ditempati key.
Akibatnya, v[0..i] sekarang terurut: v[0..j] terurut (sudah sebelumnya, dan tidak berubah), v[j+1] = key, dan v[j+2..i] terurut (semuanya > key dan terurut relatif satu sama lain).
Multi-set v[0..i] sama dengan multi-set asli v[0..i] karena hanya pergeseran terjadi, tidak ada elemen yang ditambah atau dibuang.

Maka P(i+1) benar.

Termination: loop berhenti saat i == v.size(). Pada titik ini, P(v.size()) menyatakan v[0..v.size()-1] (seluruh array) terurut dan multi-set-nya sama dengan aslinya. Inilah spesifikasi insertion sort.

Bedah Kode Baris-per-Baris #

Baris int key = v[i];: menyimpan elemen yang akan disisipkan. Setelah ini, slot v[i] boleh ditimpa.
Baris while (j >= 0 && v[j] > key): inner loop menggeser elemen yang lebih besar dari key. Kondisi j >= 0 diperiksa lebih dulu untuk menghindari akses v[-1].
Baris v[j + 1] = v[j]; --j;: menggeser v[j] ke kanan, lalu mengurangi j. Variabel v[j] sebelumnya akan ditimpa pada iterasi berikutnya (atau ditempati key setelah loop).
Baris v[j + 1] = key;: menempatkan key pada posisi yang tepat. Setelah baris ini, v[0..i] terurut.
Output: array {5, 2, 8, 1, 4, 7} diurutkan menjadi {1, 2, 4, 5, 7, 8}.

Pembuktian Membantu Menemukan Bug #

Mari kita lihat contoh implementasi buggy insertion sort dan bagaimana pembuktian membantu menemukannya.

Kode Buggy #

cpp
void insertionSortBuggy(std::vector<int>& v) {
    for (std::size_t i = 1; i < v.size(); ++i) {
        int j = static_cast<int>(i) - 1;
        // Bug: key tidak disimpan, langsung pakai v[i]
        while (j >= 0 && v[j] > v[i]) {       // v[i] berubah setelah digeser!
            v[j + 1] = v[j];
            --j;
        }
        v[j + 1] = v[i];                       // v[i] sudah ditimpa
    }
}

Analisis dengan Loop Invariant #

Pada iterasi pertama yang melakukan penggeseran, v[i] akan ditimpa oleh v[j] (saat v[j+1] = v[j] dengan j+1 == i). Akibatnya, nilai v[i] asli hilang. Loop invariant P(i) gagal dipertahankan: multi-set v[0..i] setelah iterasi tidak sama dengan aslinya.

Pembuktian maintenance memerlukan key disimpan secara terpisah, sehingga meskipun v[i] ditimpa, nilai asli masih tersedia. Inilah mengapa baris int key = v[i]; pada implementasi benar bukan sekadar gaya, tetapi kewajiban untuk mempertahankan invariant.

Kode: Verifikasi Bug #

cpp
#include <iostream>
#include <vector>

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

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

Output yang Dihasilkan:

text

Hasil buggy: 5 5 8 8 8 8

Bedah Kode Baris-per-Baris #

Output 5 5 8 8 8 8: bandingkan dengan input {5, 2, 8, 1, 4, 7} dan hasil benar {1, 2, 4, 5, 7, 8}. Sebagian besar elemen asli hilang, digantikan oleh 5 dan 8 yang merupakan elemen awal yang nilainya ikut “terseret” saat penggeseran.
Penyebab: saat i = 1, v[i] = 2. Inner loop membandingkan v[0] = 5 > v[i] = 2, lalu menggeser v[1] = v[0] = 5. Sekarang v[i] = v[1] = 5, bukan lagi 2. Iterasi berhenti karena v[0] = 5 tidak lebih besar dari v[i] = 5. Setelah loop, v[0] = v[i] = 5. Nilai 2 dan elemen lainnya hilang karena terus ditimpa.
Konsekuensi: multi-set elemen rusak parah. Loop invariant P(i) gagal dipertahankan — tidak hanya multi-set berubah, tetapi juga elemen-elemen yang seharusnya tidak ikut digeser ikut berubah.
Implikasi: pembuktian bukan sekadar formalitas. Pembuktian membantu kita memahami mengapa kode tertentu ditulis dengan cara tertentu, sehingga kita tidak “merapikan” kode dengan cara yang melanggar invariant.

Strategi Pembuktian Umum #

Berikut strategi yang dapat dipakai untuk membuktikan algoritma:

Identifikasi spesifikasi: apa input valid, apa output yang diharapkan.
Tentukan loop invariant / hipotesis induksi yang cukup kuat untuk menyimpulkan spesifikasi.
Buktikan initialization: invariant benar sebelum iterasi pertama.
Buktikan maintenance: invariant tetap benar setelah iterasi.
Buktikan termination: loop pasti berhenti (biasanya melalui analisis kompleksitas).
Konklusikan correctness: saat loop berhenti, invariant + kondisi loop exit memberi spesifikasi.

Ringkasan #

Correctness algoritma = termination + partial correctness.
Linear search dibuktikan dengan loop invariant “target tidak ada di prefix yang sudah diperiksa”.
Insertion sort dibuktikan dengan loop invariant “prefix terurut dan multi-set sama dengan aslinya”.
Pembuktian membantu menemukan bug halus, seperti duplikasi elemen atau kehilangan elemen pada implementasi yang terlihat “hampir benar”.
Strategi umum: spesifikasi → invariant → initialization → maintenance → termination → konklusi.

Pada Chapter berikutnya kita akan beralih ke recurrence relation — alat formal untuk menganalisis kompleksitas algoritma rekursif.